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 prove the existence of a universal recovery channel that approximately recovers states on a v. Neumann subalgebra when the change in relative entropy, with respect to a fixed reference state, is small. Our result is a generalization of previous results that applied to type-I v. Neumann algebras by Junge at al. [arXiv:1509.07127]. We broadly follow their proof strategy but consider here arbitrary v. Neumann algebras, where qualitatively new issues arise. Our results hinge on the construction of certain analytic vectors and computations/estimations of their Araki-Masuda norms. We comment on applications to the quantum null energy condition.
This mission is the statement-level formalization of Approximate recovery and relative entropy I. general von Neumann subalgebras (arXiv:2006.08002v1). 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 A support-dominating state in a closed convex family (Lemma 2: support-dominating state in a closed convex set, 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.
31 results of the paper are not stated yet, because the library lacks an interface they need:
We present an efficient machine learning (ML) algorithm for predicting any unknown quantum process over qubits. For a wide range of distributions on arbitrary -qubit states, we show that this ML algorithm can learn to predict any local property of the output from the unknown process~, with a small average error over input states drawn from . The ML algorithm is computationally efficient even when the unknown process is a quantum circuit with exponentially many gates. Our algorithm combines efficient procedures for learning properties of an unknown state and for learning a low-degree approximation to an unknown observable. The analysis hinges on proving new norm inequalities, including a quantum analogue of the classical Bohnenblust-Hille inequality, which we derive by giving an improved algorithm for optimizing local Hamiltonians. Numerical experiments on predicting quantum dynamics with evolution time up to and system size up to qubits corroborate our proof. Overall, our results highlight the potential for ML models to predict the output of complex quantum dynamics much faster than the time needed to run the process itself.
This mission is the statement-level formalization of Learning to predict arbitrary quantum processes (arXiv:2210.14894v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
37 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Corollary 3 (Norm inequality for general 𝑘-local Hamiltonian) (Corollary 3 (Norm inequality for general 𝑘-local Hamiltonian), 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.
17 results of the paper are not stated yet, because the library lacks an interface they need:
Let be a real finite-dimensional Lie algebra containing pointed generating invariant closed convex cones. We determine those derivations of which induce a 3-grading of the form on such that the -eigenspaces of are generated by the intersections with generating cones of the form , where is the coadjoint orbit of a linear functional and is the dual cone of . In particular, we show that, if is solvable, no such derivation except the trivial one exists. This continues our classification of Lie algebras generated by Lie wedges of endomorphism semigroups of standard subspaces. The classification is motivated by the relation of nets of standard subspaces to Haag-Kastler nets of von Neumann algebras in Algebraic Quantum Field Theory.
This mission is the statement-level formalization of Lie wedges of endomorphism semigroups of standard subspaces in admissible Lie algebras (arXiv:2007.13445v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
25 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 3.17 (Non-degeneration Theorem); precise result selected for the seed (Theorem 3.17 (Non-degeneration Theorem); precise result selected for the seed, PDF p. 23). 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:
Unitary equivariance is a natural symmetry that occurs in many contexts in physics and mathematics. Optimization problems with such symmetry can often be formulated as semidefinite programs for a -dimensional matrix variable that commutes with , for all . Solving such problems naively can be prohibitively expensive even if is small but the local dimension is large. We show that, under additional symmetry assumptions, this problem reduces to a linear program that can be solved in time that does not scale in , and we provide a general framework to execute this reduction under different types of symmetries. The key ingredient of our method is a compact parametrization of the solution space by linear combinations of walled Brauer algebra diagrams. This parametrization requires the idempotents of a Gelfand-Tsetlin basis, which we obtain by adapting a general method arXiv:1606.08900 inspired by the Okounkov-Vershik approach. To illustrate potential applications, we use several examples from quantum information: deciding the principal eigenvalue of a quantum state, quantum majority vote, asymmetric cloning and transformation of a black-box unitary. We also outline a possible route for extending our method to general unitary-equivariant semidefinite programs.
This mission is the statement-level formalization of Linear programming with unitary-equivariant constraints (arXiv:2207.05713v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 2.2: equivariance characterized by the Choi commutator (Proposition 2.2: equivariance characterized by the Choi commutator, PDF p. 10). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
15 results of the paper are not stated yet, because the library lacks an interface they need:
The quantum Schur transform maps the computational basis of a system of qudits onto a \textit{Schur basis}, which spans the minimal invariant subspaces of the representations of the unitary and the symmetric groups acting on the state space of -level systems. We introduce a new algorithm for the task of weak Schur sampling. Our algorithm efficiently determines both the Young label which indexes the irreducible representations and the multiplicity label of the symmetric group. There are two major advantages of our algorithm for weak Schur sampling when compared to existing approaches which proceed via quantum Schur transform algorithm or Generalized Phase Estimation algorithm. First, our algorihtm is suitable for streaming applications and second it is exponentially more efficient in its memory usage. We show that an instance of our weak Schur sampling algorithm on qubits to accuracy requires only qubits of memory and gates from the Clifford+T set. Further, we show that our weak Schur sampling algorithm on qudits decomposes into gates from an arbitrary fault-tolerant qudit universal set, for , and requires a memory of qudits to implement.
This mission is the statement-level formalization of Weak Schur sampling with logarithmic quantum memory (arXiv:2309.11947v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Streaming weak Schur sampling with logarithmic quantum memory at fixed local dimension (Abstract; III and III.A, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
3 results of the paper are not stated yet, because the library lacks an interface they need:
A nonprofit choosing how to serve people with different needs may have two ways to use an additional dollar: offer more product variants, or deliver a larger fraction of each product. Beneficiaries can sometimes finish an incomplete product themselves, but doing so takes effort. Zhang, Atasu and Ramachandran study this choice for services such as incremental housing and temporary shelter. The question is how a limited budget changes the optimal combination of variety and completion.
The paper’s main text first models the beneficiaries’ needs and the nonprofit’s costs, then derives the allocation pattern in Lemmas 1–2 and Proposition 3. This mission targets those results in the authors’ SSRN version. The optimization is over a continuous variety level, as the paper explicitly assumes in §4.2; the integer case has a different comparative static for completion at footnote 5 on p. 13.
A variety level describes how many equally spaced variants the nonprofit offers to a unit mass of beneficiaries with uniformly distributed ideal locations. The analysis treats as a real decision variable. A completion level is the fraction of each variant the nonprofit provides. Heterogeneity reduces the utility of a complete variant with distance from a beneficiary’s ideal. Aggregating the closest variant’s utility gives §3, pp. 7–8.
Each beneficiary may complete at most of the product. With quadratic effort cost , where , optimal self-completion effort is . The nonprofit’s expenditure is , where , , and for . Its total net benefit is
At a budget , a decision is feasible when , , and . An optimal decision is a feasible decision whose value of is at least that of every other feasible decision. Without the budget constraint, the same domain , defines the unconstrained problem §3, p. 10 and §4.2, pp. 12–13.
The standing assumption that provision is worthwhile says some satisfies . Let be the unconstrained optimal variety: it is when ; otherwise it is the solution above of . Write and . These are the unconstrained completion level and the budget needed to afford that pair Lemma 1, p. 12.
Lemma 1 asserts that maximizes without a budget constraint. Lemma 2 says every optimal decision exhausts its budget below :
Proposition 3 is the goal. It asserts thresholds , a small-budget variety , and middle-regime decisions such that an optimal pair can be selected as
Both and are nondecreasing on the middle interval, using the paper’s weak meaning of “increasing.” The goal characterizes using the appendix’s function : if , and otherwise is its zero. It also requires . These conditions retain the paper’s small-budget regime and prevent an arbitrary threshold from making it empty Proposition 3, p. 13; proof, Online Appendix p. 2.
The three regimes identify when a nonprofit should spend an increment of budget solely on completion, when variety and completion should rise together, and when additional budget no longer changes its choice. Lemma 1 also says that, even with ample funds, completing the entire product need not be optimal because beneficiaries can add value through their own effort §4.2, pp. 12–14.
The paper proves these claims analytically. This mission asks for machine-checked proofs of the continuous model’s optimization statements, including the attainment and feasibility of each claimed optimum. The reusable part is a compact interface for a two-variable budget-constrained optimization problem with a beneficiary best response. There is no existing machine-checked proof of these particular claims in the platform catalog at drafting time.
The binding-budget curve crosses the point , where beneficiary effort changes formula. Thus optimizing a single smooth expression over all variety levels does not cover the problem. A stationary point calculated in one region also must be checked against feasible points in the other. The argument needs to establish global optimality and preserve the bounds as the budget changes Online Appendix pp. 2–3.
The appendix’s candidate threshold in one case can exceed when the unconstrained variety is . Proposition 3 itself asks only for a threshold , so the formal goal retains that existential form. The proof’s candidate must be capped at in that case; the middle interval can then be empty. This discrepancy is recorded for solvers, who should establish the proposition as stated rather than assume the appendix’s candidate always satisfies the bound Online Appendix p. 3.
All quantities are real. The Lean model stores , , and as separate functions and requires the two derivative identities, positive and nonnegative for . It uses the closed formula for and the minimum formula for effort. The hypotheses , , and make explicit the economic parameter and budget domains; is needed for the stated variety characterization, and is implicit in the paper’s increasing quadratic effort cost. The paper’s , , and worthwhile-provision assumption are retained.
Optimality always includes membership in the feasible set. This rules out an out-of-domain maximizer. The upper regime asserts that the displayed pair is an optimum, allowing other optima when . Division by and is used only at varieties ; the standing assumptions imply there. The goal fixes by the paper’s formula and pins down , so it cannot be discharged by choosing arbitrary empty budget ranges. Proofs of the two appendix monotonicity claims, the binding-budget lemma, and the global small-budget optimum are welcome along with the goal.
Banks and other financial institutions are notoriously hard to see into: their loan books are complex and their public reports are coarse. A long-standing policy question is whether competition among financial institutions makes them more or less transparent. One view holds that competition for funding disciplines institutions into disclosing more; another that competitive pressure rewards opacity. G. Zhang, Competition and Opacity in the Financial System (SSRN 3428683; Management Science 2020, doi:10.1287/mnsc.2019.3512), gives an answer inside a coordination model in the tradition of Morris and Shin (2002) and Angeletos and Pavan (2004): competition lowers disclosure precision exactly when investors' own private information is precise.
The model belongs to the literature on public information in beauty-contest economies, where public reports serve both as information about fundamentals and as a focal point for coordination. The paper adds a second force, competition between two institutions for the same investors, and asks how the institutions' chosen precision of public disclosure responds.
Two financial institutions (FIs) raise funds from a continuum of risk-neutral investors . FI 's project has fundamentals , independent across , with prior mean and prior precision . Its return is
where is the aggregate investment in FI and is the FI's rollover-risk exposure: the more others invest, the higher the return.
Before learning , FI commits to a disclosure precision and pays . It then publishes with . Each investor also observes private signals of precision , and invests
in FI , where is the intensity of competition (: none; : the intense case analysed in the paper's main result). Here is investor 's posterior expectation; for Gaussian signals . A linear equilibrium of the investors' game is a strategy that satisfies this rule when every investor uses it.
FI 's payoff is . A disclosure equilibrium is a pair of precisions, each a best response to the other given the investors' linear equilibrium. Write for the equilibrium precision without competition () and for the one with competition.
For sufficiently large:
The goal fixes no constants: is only asserted to exist.
Proposition 4 is the paper's main result. It separates two channels through which competition acts on disclosure: competition amplifies investors' reaction to every signal, which both reduces the coordination problem that disclosure is meant to solve and raises the value of a precise report for allocating funds between the institutions. Which effect dominates depends on the precision of private information, and the result pins this down to a single threshold. Without rollover risk the two channels vanish and competition is neutral. The paper's policy discussion of opacity in the financial sector (§3.3–§4) and its welfare analysis rest on this comparison.
The result is proved in the paper by hand computation; it has no machine-checked proof. Formalizing it requires the Gaussian payoff computation, a linear fixed-point argument for the investors' game, an optimization argument for the institutions' disclosure choice under a large-cost assumption, and a sign analysis of an explicit quartic.
The payoff is an expectation of a quadratic in four independent Gaussians whose coefficients are themselves the solution of the investors' fixed point. Differentiating it in means differentiating through the equilibrium coefficients, and at the coefficients of FI depend on both precisions; the closed form (44) holds only after cross terms cancel.
The comparison is global in . Reading off the sign of the marginal payoff at gives a condition on , not on , and itself moves with . A threshold on exists only because is monotone and the quartic changes sign once. The "sufficiently large " must be uniform in : a bound that depends on does not give a single threshold.
Fin 2 (FI 1 of the paper is 0), the other FI is i.rev. The law of is a product of Mathlib gaussianReal measures; precision is variance . At the noise is a point mass, and the equilibrium puts no weight on .Classical.epsilon; Lemma 1 and Proposition 3 show it is determined in every coefficient the payoff uses. A disclosure equilibrium is a Nash equilibrium in .Electric vehicle adoption depends on both the number of drivers willing to buy a vehicle and the availability of places to charge it. These decisions reinforce one another: an additional charging pile reduces expected search cost, while an additional vehicle increases demand for charging. A city may subsidize the vehicle purchase, each charging session, or the construction of a pile. The instruments can have different effects even when the public spending they require is equal. Zhang and Dou study these tradeoffs in a two location market with different pile costs and charging inconvenience. Their 2021 paper gives conditions under which one subsidy has a greater marginal effect on gross social surplus than another.
The target here is the paper's Theorem 3. It addresses a local comparison of policy instruments at a given policy mix. It does not claim that a policy satisfying a condition is globally optimal or that the same ranking holds after a large change in subsidy.
There are two locations, A and B. A fraction of potential drivers resides at A and the remainder at B. Driver type measures the annual benefit of using an electric vehicle. In the base model it has distribution for , with . A vehicle costs per year, and each driver needs one charging session every years. A session occupies a pile for time .
At location , a session has regulated fee , waiting cost , and expected search cost when expected pile utilization is . Drivers at A charge at A. Drivers at B choose between the locations using the paper's logit probabilities and ; their expected cost is a log sum of the two location costs. The purchase threshold is , where is the vehicle purchase subsidy. These thresholds, the purchase probabilities , and the choice probabilities determine the arrival rates and .
Charging service providers choose piles per provider to maximize annual profit, taking expected utilization as fixed. The number of providers is ; a pile at costs annually. A policy pays per pile and per session, in addition to per vehicle purchase. A rational expectations equilibrium matches each expected utilization with the actual ratio , while the provider's pile choices maximize profit. The mission uses the positive pile regime of the paper's equilibrium analysis. In it, Theorem 1 determines .
Gross social surplus, denoted , has three components in equation (8): the external benefit , the integral of driver surplus above each purchase threshold, and provider surplus. The total subsidy value and the government's objective are represented separately. The goal compares derivatives of per equal increment in subsidy value, following the normalization in the proof of Theorem 3.
Theorem 1 asserts existence and uniqueness of the positive pile equilibrium. The proof of Theorem 3 also states that provider break even makes its gross social surplus equal to
This is a theorem about the surplus defined by equation (8), not its definition. The milestone list also records the purchase subsidy derivative and bounds on the usage and pile subsidy derivatives given in the paper's technical proof.
The goal is Theorem 3. Write . For a pile subsidy mix , a sufficient condition for the purchase subsidy to yield at least as much additional gross social surplus as the paper's pile subsidy direction at equal marginal spending, when the pair is balanced and the subsidies are nonnegative, is
For a nonnegative usage subsidy mix , a sufficient condition for usage subsidy to yield at least as much is
Here is the efficiency of the vehicle purchase subsidy relative to subsidies paid to providers. The inequalities are local sufficient conditions; they make no claim about large policy changes.
The two conditions connect the subsidy ranking to pile cost, search cost, charging time, and subsidy efficiency. They identify parameter regimes in which a city can increase gross social surplus more through charging side support, or more through vehicle purchase support, at equal marginal subsidy value. This gives a precise comparison within the paper's model, complementing its separate results on spatial mismatch and policy optima. The source result and its proof are published in the authors' version; this mission asks for a machine checked formalization of that known result.
A complete development would also supply reusable results on the exponential tail integral, derivatives of logit choice probabilities, and the relationship between a profit maximizing provider choice and equilibrium utilization. Those statements are useful for other two sided adoption and infrastructure models that combine provider investment with consumer choice.
Changing a subsidy changes more than the direct transfer. It changes utilization, search costs, the logit split of B's charging sessions, vehicle purchase thresholds, and both arrival rates. A comparison that looks only at the direct increase in purchases misses the displacement of charging activity between A and B. The pile subsidy comparison is especially sensitive to the direction in which the two pile subsidies change: equal changes in and do not have equal marginal effects or equal costs. The equilibrium quantities must also be connected to the derivatives of the actual surplus expression rather than to an assumed closed form.
The Lean model uses real valued parameters, policies, utilizations, arrival rates, and pile counts, with two explicit locations. It fixes , as the base model does. The standing assumptions are , , , , , , and . It also requires : the externality is described as a benefit, and the derivative comparisons use its nonnegative contribution. The interior regime is and at both locations. Positive purchase thresholds are required at derivative evaluation points because the exponential distribution has a boundary at zero.
Equation (10) is expressed by , with utilization constrained below one. This excludes a division by zero that would otherwise create a false zero pile equilibrium in Lean. The distribution function is zero below zero. The subsidy value is , read from the proof's displayed derivatives on p. S10 and its treatment of pile subsidies on p. S9. The goal quantifies over every equilibrium selection on the interior regime and asserts such a selection exists. Its marginal comparisons use and the pile subsidy direction . A pile subsidy pair is balanced if no feasible nonnegative pair with the same equilibrium subsidy value yields higher gross social surplus. The goal requires this condition for the pile subsidy comparison and requires nonnegative subsidies at each policy mix.
The formalization must retain equation (8)'s driver surplus integral and provider surplus. Defining by the break even closed form would make the goal circular. Contributions on the source's integral, equilibrium existence, derivative bounds, and the connection to the selected equilibrium are within scope.
Intertemporal choice compares outcomes received at different times. A familiar model assigns each instantaneous outcome a utility and aggregates those utilities with a time weight. That model is useful in economics and operations research, but its meaning depends on what choices are feasible and how a preference over one stretch of time relates to a preference over another. When outcomes must vary continuously, an agent cannot freely paste two trajectories together at a chosen instant. Pivato's 2018 preprint asks which observable properties of preferences still force an integral representation under that constraint. The resulting theorem concerns a finite horizon; the paper also develops distinct infinite-horizon representations, which are outside this mission.
Earlier discounted-utility models often begin with an integral or a discounted sum and then study its implications. Here the integral is the conclusion. This changes the formalization problem: the preference structure, the permitted trajectories, and the relation between preferences on overlapping time regions must be defined independently of any utility or discount function. Theorem 1 on p. 13 is the paper's finite-horizon characterization. The Appendix A and B results selected as milestones connect its structural axioms to a content-based representation and then to an integral.
Time is the compact interval , with . The outcome space is connected, and a trajectory is a continuous map from to . A set of feasible trajectories includes every constant trajectory , which gives outcome at every time. Feasibility is substantive: a trajectory obtained by pasting arbitrary continuous pieces may fail to be continuous at the join.
A time interval is relatively open in . It includes when and when , but excludes any interior endpoints. A time span is a finite union of disjoint such intervals with distinct endpoints. The empty span is allowed. Relative interior and closure give the Boolean operations and . These operations can bridge omitted boundary instants.
For every time interval , a primitive preference order compares restrictions of members of to . Each such order is complete, transitive and nontrivial. The order on the whole horizon is ; its comparison of constant trajectories induces the synchronic preference on outcomes. Preferences on general spans are induced through the paper's limited-separability construction: representatives agree with the compared trajectories on , are indifferent on each component of , and are then compared on the full horizon. The representatives must belong to .
The axioms constrain this primitive structure. Richness (R) permits preference-preserving insertion of a middle trajectory between fixed outer restrictions. Minimal equicontinuity (MinEqn) requires interiors of synchronic contour preimages to be time spans. The eight characterization axioms are interval separability (ISep), limited separability (LSep), static equivalence (StEq), continuity of synchronic preferences (C), dominance (Dom), continuity of intertemporal preferences (CIP), tradeoff consistency (TC), and ephemerality (Eph). Their definitions refer only to preferences and feasible trajectories.
A discounted utility integral representation consists of a continuous utility and a continuous, strictly increasing map with and . For every time span and feasible restricted trajectories , it satisfies
The goal is Theorem 1 of the preprint: under the standing preference assumptions, (R), and (MinEqn), the eight axioms hold if and only if such a representation exists. The theorem also says that the normalized is unique and that any two representing utility functions differ by for some and . The milestone list includes the structural equivalences of Lemmas A1, A3 and A4; the compatibility and separability results of Lemma A5 and Proposition A6; the richness result of Lemma A9; the comeasurability claim of Lemma B1; and the content-utility characterization in Theorem B2(b).
The characterization identifies when local comparisons, continuity, and consistency of tradeoffs across regions of time determine one common utility scale and one normalized time weight. The uniqueness clauses prevent two different discount profiles from representing the same structure, while allowing the expected positive affine freedom in utility. Without the characterization, an integral can be used as an example of a preference rule, but the stated axioms would not certify that every admissible rule has that form.
The paper gives a mathematical proof, but this mission records open Lean statements rather than verified proofs. A completed development would make the time-span algebra, the induced intermittent order, and the content integrator reusable for related representation results. It would also expose precisely where the finite-horizon assumption is used before adapting the framework to the paper's later infinite-horizon theorems. The cited preprint relies in part on companion results about contents and their measure representations; formal proofs of those results are welcome groundwork.
Continuous trajectories cannot generally be pasted at a time boundary while remaining feasible. This blocks the immediate finite-product argument often used for separable preferences. The paper's richness conditions replace that maneuver with preference-equivalent trajectories whose restrictions can be coordinated across component intervals. A second difficulty is that a finitely additive content on regular-open spans is not automatically a Borel measure: the representation needs a way to account for boundary behavior before the integral formula follows. The source treats this in its appendices and invokes companion work.
Lean uses the subtype with its relative topology, continuous maps for feasible trajectories, and sets of subtype times for spans. A member of is represented by a full member of , so comparisons never range over arbitrary functions on . The intermittent order is existentially induced from whole-horizon comparisons; a universally quantified extension rule could be vacuous when no extension exists. The axioms are stated directly on preferences, without mentioning or .
The integral is represented by integration against the Lebesgue–Stieltjes measure of a continuous StieltjesFunction. This is the paper's Riemann–Stieltjes expression on bounded continuous integrands, using its equation (B12). Integrals are restricted to the image of the span in . The representing function is normalized at both horizon endpoints; uniqueness compares its values on . Both the final integral representation and the intermediate content representation require agreement with primitive interval orders, in accordance with their identification with induced orders in Lemma A5. The intermediate utility also represents synchronic preference.
The strict clauses of (Dom), (TC), and (CIP) range over nonempty spans; at the empty span their literal unqualified forms become contradictory. Condition (R) is stated for a nonempty middle interval, : with as printed, continuity would force the two outer trajectories to agree at , which no set containing two distinct constant trajectories in a Hausdorff outcome space can satisfy. These domain choices and the specialization of Appendix B's Theorem B2 to are recorded in the moderation notes. Definitions of time spans, preference orders, contents, simple-function integration, and the measure connection are reusable contributions. Machine-checked proofs of the listed milestones and of the final equivalence are the intended contributions.
Large bonuses in some industries are paid within a few weeks of each other across firms: banks in a given region announce bonuses in the same months, and top-tier US law firms announce theirs almost simultaneously. Van Wesep and Waters (SSRN 3124536, published in Management Science, 2022, doi:10.1287/mnsc.2021.4076) explain this coordination with a search model of the labor market. If many workers leave their employers at the same time of year, the labor market is deeper at that time, which makes it a better time to replace a worker who has become a poor match. Firms then have reason to make dissatisfied workers stay until that time, which a bonus at the end of the cycle achieves, and the bonuses in turn concentrate quits at that time. The question is when this self-reinforcing seasonality is an equilibrium.
The model builds on the search-theoretic labor market with an aggregate matching function (surveys: Petrongolo and Pissarides, 2001; Rogerson, Shimer and Wright, 2005) and on wage bargaining with transferable utility.
Time is discrete; periods alternate between odd (index 1) and even (index 2). A continuum of firms of mass and of workers of mass , , are either matched in pairs or searching. A match produces revenue per period. A new worker is satisfied, with per-period disutility ; at the end of each period a satisfied worker becomes dissatisfied, with disutility , with probability , and stays so; matches separate exogenously with probability ; workers may quit at the end of any period. Here and , the discount factor. The importance of match quality is
If firms and workers search, matches form, where is homogeneous of degree one, increasing in each argument, differentiable, and (Assumption A1). A vacant firm matches with probability and an unemployed worker with probability ; these depend only on the labor market depth .
In the periodic turnover plan, a dissatisfied worker quits at the end of even periods and stays at the end of odd periods. Under it the masses searching at the start of each period solve a fixed system of flow equations, which yield matching likelihoods . A newly matched pair bargains over pay with worker weight (generalized Nash bargaining); the resulting values (firm with a new hire), (vacant firm), (new hire, gross of pay), (unemployed worker) and the bargained present value of pay solve a linear system together with the Nash conditions. With and the paper defines two thresholds
A periodic equilibrium consists of a labor-market state solving the flow equations, with depth differing between odd and even periods; Nash-bargained values; Pareto optimality of the periodic plan for every newly matched pair (no other turnover plan yields a larger joint value); and a periodic contract (a signing bonus depending on the hiring period, a wage in odd and in even periods) that makes the periodic plan incentive compatible and delivers the bargained present values , .
With computed from the solution of the flow equations,
Proposition 2 is the existence result on which the paper's account of coordinated bonuses rests: the subsequent results on equilibrium contracts (that rising wage profiles, i.e. end-of-cycle bonuses, always implement the equilibrium and are sometimes necessary) and on the stylized facts of compensation in finance and law presuppose a periodic equilibrium. It shows that seasonality of labor markets can be self-sustaining, with no exogenous seasonal shock, exactly when match quality matters neither too little (then dissatisfied workers are never released) nor too much (then they are released at once).
The result is proved in the paper by hand algebra over a dozen coupled equations. No part of it is machine-checked, and the platform has no search-and-matching labor market, no aggregate matching function and no turnover contract. The mission produces a checked version of the existence characterization, of the closed forms behind it, and a reusable formal model of a two-period search market with Nash-bargained, incentive-compatible contracts.
Lemma 2's existence and ordering do not follow from monotonicity of alone: the flow equations couple both periods, and the natural scalar reduction evaluates outside its domain when , so the interval on which an intermediate-value argument runs must be chosen with care. The closed forms of Lemma 3 come from eliminating ten unknowns from a linear system whose coefficients are themselves the matching likelihoods; the paper's own equation (21) contains a typo that makes (29) false if taken literally. The thresholds of Proposition 1 require turning two inequalities on joint values into inequalities in , where the sign of each denominator has to be controlled. Finally, the equilibrium compares the periodic plan with every alternative plan through their joint-value recursions, not through the closed forms.
All quantities are real. Periods are indexed 1 (odd) and 2 (even); firm masses are derived, . Assumption A1 is stated on the closed quadrant, with "increasing" read strictly, which Lemma 2's strict inequalities require. Equation (21) is used with restored, . Nash transfers are defined as maximizers of the Nash product, not by (24)–(25). Definition D3 is imposed as . Pareto optimality compares the four turnover plans that are stationary across periods of the same parity, with satisfied workers never quitting, through their joint-value recursions. Present values of contracts are infinite sums. The goal leaves the endpoints open: the paper's statement excludes them while its proof includes them. Proposition 1's printed interval is read as , as in its proof.
The periodic equilibrium is not defined through , , conditions (i)–(ii) or the closed forms, which would make the goal a tautology; it is built from the market equations, the bargaining problem, the plan comparison and the contract.
Corollary 1, Proposition 3, Lemmas 6–7 and §5–6 are not part of this mission. Contributions to the infrastructure (Nash split, geometric tsum evaluation of periodic present values, contraction arguments for the value recursions) are welcome and reusable for other search and bargaining models.
Manufacturers of durable products — airlines' aircraft, consumer electronics, cars — increasingly hand the after-sales product service (help desks, repair, field maintenance) to a third-party provider. The provider is often more cost-efficient, and the brand can concentrate on its core product. The price of outsourcing is visibility: once the service is run by someone else, the brand no longer observes the service environment that drives the cost of serving customers, and it pays the provider on the basis of a belief that drifts away from reality as unobserved shocks accumulate.
Y. Wang, M. Li, N. Ma and H. Zhang (MSOM 2024, doi:10.1287/msom.2022.0222) model this trade-off with a martingale model of forecast evolution (MMFE, in the sense of Heath and Jackson 1994): the environment evolves by multiplicative mean-one lognormal shocks, and after outsourcing the brand stops seeing them. Their Proposition 4 shows that this loss of visibility alone — with no switching cost, a cheaper provider and a product-value gain — can make outsourcing unprofitable. The question belongs to the operations literature on service outsourcing under information asymmetry (e.g. Hasija, Pinker and Shumsky 2008; Feng, Ren and Zhang 2019).
A single service period is described by the following data.
Partial observability. The brand holds a belief about the environment. The true environment is , where the unobserved shock is lognormal with mean and variance parameter (the variance of ). Equivalently, with .
Payment. Without reporting, learning or monitoring, the brand pays ; when the true environment exceeds the belief, the provider's participation constraint forces the payment up to . With full observability the payment would be always.
Value of outsourcing. , and is the same expectation with the full-observability payment. The error function is .
For all parameters satisfying the standing assumptions:
with a pointwise nonnegative loss term (part (a): only an upward drift of the belief matters);
(part (b)); and (part (c)) there exist admissible parameters with , and some such that .
The result. Proposition 4 separates two effects that are usually conflated in the outsourcing literature: environment uncertainty, which makes outsourcing more attractive (the provider absorbs a growing cost), and partial observability, which erodes its value. It shows that the second can dominate on its own: the value lost when the belief overshoots the true environment grows with the accumulated variance, and with a long enough relationship it wipes out both the provider's cost advantage and the product-value gain. This underpins the paper's later analysis of learning and monitoring (§5.1–§5.2), which are evaluated by how much of this loss they recover.
Formalizing it. The result is proved in the paper; nothing in it is machine-checked. The mission produces a checked version of the benchmark analysis with every hidden convention made explicit: the representation of the lognormal shock, the payment rule at the boundary, and the per-period reading of . Along the way it produces reusable facts about mean-one lognormals — the mean identity, the closed form of their lower tail and of their truncated first moment in terms of erf, and the monotonicity of the tail in the volatility — which recur wherever MMFE-type forecast evolution is used.
The model-level algebra is short; the work is in the probability. The parts of the argument that are not routine are:
The obvious shortcut — replacing by an erf formula and proving monotonicity of erf — is exactly what the mission excludes: the closed form of is not stated in the paper and must be derived from the model.
All objects live in the namespace PSOutsourcing.PartialObs in one definitions file. Conventions committed to:
gaussianReal 0 1; the shock is xi s z = exp(s z − s²/2) and the true environment is xi s z * db.Real.log 0 = 0 cannot express the paper's ); Lemma 3(c) adds , which its proof uses; derivatives are stated with HasDerivAt.A formalization in which is defined by its closed form, or in which the payment ignores the participation constraint, trivializes the goal and is ruled out: is the expectation of the period-profit difference under the stated payment rule.
Infrastructure needed: erf and its relation to the standard normal distribution function, the Gaussian moment generating function (Mathlib's mgf_gaussianReal), truncated lognormal moments, and differentiation of Gaussian tail probabilities in a parameter. These lemmas are reusable well beyond this mission, and contributions of them as standalone theorems are welcome.
Asset-pricing models relate an asset's expected return to the risks it shares with the market. A familiar covariance term measures exposure to the market return, while a coskewness term measures exposure to the square of that return. Shi, Cui and Zhou ask how these two coefficients change when investors weight probabilities as well as valuing outcomes. Their 2020 working paper derives a market pricing kernel and a three-moment capital asset pricing relation from a representative investor's rank-dependent utility. The paper subsequently studies the signs of the coefficients and tests the resulting relationships with financial data; this mission concerns its theoretical pricing result, Theorem 2.
At date 0, investors choose positions in finitely many assets. At date 1, asset pays a random total return per unit invested. One asset is risk-free, so its total return is the constant . A pricing kernel is a strictly positive random variable that prices every total return by . The market return is , where the market-capitalization weights sum to one. A return rate subtracts the invested unit: and . These are the conventions of §§2–3 of the source.
The representative investor has rank-dependent utility. For a nonnegative payoff with cumulative distribution function , an outcome-utility function , and a probability-weighting function , its value is the distributional integral
The model assumes an atomless probability space; is strictly increasing and strictly concave on positive wealth, continuously differentiable there, and satisfies the Inada and asymptotic-elasticity conditions of Assumption 1; is strictly increasing and continuously differentiable on , with and . Problem (P′) asks for the largest among measurable nonnegative payoffs with . Equilibrium means that attains this value. The working paper states these assumptions and this optimization problem on pp. 8–9 and identifies equilibrium with the optimal market return in Appendix A, p. 33 (source).
Write for the CDF of and set . The paper defines the pricing function
The probability weight depends on the market distribution, while marginal utility depends on the realized total return. Their joint variation determines the pricing coefficients in Theorem 2 (source, pp. 10–11).
For an equilibrium whose market return has a continuous CDF, the goal begins with the almost-sure identity
Appendix A states an intermediate first-order form with a positive multiplier , then equation (12) determines from the risk-free asset. Both are milestones (source, pp. 33–34).
When has a continuously differentiable density , Theorem 2 gives a beta premium and a coskewness premium by the closed forms in its equations (6)–(7), with and . It states
The formal target makes the last term exact. Define , with as . The pricing identity then has remainder . The source's quadratic expansion (13), its premium identities (6)–(7), and its covariance pricing identity are the remaining milestones (source, pp. 11 and 34–35).
The kernel identity connects the market's state prices to both marginal utility and probability weighting. The three-moment relation then specifies how an asset's covariance and coskewness with the market enter its expected return. Without the kernel identity the coefficients would be free parameters; without the density and derivatives their explicit forms would be unavailable. The paper uses these coefficients to analyze beta and coskewness pricing under particular weighting functions and later compares the relationships with data (source, §§3–5).
The paper result is published in Operations Research; this mission follows the held SSRN version of June 2, 2020, whose theorem numbering and pages are pinned below. The Lean theorem statements in this proposal compile as open targets; they do not yet have machine-checked proofs. A completed development would add a reusable RDU model, a pricing-kernel characterization under equilibrium, and a precise covariance relation with a controlled remainder. The later parameter-specific propositions and empirical sections are outside this mission.
The central difficulty is the first part of the theorem. The optimality condition concerns an objective that depends on the entire payoff distribution through , so ordinary pointwise differentiation of does not identify the kernel. The paper obtains this step from an earlier result of Xia and Zhou, then uses the risk-free asset to fix the multiplier (source, Appendix A). The second part needs third derivatives of and although Assumption 1 only says they are continuously differentiable. It also uses a random-variable little-o without specifying how that term enters an expected return. These are mathematical conditions the formal statement must make explicit.
Lean represents the probability space by a probability measure and atomless by the event-splitting property: every positive-measure event has a measurable subset of strictly intermediate measure. Assets are indexed by Fin n; the risk-free asset is specified by its constant total return, and is computed from the weights and asset returns. The RDU objective is the paper's integral against the payoff law, including the CDF factor, and equilibrium is optimality for problem (P′). It is not defined through the desired kernel equation.
The Bochner RDU integral is required to be integrable for the market payoff and for compared competitors. Those competitors also have continuous CDFs and positive payoffs almost surely, so endpoint values of the two-sided derivatives and the utility at zero do not affect the comparison. This is a disclosed strengthening of the conclusion's scope: the equilibrium requirement compares fewer payoffs than the paper writes. The CAPM clause assumes local regularity of at and at , , a nonnegative density represented as the law of , and finite second and fourth moments needed for genuine covariances. Its premiums are the closed forms of (6)–(7), and its remainder is computed from , once for every asset. The kernel identity is a conclusion; an assumed kernel or an independently chosen remainder would erase the target.
The development uses Mathlib's CDF, pushforward and density measures, Bochner integrals, covariance, MemLp, derivatives, and little-o. The event-splitting predicate, priced-market interface, RDU functional, feasibility and equilibrium notions, closed-form premiums, and Taylor remainder are local definitions. Contributions to the first-order characterization, the derivative identities, the precise expansion, and the covariance step all advance the goal.
A trade moves the price at which subsequent trades are executed. Price impact models describe this shift as a function of the signed order flow and are the basic input of optimal execution and statistical-arbitrage problems. Empirically, the immediate impact of a trade is a concave function of its size, close to a square root for large orders (Bouchaud et al. 2009; Bucci et al. 2019), while most tractable models for optimal trading assume linear impact, as in the model of Obizhaeva and Wang (2013). Muhle-Karbe, Wang and Webster (SSRN 4286108; Operations Research, 2022) connect the two: when trades are small, frequent and diffusive, a nonlinear propagator model with concave impact converges to a linear impact model whose illiquidity parameter is stochastic and moves with the volatility of order flow. This mission formalizes that scaling limit, Theorem 3.3 of the paper, together with the steps of its proof in Appendix A.1.
Fix a horizon and a filtered probability space carrying two independent -Brownian motions and . The signed order flow is an Itô process with stochastic volatility,
where are locally bounded càdlàg processes, , and .
Divide into steps of width , with grid points and increments . An impact function is odd, continuously differentiable and concave on . The nonlinear propagator model (Definition 2.1) with the diffusive scaling (3.1) is the recursion
for a decay rate : each trade shifts the price by a concave function of its size, and the shift decays exponentially.
The limit involves Gaussian averages of . With the density of the centred normal law with standard deviation ,
and .
A limit of this kind lives on an extension of the probability space, a larger filtered space with a projection preserving the law; it is very good if every -martingale remains a -martingale. Stable convergence in law of processes on to on such an extension means for every bounded measurable on and every bounded path functional that is Lipschitz for the uniform distance on .
As , the step paths converge stably in law to a solution of the linear impact model
where is a Brownian motion on a very good extension with
stably in law, with standard normal and . 3. Rescaled convergence (p. 28): stably in law.
The theorem shows that the nonlinearity of microstructure impact does not disappear in the continuous-time limit; it is absorbed into a stochastic illiquidity that is an explicit Gaussian average of at the current order-flow volatility, plus an additional noise term and a drift correction . Section 4 of the paper uses the limit to solve optimal trading problems explicitly for nonparametric signals and to derive conditions that rule out price manipulation, and Section 5 fits the resulting model to public trading data. Without the limit theorem, those linear-model results would have no stated connection to the concave impact observed in the data.
The paper proves Theorem 3.3 by reduction to a functional central limit theorem of Jacod and Protter (2012, Theorem 10.3.2(a)), outlined in Appendix A.1 rather than written out. To our knowledge none of these results has a machine-checked proof. The mission produces a precise statement of the scaling limit, including the mode of convergence and the space on which the limit lives, and a formal statement of the stable functional CLT (Theorem A.3), which is a standard tool in high-frequency statistics and reusable well beyond this paper.
The impact process is not a functional of increments of a fixed process: solves a difference equation whose coefficients depend on the grid, so a central limit theorem for sums does not apply to it directly. Even for such sums the stable CLT is needed in full: the rescaled increments are of order one, so cannot be linearized pointwise, and the limit carries both a Gaussian average of and an independent noise term. The CLT itself is the hard part. Its limit lives on an extension of the original space, the drift term arises from the correlation between the volatility increments and the increments of , and stability (joint convergence with every bounded -measurable variable) is what allows the limit to be combined with the stochastic factor and with . A naive Taylor expansion of around zero gives the wrong limit for every nonlinear .
Time is and statements read . Brownian motions are IsBrownianReal with continuous paths for every , adapted, with increments independent of the past; Itô integrals use the published relation EthierKurtz_HasBrownianItoIntegral with continuous versions, and quadratic covariation the published EthierKurtz_HasCrossVariation. Itô coefficients are progressively measurable with locally integrable drift paths. is Mathlib's gaussianPDFReal 0 (v^2), whose parameter is the variance. Stable convergence is encoded with bounded measurable times bounded functionals Lipschitz for the -valued uniform distance on ; since the limits have continuous paths this matches Skorohod-topology stable convergence, and no Skorohod space is built. The goal is existential in the extension, in and in the solution ; a universal reading would be false.
Added and disclosed conventions: the growth bound (Assumption A.2(c), p. 25, required by the paper's proof); and ; capped at for the paper's ; for the negative powers on p. 27. The printed formulas for and are kept.
The statements cannot be satisfied trivially: is a solution of the integral equation (3.2), not a definition as the limit of ; the coefficients are the Gaussian integrals themselves; and the test class of stable convergence contains non-constant functionals, so convergence of the zero process to a non-zero limit fails (checked in a sorry-free sanity file).
A complete development needs a stable functional CLT for triangular arrays, Gaussian integration by parts, existence of very good extensions carrying independent Brownian motions, and pathwise stochastic calculus for Itô processes with stochastic volatility. The extension and stable-convergence definitions and Theorem A.3 are reusable for realized-variance and high-frequency estimators. Contributions on any milestone, and on the general infrastructure, are welcome.
How far apart are two preferences? Distance functions on preference relations are used to deduce a consensus ranking from a collection of individual preferences. The classical answer is the Kemeny–Snell metric (Kemeny and Snell 1962), proposed axiomatically for linear orders and extended by Bogart (1973) to partial orders. It counts rank reversals between two orders and weighs all of them equally: swapping the two best alternatives costs as much as swapping the two worst.
For a decision maker who chooses from menus, these swaps are not equivalent. A disagreement at the top of the ranking changes what is chosen from many menus; one at the bottom changes almost nothing. Weighted Kendall-type metrics on linear orders (Can 2014; Hassanzadeh and Milenkovic 2014) were proposed for this reason, but they live only on linear orders. Nishimura and Ok (2022) instead compare two preferences by the sets of maximal elements they select in every menu. Their domain is the set of acyclic orders, which contains linear orders, partial orders, preorders and the non-transitive acyclic relations that arise as revealed preferences. Their main result, Theorem 3.1, is an axiomatic characterization of this family of semimetrics.
Let be a nonempty finite set of alternatives. For a binary relation on , the asymmetric part is defined by iff and not , and the symmetric part is . is an acyclic order if it is reflexive and there is no cycle of pairwise distinct elements. The set of all acyclic orders is . A generic acyclic order is written , with strict part and symmetric part ; a second one is , with strict part . For , the set of maximal elements is
For a positive (possibly zero) measure on , the -top-difference semimetric is
The axioms use elementary perturbations. For distinct not comparable by , the single addition makes strictly better than . It is when are -incomparable and when , and it is admitted only when the result is acyclic. For , the single deletion is . An acyclic is a one-step perturbation of toward , written , in either of two cases:
An order is in-between and if it is reached from by a finite nonempty chain of one-step perturbations toward .
For distinct , the partial order ranks every alternative other than strictly above both and and makes no other comparisons, and adds . Put . For a semimetric on with values in :
For every nonempty finite and every semimetric on ,
The "if" direction:
The "only if" direction:
Theorem 3.1 gives a complete description of a family of preference distances that is sensitive to where in a ranking two preferences disagree. The weight in Axiom 3 is the number of menus in which a change at is visible. Taking to be the counting measure gives the top-difference semimetric (Theorem 3.2, with the normalization Axiom 2). The paper then uses to compute diameters of classes of orders, to find best transitive approximations of acyclic preferences, and to compare with weighted Kendall metrics. All of these rest on the additivity (Axiom 1) and on the perturbation calculus of §2.3.
The result is proved in the paper; nothing here is open. To our knowledge none of it has been machine-checked. The mission formalizes the definitions and the proof's structure: the reachability theorem for acyclic orders (Theorem 2.2), the menu-wise decomposition (Lemma 3.3), the counting identity behind Axiom 3, and the reconstruction of from . The perturbation calculus and the reachability theorem are reusable for other order-theoretic distances.
The "if" direction rests on Lemma 3.3. The obvious generalization fails: for the literature's notion of betweenness (), Example 2.1 (p. 10) shows that maximal sets can move away from the target, and additivity breaks. Condition (2) is exactly what restores it, so it must be kept.
The "only if" direction has two hard points. First, Theorem 2.2: arbitrary additions and deletions need not lead from to . A deletion may violate (2), and an addition may create a cycle in a non-transitive relation. The perturbations must be chosen in a particular order. Second, the count of the menus affected by a single addition, and its interaction with acyclicity, must be established exactly, since Axiom 3 fixes these constants.
Everything sits in the namespace PrefSemimetric.TopDiff, with one definitions module Model. The conventions are:
X → X → Prop over [Fintype X] [DecidableEq X]. The goal assumes [Nonempty X], as in "nonempty finite set".IsAcyclicOrder. Acyclicity is reflexivity plus irreflexivity of the transitive closure of the strict part, which is equivalent to the page's absence of cycles of distinct elements.IsSemimetric): nonnegative, zero on the diagonal, symmetric, and satisfying the triangle inequality.Nb b R - 1 is natural-number subtraction; it is exact in its clause, because itself is counted.Two trivializing readings are ruled out. "In-between" keeps consistency condition (2); with the literature's weaker betweenness, the "if" direction is false. Axiom 3 keeps its acyclicity provisos, and dropping them would constrain on cyclic relations. A sorry-free sanity file confirms that the axioms are satisfiable (by ), that a genuine one-step perturbation exists, and that display (8) holds for the counting measure on a two-element set.
Not formalized: Theorem 3.2, Lemma 2.1, Examples 3.1–3.2 and §§3.4–6 (weighted Kendall metrics, computational formulas, diameters, best transitive approximations, non-embeddability). Contributions are welcome on any milestone. Theorem 2.2 and Lemma 3.3 are the natural entry points.
Bibliographic data as cited in the paper's reference list (arXiv:2203.04418v1, p. 29).
In linear regression with a budget, an experimenter holds candidate experiments, each described by a vector , and may run only of them. If the experiments in are run and the unknown parameter is estimated by least squares, the covariance of the estimate is proportional to . A-optimal design chooses to minimise the trace of that matrix, which is the mean squared error of the estimator. The criterion is one of the classical optimality criteria of experimental design (Pukelsheim, Optimal Design of Experiments, SIAM 2006) and appears in feature selection, sensor placement and matrix sparsification.
Selecting the best -set exactly is NP-hard (the paper proves this in its Theorem 1.7), so the question is approximation. Avron and Boutsidis (SIAM J. Matrix Anal. Appl. 2013) connected A-optimal design to volume sampling (Deshpande–Rademacher, FOCS 2010), which samples a set with probability proportional to , and obtained the approximation ratio . Nikolov, Singh and Tantipongpipat (arXiv:1802.08318; Mathematics of Operations Research, 2022) reweight volume sampling by a second measure that can depend on a solution of the natural convex relaxation. Their first result, Theorem 1.3, shows that the approximation ratio of this scheme is controlled by a single combinatorial property of , approximate -wise independence. Their later theorems obtain ratios (when ) and (when is large) by exhibiting such measures.
Let be a real matrix and . For , is the submatrix of the columns indexed by , so . The A-optimal design problem is
with the value for sets whose Gram matrix is singular.
The convex relaxation (1)–(3) replaces the indicator of by :
Write for the matrix with columns , , so that , and .
Let () be the subsets of of size exactly (at most) , and a probability measure on them. Proportional volume sampling with measure (Definition 1.1) is the distribution with
The measure is -approximate -wise independent with respect to a feasible (Definition 1.2) if for all with and ,
For a square matrix with eigenvalues , is the -th elementary symmetric polynomial ; .
Algorithm 1 (p. 8) solves the relaxation for , samples , and pads with arbitrary indices to size if it is smaller.
If is an optimal solution of (1)–(3) and is -approximate -wise independent with respect to , then the output of Algorithm 1 satisfies, for every -set ,
so the algorithm is an -approximation in expectation, and some -set has objective at most (the integrality gap is at most ). The constant is a parameter: the goal fixes no value of it, so later constructions of better measures plug into it unchanged.
Theorem 1.3 turns an approximation question about a continuous, spectral objective into a question about the marginals of a distribution on sets: any measure with approximately independent - and -marginals relative to the relaxation's solution yields an approximation algorithm with the same ratio, and simultaneously bounds the integrality gap of the relaxation. The paper's Theorems 1.4 and 1.5 are proved by applying it to hard-core distributions, giving a -approximation for and a -approximation for .
The result is proved in the paper; nothing here is open. To our knowledge none of it has a machine-checked proof. The formalization produces, beyond the theorem itself, a reusable linear-algebra layer that the pinned Mathlib lacks: the Cauchy–Binet formula for Gram matrices, its extension (4) to all elementary symmetric functions of the spectrum, and the identity . These are standard tools for determinantal point processes and volume sampling, and a later formalization of the hard-core constructions (Theorems 1.4, 1.5) would build directly on this mission's goal.
The reduction itself is a short calculation once both sides of (5) are written as ratios of sums over - and -subsets; the difficulty is in the linear algebra that produces those ratios. Identity (4) needs Cauchy–Binet for non-square matrices together with the relation between the coefficients of the characteristic polynomial, its roots and sums of principal minors; none of this is in Mathlib in the required form, and the eigenvalue side requires that the characteristic polynomial of a real symmetric matrix splits over . Applying (4) to every separately and exchanging the order of summation is bookkeeping between index sets of different sizes, which is where informal proofs are quietest. The expectation also has to be handled honestly at sets with singular : they are never sampled, but the paper's displayed equality on p. 9 counts them, so the first display holds only as an inequality.
Everything is over , with index sets Finset (Fin n) and a Matrix (Fin d) (Fin n) ℝ. A probability measure on is a nonnegative function on subsets of with total mass vanishing on sets larger than ; this covers as a special case. is the elementary symmetric function of the real roots of the characteristic polynomial, applied only to symmetric matrices. Lean's matrix inverse is on singular matrices, so every comparison of objectives assumes positive definiteness of the inverted matrix, and OPT is expressed by quantifying over -sets with positive definite Gram matrix rather than by an infimum.
The statements add the following, each disclosed in the item's Formalization Note: (for the natural-number subtraction ); a positive normaliser , which Definition 1.1 presupposes; positive definiteness of , which is what a finite CP means; Definition 1.2 in cross-multiplied form; and "" in place of the printed "" in the first display of p. 9. Theorem 1.3 assumes a suitable only for the optimal , as the remark after the theorem says; this implies the printed form. The padding of Algorithm 1 is an arbitrary map with and on the support of .
The goal is not inequality (5) alone and is not defined as a sum of minors, and the expectation is not defined as the ratio of p. 9; any of those would make milestones true by definition. A sorry-free sanity file shows that all hypotheses of the goal are simultaneously satisfiable (, , , the point mass at , ).
Contributions are welcome at every milestone; the Cauchy–Binet layer (milestones 2 and 3) is reusable well beyond this mission and is the natural place to start.
In a bilevel program, the decision maker chooses an upper-level variable while a second decision must solve a lower-level optimization problem. This structure occurs when a leader anticipates the response of a follower, or when an outer design problem contains an optimization problem as a constraint. A feasible upper-level decision can therefore change the lower-level solution set as its parameters move. Ordinary smooth constrained optimization tests do not directly describe that dependence. Mehlitz and Zemkoho study sufficient optimality conditions for this setting; their Theorem 5.3 gives a second-order condition ensuring a strict local minimum with quantitative growth. Mehlitz and Zemkoho, 2019
Write for the upper-level decision and for the lower-level decision. The upper-level objective is , with componentwise constraints . At each fixed , the lower-level feasible set is , and its solution set is . The bilevel feasible set is . The program minimizes over . All components of are twice continuously differentiable, as assumed on page 2 of the source. Mehlitz and Zemkoho, pp. 1–2
The lower-level value function is . It may be nonsmooth even though the data are smooth. The condition can be expressed using and , giving the value-function reformulation. For the main theorem, is locally Lipschitz near the reference point and has a second-order directional derivative . This derivative measures the second-order change along the curved path , after subtracting the first-order directional term. Mehlitz and Zemkoho, pp. 5, 8–9
At a feasible point , the paper defines a linearization cone by the active and inequalities and the linearized value-function inequality. Its critical cone adds the directions in which the first-order change of is nonpositive. The Abadie constraint qualification, abbreviated ACQ, equates the tangent cone of with its linearization cone at . It is imposed on this lower-level constraint set in the joint space. Mehlitz and Zemkoho, pp. 18–19
The goal is Theorem 5.3. At a feasible , assume ACQ for the lower-level constraint set, local Lipschitz continuity and second-order directional differentiability of , and second-order epi-regularity of . The first-order test requires on . For each nonzero , the minimax program (5.5), formed from the second-order expansions of , active , , and active , must have positive optimal value. The conclusion is
and is a strict local minimizer of the bilevel program. The milestones capture the paper's supporting results: the derivative formula, rules for a finite maximum, the Hadamard derivative and tangent-cone necessary condition, Remark 5.1 under ACQ, and Proposition 2.10 on second-order growth. Mehlitz and Zemkoho, Theorem 5.3, pp. 19–20
The theorem turns tests on first- and second-order directional behavior into a guarantee about actual feasible bilevel decisions near the reference point. The growth estimate is stronger than strict local minimality: it quantifies how the upper-level objective rises with displacement along the feasible set. It applies when the lower-level value function is nonsmooth, provided its directional derivatives and epi-regularity are available. The paper gives special cases in which these hypotheses can be checked more concretely. Mehlitz and Zemkoho, §5, pp. 18–28
The result is proved in the source paper. The open work here is a machine-checked development of its variational definitions, finite-maximum rules, and sufficient-condition argument. The mission includes open Lean statements, not completed proofs. The reusable part is the generic theory of directional derivatives, epi-regularity, and growth on finite-dimensional normed spaces; the bilevel model and cones specialize it to this paper.
Smooth Taylor expansion alone does not handle : an infimum over a parameter-dependent feasible set can be nonsmooth. First-order stationarity on the paper's linearization cone also gives no quadratic increase in directions where the first-order change vanishes. The second-order test must retain the active indices of each constraint and the dependence of on both the first- and second-order directions. ACQ matters because the tangent-cone necessary condition for does not automatically apply to every linearized lower-level direction; Example 5.2 of the paper demonstrates the failure without a constraint qualification. Mehlitz and Zemkoho, pp. 19–20
Lean uses EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), with zero-based Fin indices and uncurried maps on their product. Fréchet derivatives express the paper's gradient and Hessian terms. Generic preliminary results are stated on finite-dimensional real normed spaces, a generalization of the Euclidean statements. The tangent cone uses positive sequences converging to zero. Directional derivatives are named finite limits; epi-regularity uses the eventual inequality for every admissible curved path and every positive error coefficient. The value function takes values in EReal, so an empty feasible set and an unbounded-below lower-level problem are represented by and . A real representative agrees with it on a neighbourhood of , where the local Lipschitz and derivative hypotheses apply. This agreement rules out an unrelated or default-valued value function.
The theorem's growth estimate uses the sum of squared Euclidean norms printed in (5.6), not the product space's sup norm. The positive value of (5.5) is expressed by a uniform positive lower bound over every on its maximum of constraint expressions. The generic maximum rules use a nonempty finite index type. The preliminary formulation of Proposition 2.10 includes local Lipschitz continuity, used in this mission's application and disclosed as an added hypothesis relative to its printed statement. Real-valued functions and finite second-order limits are also explicit scope conventions.
Dividing indivisible goods fairly among agents with different preferences is a central problem of fair division, with uses ranging from inheritance and divorce settlements to course allocation and fair-division services such as Spliddit (Goldman–Procaccia 2014). Envy-freeness cannot always be achieved with indivisible goods (one good, two agents), so relaxations are studied. Envy-freeness up to any good (EFX), introduced by Caragiannis et al. (2019), is widely regarded as the strongest relaxation of this kind whose existence is still unsettled: whether every instance admits a complete EFX allocation is open in general, even for additive valuations.
Timeline.
There are agents and a set of indivisible items. Each agent has a valuation assigning a real number to every bundle . It is normalized, , and monotone, . Nothing else is assumed (general valuations: no additivity, submodularity or cancelability). Write for .
An allocation is a family of pairwise disjoint bundles. It is complete if every item is allocated, and partial otherwise. Agent envies if . Agent EFX envies if for some . The allocation is EFX if no agent EFX envies another, i.e.
The two-valuation setting: there are set functions such that every equals one of them. and denote the agents with valuation and .
The proof works with a vocabulary that the definition file formalizes. The terms are non-degeneracy (distinct bundles have distinct values), minimum preferred sets and , most envious agents, -champions, the champion graph and its Pareto improvable (PI) cycles, semi-EFX allocations, and the partition leximin potential . The potential lists over in increasing order, followed by over in increasing order. means that is lexicographically larger than .
Milestones 2–6 are stated for non-degenerate instances, as in the paper. The goal is not.
The result. Theorem 1 is the most general multi-agent EFX existence theorem in which the number of agents is unbounded and the valuations carry no structure beyond monotonicity. It contains the identical-valuation theorem of Plaut and Roughgarden and the two-additive-valuation theorem as special cases. The potential is the paper's tool for making progress when no Pareto-dominating EFX allocation exists. Pareto domination is the progress measure used for additive and cancelable valuations, and it fails for general ones.
Formalization. The theorem is proved on paper and, to our knowledge, has no machine-checked proof. The remaining work is to formalize the known proof: the perturbation reduction, the champion-graph machinery (minimum preferred sets, most envious agents, PI cycles), the semi-EFX repair, and the case analysis of Theorem 14. The champion-graph layer is shared with the proofs of EFX with charity and of EFX for four agents.
The obvious argument is Pareto improvement: from a partial EFX allocation, hand out an unallocated item and keep everyone at least as well off. For general valuations no Pareto-dominating EFX allocation need exist. The progress step must therefore sometimes make an agent strictly worse off, and that agent may then come to EFX envy others. Theorem 14 allows an agent of to lose value while improving the -block of . The paper repairs the resulting EFX envy, which is confined to (semi-EFX), by trimming bundles. Keeping track of which agents may envy which bundles through several reallocations is the central difficulty. The champion-graph statements are also delicate: minimum preferred sets are not unique, and the cardinality parameter takes the value .
Agents are Fin n and items Fin m, both 0-indexed. Valuations are maps Fin n → Finset (Fin m) → ℝ, assumed normalized and monotone (IsNormalized, IsMonotoneVal). Allocations are maps Fin n → Finset (Fin m) with pairwise disjoint values (IsPartialAllocation). Completeness is pool X = ∅. EFX is IsEFX, from the published definition file LittleCharity.EFX.Setting. The two valuation classes are a finset A of agents with v i = va on A and v i = vb off A; in the goal they are ∀ i, v i = va ∨ v i = vb. takes values in ℕ∞. PI cycles are indexed by Fin k: distinct vertices, edge labels Option (Fin m), unallocated champion labels, labels pairwise disjoint. is a pair of sorted lists, and is the strict List.Lex (· < ·).
Disclosed readings:
The goal assumes neither additivity nor non-degeneracy. Its only added hypothesis is , which is necessary. Every item must be allocated: the empty allocation is always EFX, so a goal without completeness would be trivial. Contributions are welcome at every level: proofs of the milestones, the champion-graph library, and the termination argument for strict lexicographic orders on finite sets.
Deferred acceptance and top trading cycles are strategy-proof: submitting one's true preference ranking is optimal whatever the other participants do (Roth, 1982). School-choice and residency-match systems around the world use them for this reason. Yet laboratory and field data show participants misreporting systematically, most often by leaving popular options out of their list or by ranking options with high admission chances above options they prefer (Chen and Sönmez, 2006; Hassidim, Marciano, Romm and Shorrer, 2017; Chen and Pereyra, 2019; survey by Hakimov and Kübler, 2021). One line of explanation treats these reports as mistakes; another looks for preferences under which they are optimal, such as expectation-based loss aversion (Dreyfuss, Heffetz and Rabin, 2022).
V. Meisner's paper Report-dependent utility and strategy-proofness proposes report-dependent utility: on top of the value of the option she is assigned, a participant cares about where that option sits in the list she submitted, enjoying acceptance by her reported top choice and disliking acceptance only at the bottom. The paper's Proposition 2 says exactly when truth-telling survives such preferences, for every strength of the report-dependent component. This mission formalizes Proposition 2 and the steps of its proof.
A participant ranks options, labelled . She gets a report-independent payoff from being matched with option , and the options are labelled so that
A rank-ordered list (ROL) is a bijection from options to ranks ; its -th ranked option is . The true ROL ranks options by . She also receives a report-dependent payoff when matched with her -th ranked option, where is decreasing.
The other participants' reports are fixed. An option is attainable () if the participant would be matched with it by ranking it first. The attainability distribution is a probability distribution on the states ; the may be correlated in any way. In a strategy-proof mechanism she is matched with the highest-ranked attainable option of her list, so her match probability at rank under is
and her expected payoff is
Under the truth these are and . The true ROL is optimal if for every .
In Lean, options and ranks are Fin n, a ROL is Rt : Equiv.Perm (Fin n) (option ↦ rank), the truth is 1, is a function (Fin n → Bool) → ℝ, and , are matchProb P Rt r, payoff v ρ P Rt.
For every non-truthful ROL : for all decreasing if and only if
Hence the true ROL is optimal for every decreasing if and only if (3) holds against all non-truthful ROLs.
Proposition 2 gives a testable condition, stated only in terms of beliefs about admission, under which no report-dependent taste of any size can break truth-telling: no alternative list may raise the probability of being matched with one of the top ranked options, for any . Conversely, when an alternative list does raise such a probability, as ranking a safe option first does, a strong enough report-dependent payoff makes that list strictly better than the truth even though the mechanism is strategy-proof. The paper uses this to separate settings in which truthful reports are predicted from those in which self-selection is predicted, and contrasts it with Proposition 1, under which every list is optimal for some beliefs.
The result is proved in the paper; to our knowledge it has no machine-checked proof. The mission provides one, together with a reusable finite model of matching under correlated attainability (match probabilities of the highest-ranked attainable option, the expected payoff (1)) and the stochastic-dominance property of the truthful lottery, which other results about rank-ordered lists in strategy-proof mechanisms can import.
The two directions are elementary in spirit but need care. The "only if" direction in the paper takes a limit of decreasing functions ; a formal proof has to exhibit an actual strictly decreasing and control the report-independent term uniformly. The "if" direction rests on two facts the paper asserts briefly: that the true lottery stochastically dominates every other (which is a statement about the match rule under arbitrarily correlated attainability, not an assumption), and a summation-by-parts rewriting of that uses the equality of total match probabilities across lists. The paper's inequalities "" and the final "" are strict as printed but hold only weakly, so the formal statements use .
Fin n, 0-indexed (Lean index is the page's ). A ROL is Equiv.Perm (Fin n) mapping options to ranks; the -th ranked option is R.symm r; the truth is 1. States are Fin n → Bool; is a real weight function and IsAttainabilityDist P says it is nonnegative with total mass one. Probabilities are finite sums; there is no measure theory.matchProb P R r is the weight of the states in which the rank-r option is attainable and every option ranked above it is not: the highest-ranked attainable option is matched, as on p. 5. The distribution does not depend on the submitted list.StrictAnti ρ, the model's standing assumption; the equivalence also holds for weakly decreasing . The order is a hypothesis (Antitone v). The normalizations and are not imposed: all lists have the same total match probability, so adding a constant to or leaves unchanged, and the statement with them is equivalent. "Non-truthful" is Rt ≠ 1. Condition (3) is Condition3 P Rt, with rbar : Fin n the page's shifted by one and Iic rbar the ranks .Fin n and Fin n → Bool, permutations of Fin n and Mathlib's summation by parts. Proofs of any milestone are welcome, as are alternative proofs of the goal that bypass the decomposition.In many emerging economies, smallholder farmers decide each season how much of their land to give to an export crop, sold through a local processor at a price linked to the world market, and how much to keep for a traditional alternative crop. Yields are uncertain and often correlated across neighbouring regions because they share weather. Governments and development agencies frequently protect farmers with a minimum guaranteed price: no processor may pay less than per unit of harvest. Whether such a floor encourages too little, enough, or too much planting relative to the processing capacity of the region is a policy question with direct consequences for farm income and processor utilization.
Li, Kouvelis and Dada (SSRN 3531158; published in Manufacturing & Service Operations Management 26(2), 2024, doi:10.1287/msom.2022.0076) model this as a two-stage game between two farmers and two capacity-constrained processors, and characterize the land-allocation equilibria in closed form for all-or-nothing yields. This mission formalizes that characterization, together with the second-stage pricing results it is built on.
There are two regions , each with one farmer and one processor. The processed crop sells at the world price . Processor has unit processing cost and capacity , with , and the minimum guaranteed price satisfies .
Second stage. Farmer has planted units of land and harvests , where is the random yield. Both farmers sell first to the winning processor (Processor 1 on ties); a winner who cannot absorb the whole harvest first takes the harvest of its own region's farmer, and the residual goes to the losing processor up to its capacity (Theorem 1 of the paper). Processor 's profit is its margin times the amount it procures. Its willingness to pay is the highest price at which winning at is no worse than losing at (conditions (7)–(8)). The processors then settle as in a second-price auction (Theorem 3): if , Processor 1 wins and the final prices are ; otherwise Processor 2 wins and they are . Farmer 's revenue is the sum of her sales to the two processors at the final prices.
First stage. Farmer 's expected profit is
where is the per-unit cost of export-crop land, including the forgone alternative crop, and is a constant. An equilibrium is a pair in which each maximizes given the other farmer's choice.
All-or-nothing (AON) yields. Each takes the value or . In the symmetric IID chain the processors are identical (, ), the farmers are identical (, ), and the yields are independent with .
In the symmetric IID chain with , and the participation condition :
The theorem shows that the price floor is the decisive policy lever. A low floor leaves farmers with thin margins and produces under-planting together with a whole continuum of equilibria, so total production is pinned down but its split between regions is not. Intermediate floors coordinate both farmers on filling exactly the processing capacity. A high floor makes planting so attractive that both farmers plant enough to fill both processors on their own, and part of the harvest goes unsold whenever both crops succeed. These regimes underlie the paper's later comparisons of ownership structures and yield correlations (§4–§5).
The result is proved on paper; it has no machine-checked proof. Formalization adds a precise model of a second-stage protocol that is described partly in prose, and it pins down the boundary cases. Checking the printed statement already corrected three points: part 2 of Theorem 6 is false as printed, the participation condition must be strict for part 1, and the threshold of part 4 must be strict.
The profits are piecewise linear in , but the pieces come from nested and operations in the allocation rule, multiplied by a WTP that is itself a ratio of such terms. Each farmer's best response is therefore discontinuous and has to be found region by region. The two farmers are not symmetric even in the symmetric chain, because Processor 1 wins every tie and so farmer 1's harvest is served first. Equilibrium claims are global: "unique equilibrium" requires excluding every other point of , including allocations above and corners where a farmer plants nothing. The WTPs are defined as suprema, so identifying them with (9)–(10) is a separate optimization over all competing prices.
All quantities are real numbers. The model is one definition, AgriChain.LandAlloc.Model: the chain, the allocation of Theorem 1 indexed by the winning processor, the profits (5)–(6), the WTP sets defined by (7)–(8) and the WTPs as their suprema, the final prices of Theorem 3 with ties going to Processor 1, the revenues (11)–(12), AON yield laws, the expected profits (13)–(14) as finite sums over the four yield outcomes, and the equilibrium. The equilibrium is the published generic pure-Nash predicate CarbonDoubleCount.Planner.IsPureNash, with feasible sets . and are real parameters, as in the paper from (13) on.
Hypotheses added to the goal: , , and (the thresholds divide by , and , and the bound needs ); (the over-production equilibrium plants ); the participation condition of p. 19, made strict; and part 4's threshold, made strict. "Unique equilibrium" is an "if and only if", asserting existence. Part 2 of Theorem 6 is not posed: at , , , its hypotheses hold, but the unique equilibrium is , whose total is below . Theorem 5 (p. 18) and part 2 of Theorem 4 are not posed either.
The goal is about the equilibria of the full model. Defining the WTPs by (9)–(10), defining by the two-term AON form, or stating Theorem 6 for a hand-simplified symmetric profit would make the milestones definitional and is ruled out. Contributions are welcome on every milestone. The WTP computation and the AON reduction are reusable for the paper's other correlation structures (§4–§5).
A repair supplier can invest in capacity before a service contract begins, while the customer may know more about how often her equipment fails. The supplier must choose both an incentive to maintain uptime and a menu that gives customers reason to reveal their failure rates. Li, Mishra, and Netessine study this interaction for maintenance, repair, and overhaul services. Their model compares a price per repair with a performance-based contract (PBC), under which the supplier is paid for the product's uptime. The latter ties revenue to the outcome the customer values. The paper asks when that arrangement can preserve the full-information outcome despite asymmetric information about product reliability. Li, Mishra, and Netessine, SSRN author version, §§1, 3, 5.
The specific result targeted here is Proposition 5(i). The two customer types differ both in failure rate and in the value of their outside options. This creates countervailing incentives: the customer with the less reliable product need not always be the one seeking a better contract. The paper identifies a range of outside-option ratios in which a single separating PBC menu gives each type the same contract she would receive if the supplier knew her type. Li, Mishra, and Netessine, Proposition 5(i), p. 18.
A contract period has length one. A product has failures at a rate , and the supplier sets a repair rate by investing in capacity. Each repair requires a random lead time. The product's uptime is one minus total downtime. The paper's expected-uptime expression is . It uses this expression to turn the stochastic model into the closed-form payoffs of its supplementary equation (B.39). Li, Mishra, and Netessine, §3, pp. 7–10, and supplement (B.39), p. 9.
There are two types, and , with . The probability of the low-failure type is . Type can decline the contract and obtain her reservation payoff ; the setting has . The supplier receives per unit uptime from a customer choosing contract and incurs a capacity cost plus expected material cost . The customer's payoff, evaluated at her actual failure rate , is , where is revenue per unit uptime. The supplier's corresponding payoff is . Li, Mishra, and Netessine, §§3–4 and supplement (B.39).
A menu contains one positive-price, positive-rate contract for each type. Individual rationality (IR) requires that each type's payoff from her designated contract reach her reservation payoff. Incentive compatibility (IC) requires that neither type prefer the other contract. In problem (9), the supplier maximizes her prior-weighted payoff over all menus satisfying both IR and both IC constraints. Under full information, the two types can be optimized separately; Proposition 1(ii) gives the first-best PBC repair rate and the price . Li, Mishra, and Netessine, Proposition 1, p. 12; problem (9), p. 18.
The goal formalizes Proposition 5(i). Define the first-best menu by offering to type and to type . Condition (10) is
When this condition holds and both first-best prices are positive, the first-best menu is feasible for problem (9) and achieves at least the supplier payoff of every feasible menu. Both IR constraints bind, so each customer's information rent is zero; the two repair rates differ, so the menu separates the types. Li, Mishra, and Netessine, Proposition 5(i), p. 18.
The milestones follow the paper's stated calculations: the binding-IR price and reduced objective from (B.6)–(B.7); the PBC part of Proposition 1(ii)–(iii); the two IC slack formulas (B.41) and (B.42); and the first-best payoff bound used at the end of the proof of Proposition 5(i). The joint-profit benchmark is . Li, Mishra, and Netessine, supplement pp. 3–4 and 9.
The result identifies a parameter region in which screening does not reduce productive efficiency or leave an information rent to either customer type. The supplier can offer the same repair capacities and prices as in the full-information problem while satisfying each type's participation and truthful-choice requirements. This makes the full-information outcome a concrete benchmark for the other regions of Proposition 5, where one or more constraints bind differently. Li, Mishra, and Netessine, Proposition 5, pp. 18–19.
The mathematical result is proved in the paper. This mission asks for machine-checked proofs of the model identities and the first region of its screening theorem. The reusable artifacts are the explicit PBC menu, the four feasibility constraints, the separation between supplier and joint profit, and a uniform upper bound over every feasible menu. No existing platform theorem found in the local prior-art index has this paper's contract space and payoffs.
The first-best solution optimizes a contract separately for each known type. With private failure rates, a customer can choose the contract intended for the other type; solving the two full-information problems alone therefore does not establish a feasible screening menu. The signs of both IC slacks must agree with the ratio interval in condition (10), and every denominator in the ratio and in the first-best prices must be nonzero. Feasibility still is not enough for the conclusion: optimality compares the candidate with all positive-price, positive-rate menus satisfying the four constraints, including menus with slack IR constraints. Li, Mishra, and Netessine, problem (9), p. 18, and supplement (B.39)–(B.43), p. 9.
The Lean development uses real-valued prices, rates, costs, payoffs, and prior weights. It represents expected uptime and expected payoffs by the paper's closed form (B.39), ; it does not encode the underlying Poisson failure process or random repair times in this first mission. The model keeps a separate customer payoff, supplier payoff, and joint-profit function, so is never confused with . The menu's feasibility predicate contains exactly the four constraints of problem (9), plus the strict positivity of both prices and both repair rates written under its maximization sign. The objective uses the prior weights and . Li, Mishra, and Netessine, §§3–5.2 and supplement (B.39).
The standing predicate makes the parameter domain explicit: , , , , and . The order of the two outside options is stated in the paper's setting; is needed for the ratio in (10). The goal also assumes , because a first-best menu with a nonpositive price is not in problem (9)'s admissible set. The algebraic IC milestones explicitly exclude zero denominators, and the goal's ratio condition with the standing order rules out its degenerate denominator cases.
The candidate's optimality is stated against every feasible menu. Restricting competitors to first-best-form or binding-IR menus would make the main theorem weaker. Useful contributions include proofs of the source's algebraic identities, the first-best profit properties, the global upper bound, and Proposition 5(i) itself. The omitted stochastic expected-uptime identity and the remaining cases of Proposition 5 are separate formalization work; the present goal uses the closed form printed by the paper.
When a bank run forces asset sales, the sale price can reflect buyers’ beliefs about the condition of other banks as well as the assets being sold. In the two-bank model of Li and Ma, observing two runs makes buyers more pessimistic about the aggregate state than observing one. That change in beliefs lowers the market price precisely when both banks need liquidity. The paper studies whether a regulator can commit in advance to a purchase price that reduces joint failures while recovering its expected expenditure. Its Proposition 3 gives a specific break-even policy in a limiting version of the model.
The paper proves the policy result in its accepted manuscript, dated 28 October 2021, and was published in Management Science in 2022. The result is mathematically known. The work here is to state its price, payoff, and risk claims as machine-checkable theorems with the paper’s parameter restrictions visible.
There are two banks and two aggregate states, good and bad . In state , each bank’s asset portfolio produces a cash flow uniformly distributed between a state-dependent lower bound and a common upper bound . The good state has the higher lower bound: . Conditional on the state, the banks’ cash flows are independent. The prior probability of is ; the probability of is . These are the primitives of §2.1 of Li and Ma.
Each bank finances a unit portfolio using equity , retail deposits , and positive wholesale debt . A wholesale creditor who withdraws early receives a gross factor , while one who waits receives , where and . The debt obligations used throughout are
Assumptions (1)–(3) say in both states, , and . The candidate market-price interval begins at and ends below . The upper-cash-flow condition in footnote 29 is . It keeps the uniform probabilities within their intended range on this interval. Footnotes 25 and 27 explain why the interval is nonempty and ; see pp. 13 and 15 of the accepted manuscript.
Buyers who observe bank runs use a posterior probability of state , with . Their expected profit from buying one unit at price is . A market break-even price solves in . The two prices differ because the number of runs changes buyers’ posterior. In the paper’s regime, a committed regulator price gives the critical cash flow
The regulator’s expected payoff averages purchase gains over the two states and the possibilities of one or two runs, exactly as in equation (22). The systemic-failure probability is the prior-weighted probability that both banks’ cash flows fall below , using the closed uniform formula on p. 26 of Li and Ma.
The milestone path establishes the existence of the two market prices, their ordering, the payoff identity (23), the signs of at those prices, and the monotonicity of payoff and systemic risk. The main target is Proposition 3: a unique regulator price lies strictly between the market prices,
Both and decrease strictly as the committed price rises through . Among all prices in the regulator’s program (20)–(21),
the price minimizes and satisfies . This is the limit interpretation of the comparison printed at the end of Proposition 3.
The theorem identifies a precommitted price at which the regulator breaks even across possible numbers of runs, while a buyer who acts after observing the run count must break even conditional on that count. The resulting interval between and is where liquidity support can lower joint failures without an expected transfer. The program also excludes saving banks whose cash flow is below ; the policy result meets that solvency restriction.
A checked formalization would make the paper’s assumptions and the links among posterior prices, regulator payoff, and systemic risk explicit. Proposition 3 is proved in the paper; its Lean proof and the supporting results in this mission remain to be completed. The definitions of the uniform two-state model, posterior weights, and payoff sums can support later formal work on related liquidity policies, while the paper-specific financial parameters remain tied to this model.
The regulator cannot choose a price from the simple interval between two fixed asset values. Each price changes the cash-flow threshold at which runs lead to failure, which changes the posterior beliefs used in and the probabilities weighting . A direct comparison of with either market price therefore does not determine the sign of the regulator’s total payoff. The proof must control both market-contingent profits and their state and run-count weights before the break-even price and its risk effect can be certified.
Lean represents the aggregate state by a two-constructor type and the primitive bank data by one parameter structure. The standing predicate includes assumptions (1)–(3), , , , , footnote 29, and positive wholesale debt. The last condition makes the model’s financing convention explicit. The formulation uses the paper’s closed forms in the limit; it does not encode creditor signals or the full global game.
Uniform probabilities are not clipped, because the relevant threshold lies inside the cash-flow support on the stated price interval. The market prices are characterized by their break-even equations rather than chosen from a prior existence assumption: a milestone establishes their existence. is defined by equation (22), not the later identity (23), and the policy goal asserts existence and uniqueness of its zero. The feasible set is exactly program (20)–(21). Strict decrease means strict antitonicity on . Lean’s real division is total at zero, so the critical-threshold formula has junk values at singular inputs; every claim uses the economically valid interval. Useful contributions include proofs of the market-price milestones, the payoff identity and signs, and the two monotonicity results.
Online retailers and service providers quote a promised delivery time and are judged on how often they meet it. Platforms increasingly publish delivery-performance information, such as on-time ratings or conformance scores, so that consumers can weigh a quoted time against the firm's record. Producing accurate information is costly: the firm must track deliveries, audit ratings and present them clearly. Whether a firm should pay for precise information, or let consumers infer its reliability from noisy signals, is a question for operations management (capacity, lead-time quotation) and for marketing (pricing, information disclosure) at once.
Leng, Becerril-Arreola, Parlar and Ferguson (MSOM 2024; the mission follows the authors' preprint of April 2nd, 2023) model a firm that jointly sets a price, a promised delivery time and an effort toward the quality of its conformance information, facing consumers who care about all three. Their central analytical result, Theorem 1, says the firm should never invest partially: the optimal effort is either none or full.
The model joins two lines of work. The first is joint price and delivery-time decisions with congestion, as in So (2000), Liu, Parlar and Zhu (2007) and Boyaci and Ray (2006), where delivery reliability enters demand. The second is logit demand from discrete-choice theory (Anderson, de Palma and Thisse 1992), where the scale parameter measures how dispersed consumers' valuations are.
A firm serves consumers at service rate . It sets a price , a promised delivery time , and an information-quality effort . The market has size . Each consumer compares the firm with an outside option of deterministic utility .
If consumers arrive at rate , the firm operates as an M/M/1 queue, and an order is delivered within the promised time with probability
The deterministic utility of buying is
where is the base value, and are the sensitivities to the conformance score and to the promised time, and scales the score. Effort narrows the dispersion of consumers' inferences: the utility shock has scale
decreasing from at to at .
The demand rate is the logit share times the market size (eqs. (8)–(9)):
Since depends on through , this is a fixed-point equation in . The firm earns
with unit cost and unit effort cost . A plan is feasible when , and . The optimal profit is the supremum of over feasible plans, and are the demand and utility at the optimal plan, and the gap
measures by how much Lemma 2's condition (19) holds. With the largest attainable market share (eq. (10)), the capacity condition (16) is .
Let . If
then is strictly decreasing on and is the unique optimum. Otherwise strictly decreases and then strictly increases, with the turn at some . In both cases
Three supporting items have no counterpart in the paper. They state that the demand fixed point is well posed, that is continuous on , and the envelope identity .
Theorem 1 is a bang-bang result. A firm choosing how much to spend on delivery-performance information should consider only two options, no effort and full effort, and condition (23) gives a closed-form test for when no effort is optimal. The paper's sensitivity results (Corollaries 1–4) and its numerical study are all built on this reduction, since they compare the two endpoint regimes using the closed forms in Table 1.
The result has an analytical proof in the paper's online appendix, but no machine-checked proof. The formalization adds a precise statement of the model's well-posedness: the demand is a fixed point, and the optimal plan exists and is unique. It also makes the comparative statics explicit. Parts of Lemma 2 as printed are false, namely the directions of and in item 1 and of and in item 2, and the mission states only the parts that hold. A complete development would certify which of the paper's conclusions survive and by which argument.
The optimal profit is the value of a two-dimensional optimization whose objective is defined through an implicit equation, since demand appears on both sides of the logit formula. Differentiating in requires an envelope argument over a constrained problem. That in turn requires knowing that the optimum is interior, unique and a smooth function of , and that the queue constraint does not bind.
The single-crossing step is the delicate one. The paper reaches it through a derivative of with respect to (eqs. (30)–(34)) whose sign claims are partly wrong. The tempting shortcut, to read the sign of off the sign of , is unsound: when (19) holds, can rise while falls.
Everything is real-valued and lives in the namespace DeliveryDisclosure.InfoEffort. A structure Params holds , and the predicate Standing bundles the standing assumptions. The paper writes but divides by them, so Standing requires , together with and condition (16) for every .
Real.sigmoid gives the logit share.is defined as a supremum over all feasible plans and uses at the optimum, which rules out a trivializing formalization: cannot be replaced by Table 1's closed forms, by profit at a fixed plan, or by a demand with the conformance frozen. Lemma 1's corner case (item 1), Claim 1, Remarks 1–5, Table 1 and Corollaries 1–4 are not formalized.
A complete development needs implicit differentiation of a fixed point, an envelope theorem for a two-variable constrained maximization, and existence of maximizers on a non-compact feasible set. These ingredients apply to other congestion-pricing and logit-demand models. Contributions toward any milestone are welcome, as are proofs of the supporting items.
A firm can have valuable operations yet fail when a temporary cash shortfall leaves it unable to pay its bills. Cash reserves protect the firm, but holding them is costly. In Lee and Rivera’s study, the manager also doubts the probability model for future shocks. The manager evaluates a policy under the least favorable model within a prescribed set of plausible models. This makes the composition of pessimism a decision linked to the firm’s cash position. The paper’s central qualitative claim is that adverse beliefs respond to recent shocks in a way resembling extrapolation bias: a recent shock changes the manager’s assessment of future shocks of the same type.
The result belongs to the paper’s 2019 working version, Extrapolation Bias and Dynamic Liquidity Management. The later Management Science article has a different title. The theorem and equation numbers here refer to the working version, especially §2, §3.3, §4.1 and Appendix A.
The firm has a positive size δ and cash reserves M. Its cash ratio is m=M/δ. The manager chooses an investment rate i, which raises expected size growth but incurs an expenditure g(i)=i+θi²/2. The size process has a permanent shock with volatility σδ; operating cash flow has an independent temporary shock with volatility σY. The manager discounts at rate r. Cash earns r−λ, so λ is its carry cost. At cash exhaustion the firm either issues equity, paying proportional and fixed costs ρ₁ and ρ₀, or liquidates for a fraction ω of the ambiguity-only benchmark value δqᴬ. These objects and their cash-management interpretation follow the working paper’s model and HJB equations.
The manager allows drift changes h=(hᴾ,hᵀ) in an ambiguity ellipse,
The superscripts P and T mean permanent and temporary. The two radii κP and κT limit how much each drift can be distorted. A distortion h changes expected size growth by σδhᴾ and expected cash flow by σYhᵀ. The manager chooses i against the least favorable h. On the ellipse boundary, the model writes hᴾ=−κP cos φ and hᵀ=−κT sin φ for an angle φ in [0,2π].
The paper uses a scaled value function F: firm value at size δ and cash M is δF(M/δ). In the no-payout region 0≤m≤m*, F satisfies the max-min Hamilton–Jacobi–Bellman equation (25), with payout boundary m*. The conditions at m=0 compare refinancing with liquidation, and the value is linear in cash above m*. The ambiguity-only benchmark qᴬ is determined by the paper’s equations (36)–(38). For an increasing concave F, the worst-case angle and distortions are defined by (26)–(27).
For every cash ratio in the no-payout region, the angle from (26) is the unique minimizer of the HJB expression among admissible angles. Its associated worst-case distortions satisfy four shock-response inequalities:
Here the first subscript names the belief component and the second names the shock. The four coefficients are the derivatives in the display on p. 21, multiplied by the corresponding shock loading of the cash ratio. When F″(m)<0, the temporary-shock inequalities are strict. The permanent-shock inequalities are strict when also m>0. This states the paper’s §4.1 claim at the boundaries where its printed strict wording would otherwise fail.
The attack path follows four statements in the working paper: Lemma 4 equates minimization over the filled ellipse with minimization over its angle-parametrized boundary; Proposition 3 (19) gives the investment and belief-allocation conditions for the two-state HJB; equations (26)–(27) give their scaled counterparts; and §4.1 describes how beliefs change as the cash ratio rises. The milestone list retains the printed passages verbatim and identifies the necessary corrections in its titles.
The result identifies which adverse cash-flow model the manager uses at a given cash position. With little cash, temporary losses can force costly financing or liquidation, and the adverse model weighs them more heavily. With more cash, the adverse model shifts toward permanent shocks to firm size. The sign pattern translates that change in beliefs into responses to realized shocks. It supplies a precise meaning for the paper’s claim of endogenous extrapolation bias within this cash-management model.
The paper gives analytical HJB conditions and illustrates the time-varying beliefs in Figure 4.1. This mission asks for Lean proofs of the qualitative allocation and sensitivity statements for the paper’s stated variational system. The local formalization records three corrections to the working paper’s formulas and prose, so solvers have a single explicit target rather than relying on incompatible printed expressions.
The obvious appeal to worst-case beliefs does not by itself establish which point of the ellipse minimizes the HJB expression, whether that point is unique, or whether its angle remains in the required quadrant. The HJB also mixes investment and belief allocation, while the target concerns derivatives of the belief allocation with respect to the cash ratio. Finally, the printed strict signs fail at m=0 and at a smooth payout boundary where F″(m*)=0. The theorem must account for both endpoints while preserving the paper’s interior claim.
Lean represents parameters in a structure, the ellipse as a subset of ℝ×ℝ, and F as a global C² real function restricted to nonnegative cash. The scaled solution predicate includes monotonicity, concavity, the attained max-min equation (25), and the boundary conditions (28)–(31). The HJB angle interval is the closed [0,2π] of (25). No real supremum of an empty or unbounded set is used. The benchmark predicate records (36)–(38) and the positive transversality gap r−µ−iᴬ.
The working paper has three relevant slips. Lemma 4’s h-form HJB omits the volatility multipliers present in (11)–(12), so the formal statement restores them and uses the paper’s γ=2 restriction. Proposition 3 (19) prints an extra δ in the investment condition; the formal statement uses the condition implied by (18). The last sentence of §4.1 p. 20 reverses the belief monotonicity directions implied by the preceding prose and the p. 21 sensitivity display; the formal statement follows the latter. Strictly positive κP, κT, σY, ω and qᴬ specify the nondegenerate regime in which the arctangent formula and liquidation value carry their intended meaning.
The scaled solution predicate prevents an arbitrary concave function from replacing the paper’s value function. The target requires the displayed angle to be the actual unique minimizer of (25), and its divisions have positive denominators under the model assumptions. Reusable work includes the ellipse minimization and real-analysis facts behind the angle’s monotonicity. Contributions proving these milestones or the final sensitivity theorem are within scope.
Humanitarian organizations (HOs) have long helped refugees with in-kind assistance: food, hygiene and shelter items bought at wholesale cost and handed out. Cash assistance, money that refugees spend at local stores, has grown quickly. In 2014 it was 6% of the $25 billion of humanitarian assistance worldwide; by 2019, cash and vouchers were 18% (High Level Panel on Humanitarian Cash Transfers 2015; Jódar Vidal et al. 2020, both as cited by Kotsi, Wu and Pedraza-Martinez). Cash lets refugees buy what they need and brings revenue to the host community. It also creates demand that a local retailer with market power can exploit: field reports from Swaziland and Uganda describe price increases after cash programmes began, and UNHCR advises in-kind assistance "where increased demand on markets will cause inflation".
Kotsi, Wu and Pedraza-Martinez (MSOM 24(6), 2022) model this as a game between an HO and a monopolist retailer. Without intervention the retailer answers cash assistance by raising its price above the monopoly price it charged before the refugees arrived. That hurts local residents and reduces the quantity of goods refugees receive. The paper then designs interventions run by an HO-government partnership. One of them is price-dependent cash assistance (PDCA): the HO announces how much cash it will give as a function of the retailer's prices. This mission formalizes the paper's result that a correctly designed PDCA schedule makes a chosen target price the retailer's own optimal choice.
An HO has budget . It gives a fraction to the refugees as cash and spends the rest on goods bought at unit cost . A monopolist retailer buys at the same unit cost and sets the retail price.
In the symmetric-goods case every good has the same cost and price , and is the local residents' aggregate demand. Refugees spend their cash in full, buying units. The retailer's profits from refugees and from residents are
and its total profit is . Assumption 2 of the paper: is continuously differentiable, on where , and is unimodal with unique maximizer . The pre-arrival maximum profit is .
The HO-government partnership picks a target . It is feasible if the retailer earns at least its old profit, , and residents are no worse off, which the paper writes as . The symmetric PDCA scheme (equation (27)) pays the cash fraction
when the retailer sets price . The retailer then earns .
In the general -good model, prices are vectors, is the refugees' demand under cash fraction and in-kind bundle , and the PDCA policy of Proposition 4 is a clipped linear function of a weighted price index .
Assume Assumption 2, concave on , and a feasible target with and . Then , and
with the unique maximizer when (§6.3, p. 22).
The goal is the paper's positive design result. Without a policy, the retailer's best response to cash assistance is a price above (Proposition 1 of the paper). The PDCA scheme reverses this incentive with no price regulation: the government only monitors that announced prices are kept. Every feasible target, including the one that maximizes social welfare, can be implemented this way, and the retailer still earns at least . Proposition 4 gives the general -good recipe: weight each price by the retailer's marginal profit, and let the cash fraction fall with the price index at the rate that offsets the marginal gain from raising prices.
The results are proved in the paper, which argues the symmetric case in two paragraphs. No machine-checked version exists. Formalizing them makes several conditions explicit that the text leaves implicit. The slope of the scheme must be non-positive, which needs . The clipped branches must be compared with the unclipped concave profit. The general proposition is established at the level of the first-order condition.
The obvious argument says that the PDCA profit has a critical point at by construction, so is optimal. This fails twice. First, the schedule is clipped to , so the profit is only piecewise smooth and is not globally concave: on the branch the profit need not be dominated by a concave function through unless the comparison is made explicitly. Second, the middle branch is concave only if the schedule's intercept is non-negative, which depends on the sign of and hence on and Assumption 2. The uniqueness clause needs strict versions of each comparison and fails without .
All quantities are real. Prices range over ; the scheme, the profits and the slope are explicit defs transcribing (18) and (27), with as Lean's deriv, used only at points where Assumption 2 makes differentiable. is the value , not a supremum. Assumption 2 is read on : continuously differentiable there, on , and nondecreasing on , nonincreasing on , with its unique maximizer. " concave" is read on . Feasibility uses the retailer clause and ; the refugee-utility clause of (26) is dropped, which strengthens the goal. In the -good model, and are abstract functions, partial derivatives are Fréchet derivatives on unit vectors, and Proposition 4 assumes , and differentiability at the target, and concludes the first-order condition (A.13) of its proof; the mission does not state the -good global optimality (16).
The goal must not be replaced by the first-order condition alone (milestone 3) or by an assumption that the PDCA profit is concave: it quantifies over every price , with the clip of (27) in place.
The development needs only one-variable calculus and convexity from Mathlib. The hypotheses are satisfiable: for , , , , , , the target profit exceeds . Proofs of any milestone, and statements of the paper's Propositions 1, 3 and 5 for the same model, are welcome.
Biopharmaceuticals such as vaccines and therapeutic proteins are produced by living cells grown in a bioreactor. In a batch fermentation the cells multiply until the medium is depleted and the culture enters a stationary phase, after which the batch is harvested. A bleed–feed operation removes part of the culture and replaces it with fresh medium, restarting exponential growth in the same bioreactor and saving the cost of cleaning, sterilising and setting up a new batch. Regulators cap the number of bleed–feeds per batch. The operational question is when to bleed–feed: too early forgoes biomass that would have grown, too late risks the culture entering the stationary phase first and the opportunity being lost.
Koca, Martagan, Adan, Maillart and van Ravenstein model this decision as a finite-horizon Markov decision process and show that, under conditions on the growth and risk profile, the optimal policy is described by three thresholds (SSRN 3659907; published in Manufacturing & Service Operations Management, doi:10.1287/msom.2022.1163). The paper reports an implementation at MSD (Merck), and threshold rules of this form are what can be written into production plans.
The state of a batch is :
Starting from biomass , the biomass at age is , and continuing for one period earns the increment . The culture stays in exponential growth with probability , where the rate is zero up to a critical biomass and strictly increasing beyond it; otherwise it enters the stationary phase and earns nothing more. The critical age is the least age at which .
The value function is defined by the optimality equations: and, for ,
with and . Bleed–feed is optimal in when and ; continuing is optimal when .
Assume Condition (4), for ; Condition (5), for and ; and Assumption 1, that bleed–feed is optimal at age whenever . Then there are thresholds , and with
In the paper's order: the risk profile facts of §3 (p. 12); Remark 1 and Propositions 1–2, giving monotonicity in the age and Theorem 1; Propositions 3–4, giving monotonicity in the growth rate and Theorem 2; Propositions 5–6, giving monotonicity in the count and Theorem 3. Theorems 1, 2 and 3 are the three clauses of the goal, each under its own hypotheses (Theorem 3 needs none).
The result turns a dynamic program over a continuous state into three monotone rules, each with a direct operational reading: bleed–feed older cultures, faster-growing cultures, and cultures early in their bleed–feed budget. The thresholds are monotone in the remaining coordinates (Corollary 2 of the paper), which is what makes the policy tabulable for a production plan.
The paper proves the result on paper; nothing about this model is formalized. A complete development gives a machine-checked monotone-comparative-statics argument for a reset-type MDP with a continuum of states and an expectation over a general distribution, including the measure-theoretic content the paper leaves implicit: that is an honest integral of a bounded measurable function. The formalization also repairs two printed points that matter for correctness (see Formalization scope).
Each monotonicity result is a backward induction a few lines long on paper, but the inductions interact. Monotonicity in holds trivially before the critical age and needs Condition (4) after it; the age threshold requires gluing the two regions, which the paper does not spell out. Monotonicity in compares two cultures whose critical ages differ, and its base case at age rests on Assumption 1. Monotonicity in requires , an inequality between integrals whose integrands are themselves defined by the recursion, so integrability and measurability in must be carried through the induction. A pointwise argument that ignores the integrals proves nothing about .
All declarations live in the namespace BleedFeed.ControlLimit. One definition file holds the parameters (Params), the standing assumptions (Standing), , , , the critical age, the value recursion , , , the predicates BleedOpt and ContOpt, Condition (4), Condition (5) and Assumption 1. Ages and counts are natural numbers; everything else is real. is a probability measure on with , and is a Bochner integral against it.
Committed conventions, each disclosed in the statements:
"Optimal" is always the comparison of with in the optimality equation, never a threshold policy assumed in advance, and is the integral, not a free parameter: a formalization in which could vanish by non-integrability would make continuing always optimal and the thresholds trivial. The hypotheses of the goal are jointly satisfiable with (checked on an explicit instance).
Contributions welcome: proofs of the milestones; general lemmas on measurability and integrability of finite-horizon value recursions over a real parameter; and a sharper, non-vacuous instance witnessing Condition (5).