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?
Companies often sell a machine-learning product before its model has reached its final quality. Use of the product then yields data that can improve later versions. This feedback is the AI flywheel studied by Gurkan and de Véricourt. A firm may hire a specialist to develop the model, but the specialist's effort is costly and hidden. More customer data can then change both the product's future quality and the cost of inducing effort. The authors ask how that interaction changes the firm's price and data collection relative to a firm that develops the model itself. Their working paper reports that the direction depends on how the effect of effort varies with dataset size Gurkan and de Véricourt, 2021/2022.
The setting connects a pricing decision to an incentive decision. A lower price attracts more buyers and supplies more data for the next period, yet it also gives up current revenue. When a provider trains the model, the value of additional data depends on how data alter the provider's chance of producing a high-quality result under effort and under shirking. The theorem isolates that change through one ratio rather than requiring a particular parametric learning curve.
There are two periods and a unit mass of potential buyers in each. A buyer's sensitivity to algorithm accuracy is uniformly distributed on . The algorithm's accuracy is either or , where . Given a dataset of size , a provider who exerts effort produces high accuracy with probability and pays cost ; a provider who shirks produces it with the lower probability and pays no effort cost. The firm observes accuracy and can condition payments on it, while effort itself is unobservable.
If the firm collects data at capacity , the buyer model gives period revenue
First-period sales add data to the initial dataset . When the first algorithm has low accuracy, the provider retrains it on ; when accuracy is already high, no retraining is needed. The data impact
measures the relative effect of effort on the high-accuracy probability. The paper assumes is convex on the relevant data interval Gurkan and de Véricourt, §3.2.
The firm's contract selects four nonnegative payments, one for each accuracy outcome in each period, and two first-period data quantities, and . Its expected profit and two incentive constraints are Problem (6)–(9) in the working paper. The first-best benchmark fixes each payment at and removes the incentive constraints. Write for the low-accuracy data quantity of an optimal contract and for that of an optimal first-best plan.
The main target is Theorem 1 of the working paper. For interior optimal prices, it compares the two global optima:
Since price and purchased quantity move in opposite directions in this buyer model, collecting more data corresponds to charging less than the first-best price. The three cases cover equality, underpricing, and overpricing without fixing a learning-curve formula Gurkan and de Véricourt, Theorem 1.
The milestones follow the paper's stated results. Lemma 1 characterizes the last-period myopic quantity and revenue. Lemma 2 identifies the optimal accuracy-contingent payments when first-period data choices are fixed. Proposition 1 characterizes the unique optimal contract and its reduced data-choice objective; Proposition 2 gives the unique first-best plan and places its low-accuracy data quantity above the myopic quantity. Two claims in the proof of Theorem 1 record the weak comparison and the distinctness of interior optima under strict monotonicity.
The theorem specifies the direction of a distortion in a firm's choice of data collection. Its conclusion depends on the relative change in two learning curves, not merely on the fact that more data improve model accuracy. In the increasing-impact regime, the contracting firm collects more data than the first-best firm; in the decreasing-impact regime, it collects less. The result gives a qualitative comparison for pricing and data acquisition when algorithm development is outsourced Gurkan and de Véricourt, §4.2.
The result is proved in the source paper; the task here is to give its two-period model, contract constraints, and comparison a Lean proof. The definitions also provide a reusable small model of two-outcome, two-period moral hazard with limited liability. A complete development would let later statements about welfare, capacity, or alternative contracts reuse the same precise optimization problems. No existing platform definition matches this paper's model, and the draft theorem statements currently have compilation placeholders rather than machine-checked proofs.
The first obstacle is the contract itself. Payments in the second period affect the provider's expected continuation payoff and thereby the first-period incentive constraint, so choosing each period's payments independently does not describe Problem (6). The data choice changes the probability of later accuracy and the incentive cost at the same time. A direct comparison of the two full objective values does not determine whether lies above or below ; the paper's comparison depends on how the data impact changes with . Strict inequalities also need interior optimal choices. At a boundary, two distinct objective functions can select the same endpoint even when is strictly monotone.
The Lean development uses real-valued data sizes, payments, probabilities, and revenues. It represents the learning curves and as functions on , with hypotheses restricted to . Feasible data choices lie in , and keeps every evaluated learning-curve value inside the stated domain. The standard-uniform quantile is the identity on its support. The second-period value is the supremum of revenue over ; Lemma 1 supplies its attained maximum. Both contract and first-best optimality are global over their respective feasible sets.
The standing assumptions include positive effort cost and low accuracy, , strictly increasing concave learning curves and , differentiability of both curves, and convexity of . Positive and strict make the paper's uniqueness conclusions well posed. Differentiability is weaker than the twice-continuous differentiability mentioned in the source's later proofs. The paper's condition favoring effort in both periods motivates the chosen contracting problem; effort is already imposed by its two incentive constraints. Interiority of the optimal low-accuracy quantities is an explicit hypothesis of the comparison theorem, reflecting the paper's assumption that optimal prices neither cover nor exclude the entire market Gurkan and de Véricourt, §3.4 and EC.1.
The goal concerns optimal solutions of the full six-variable contract problem and the full first-best problem. Defining and only as maximizers of the reduced one-variable objectives would omit the contract's incentive constraints. A complete proof needs real optimization on compact intervals, concavity and differentiability facts, and a precise account of the payment constraints. Contributions to those components and to the stated milestones fit this mission.
Firms decide not only how to pay workers but whom to put together. A long empirical and theoretical literature on teams asks whether homogeneous ("specialized") or heterogeneous ("diverse") teams perform better. Most arguments for diversity are informational: diverse teams bring different knowledge or perspectives. Glover and Kim (SSRN 3344922, published in Management Science 2021, doi:10.1287/mnsc.2020.3762) give an argument based on incentives instead. In a repeated relationship, teammates who can watch each other can enforce effort by threatening to punish a shirker (mutual monitoring). The same ability lets them coordinate against the principal (tacit collusion). Whether production efforts are complements or substitutes determines how strong each force is. The paper shows that diverse teams, whose efforts are complements, can be cheaper to motivate even when specialized teams are more productive. This mission formalizes the paper's main comparative-statics result about this trade-off.
The model belongs to the literature on implicit incentives in repeated teams, which studies relational contracting and mutual monitoring among agents (Arya, Fellingham and Glover 1997; Che and Yoo 2001). Its new element is that the team's technology depends on its composition.
A principal hires four agents for two tasks each period. Each task is done by a team of two agents. Each agent chooses effort (shirk or work) at cost , with , and all parties share a discount factor . A team of kind (specialized or diverse) produces with probability when of its two members work, and otherwise. The agent receives a wage on success and nothing on failure.
The standing assumptions are:
The normalized punishment is . Two thresholds matter:
The principal's programs (Appendix A) minimize the wage subject to constraints:
The least feasible wages are (diverse), (specialized, mutual monitoring only) and (specialized, collusion-proof). Expected wages are . The principal's per-period payoffs are and . With , the output threshold is
Assume , and write . Then
In attack order:
Proposition 2 says that patience affects the two compositions in opposite directions once collusion matters. As long as only mutual monitoring binds, more patience helps specialized teams more, because their larger normalized punishment is multiplied by . Beyond the specialized team must be paid to prevent its members from taking turns shirking, and this cost grows with . The threshold below which diversity is optimal therefore rises with patience past . So the model predicts that long-lived teams with valuable but not too valuable output should be diverse, for incentive reasons alone.
The proofs in the paper are short calculations, and the proof of Proposition 1 compares the gap only at , and . A machine-checked development certifies the closed forms of the three programs, the strict monotonicity on whole intervals (not only at sample points), and the derivative claim. To our knowledge none of these results has been formalized.
Each wage is a minimum over a feasible set defined by inequalities. The specialized (M-IC) constraint changes form at , and the (No-cycling) constraint takes over at . A solver must first identify the binding constraint on each region and show that the least element exists, which is Lemmas 1 and 3, before any monotonicity argument starts. The obvious approach, comparing the two closed forms termwise, fails on : there both expected wages decrease, and the claim is that the specialized one decreases faster. That requires the ratio condition together with A.1 and A.3, not just the sign of each derivative. Strictness at the kinks and , where the piecewise wage is not differentiable, also needs care.
All quantities are real numbers. A technology is a structure Tech with fields f0 f1 f2. Assumptions A.1–A.3 are kept in the paper's ratio form inside Standing. The optimal wages are not defined by closed formulas. Every theorem about them takes arbitrary functions ws wd : ℝ → ℝ with the hypothesis that, for each , ws δ and wd δ are the least elements (IsLeast) of the Appendix A feasible sets. Defining the wages by their closed forms would make Lemmas 1 and 3 hold by definition, and that trivializing formalization is ruled out. The specialized (M-IC) constraint is piecewise at , exactly as printed.
Conventions:
StrictAntiOn, StrictMonoOn).deriv on the open interval , so it also asserts differentiability.Not formalized:
The development needs only real inequalities, maxima of finitely many functions, and one-variable calculus from Mathlib. Contributions are welcome at every milestone. Lemmas 1 and 3 are reusable by anyone working on further results of the paper.
Lenders, employers and insurers increasingly screen applicants with learned scores, and regulators and the fair machine learning literature ask that such screening be fair across demographic groups. Two notions are standard. Equal treatment (ET) asks that the same decision rule be applied to everyone, regardless of group; the paper notes that it is what the law currently requires. Equal opportunity (EO), proposed by Hardt, Price and Srebro (2016), asks instead that qualified applicants be accepted at the same rate in every group. EO is often presented as the notion that protects a disadvantaged group better, because it corrects for differences in how well the screening technology separates good from bad applicants in each group.
Most analyses of these notions take the classifier as given. Fu, Aseri, Singh and Srinivasan point out that a profit-maximizing firm also chooses how much to invest in learning, and that a fairness constraint changes that choice. Their Theorem 2 identifies a regime in which, once the firm's learning response is taken into account, EO accepts no larger a share of the protected group's qualified applicants than ET does. The result is a short, fully explicit comparative-statics statement about a parametric model, which makes it a natural target for formal verification.
A bank screens loan candidates from two groups of equal (unit) size: a protected group and a regular group . A good candidate repays and earns the bank ; a bad candidate defaults and costs it . The proportions of bad candidates are and , with , and the expected profit and loss per group are
with the paper's assumption (hence ).
The bank chooses a learning effort . In group , scores of bad candidates are uniform on and scores of good candidates uniform on , where the learning rates satisfy : learning separates the regular group faster. The bank accepts a candidate of group whose score exceeds a threshold , and pays the learning cost . Its profit is equation (1) of the paper: expected profit from accepted good candidates minus expected loss from accepted bad candidates, summed over the two groups, minus .
The coverage rate of group is the fraction of its good candidates that are accepted,
Under ET the bank must use ; under EO it must equalize the coverage rates, (equation (6)). Writing for the bank's optimal decision under constraint , the quantity of interest is , the protected coverage rate at that optimum.
The paper focuses on the low-loss case (case (1), p. 17) and on learning costs in a middle range: with
it assumes with , so that learning is neither so cheap that it separates perfectly nor so expensive that the market fails.
Under the standing assumptions, the low-loss case and the cost range above, if
then for every optimal ET decision and every optimal EO decision
Theorem 2 is the paper's main statement about the protected group. It says that a constraint designed to raise the protected group's acceptance of qualified applicants can fail to do so once the firm re-optimizes its investment in learning: when lending to the protected group is risky enough relative to its return, the EO-constrained firm learns less, and the protected group's coverage rate is no higher than under ET. The paper uses it, together with its Theorem 3 on success rates, to argue that the choice between fairness notions should account for endogenous learning, and it explains the condition's dependence on the learning-efficiency gap and the expected loss .
The result is proved in the paper by first-order conditions and algebra. It has not been formalized. The formalization adds a machine-checked passage from the bank's joint optimization over thresholds and effort, with the piecewise-linear profit (1), to the closed-form comparison: the threshold reductions and the existence and location of the optimal efforts are asserted in the paper with little or no argument, and the mission makes each of them an explicit, checked statement.
The algebra of (53)–(59) is short. The work lies upstream of it. The profit (1) is a sum of min and max terms, and its maximization over thresholds must be carried out case by case on the positions of relative to the four breakpoints ; under EO the thresholds are further tied by constraint (6). The first-order conditions (47)–(48) identify the optimal efforts only once unimodality and interiority are established, and these hold only in the stated cost range: at its endpoint the ET optimum sits exactly at the boundary . Substituting the closed forms (51)–(52) directly into the conclusion skips all of this and is not the theorem.
Everything is real-valued and lives in the namespace UnfairML.Coverage. One definitions file holds the parameters (Params: ), the derived quantities, the standing assumptions (Standing), the low-loss case (LowLoss), the cost , profit (1), the coverage rate, the EO constraint (6), the optimality predicates IsOptET and IsOptEO, the reduced profits of case (1), and the cost range CostRange.
Conventions committed to:
A goal stated about maximizers of , or with (51)–(52) substituted, would be a different and much weaker statement and is ruled out. The cost range is satisfiable only when ; a sorry-free check that all hypotheses of the goal hold together for an explicit rational instance accompanies the development.
No Mathlib extension is needed beyond real analysis on intervals (monotonicity from derivatives, IsMaxOn). Contributions are welcome at every milestone; the threshold reductions are self-contained piecewise-linear arguments and a natural starting point.
Humanitarian organizations (HOs) such as the Red Cross or UNICEF keep prepositioned stock ("prepo") of relief items in distribution centres, so that they can fly supplies to a disaster area in the first days after a rapid-onset event. A second source is local purchasing in or near the affected region after the disaster strikes: it is cheaper per unit and supports the local economy, but local supply is uncertain (a severe event can destroy it), and buying it requires cash that the HO may not have at the right moment. Budgets of HOs are tight and partly random: a fixed budget at the start of a cycle, a steady inflow of donations, and an emergency fund raised once a disaster is in the news.
Eftekhar, Song and Webster (SSRN 3210309; published in Manufacturing & Service Operations Management, 2021, doi:10.1287/msom.2020.0956) model the HO's choice of a prepo level under budget, demand and local-supply uncertainty. Their single-cycle result answers a practical question: when is the classical newsvendor rule (stock the critical fractile of demand) the right prepositioning policy, once local supply and budget constraints are taken into account?
A prepo cost cycle starts when the HO chooses a prepo level and ends after the relief period of the next disaster. The unit cost of prepo is normalized to . The parameters are a holding cost per dollar-period; a local supply cost multiple ; a unit shortage cost ; an initial budget , with ; and a funds inflow rate .
On a probability space, the random time to the disaster , the relief demand , the local supply and the emergency fund are nonnegative and integrable, and is independent of ; , . When the disaster strikes, the money available for local spend is
The HO buys locally first, units, leaving the local shortage ; prepo covers and is unmet. The expected cycle cost is
and the HO solves . The auxiliary model relaxes the local budget constraint, replacing by :
With , the number is a -fractile of the net demand , and the threshold budget is
with the support of and the lower end of the support of .
If , then
The paper prints "". The last equality is false in a corner: if and almost surely, then , and any with makes infeasible. The goal states the printed equality under the extra condition, and the optimality of under alone.
Proposition 2(b) says that a well-funded HO can plan prepositioning with a newsvendor rule on net demand : the optimal shortage probability is , set by holding cost, disaster frequency and shortage premium, and the budget matters only through the cap . Below the threshold, the same rule gives an upper bound on optimal prepo (Proposition 2(a)), so separates the regime where the heuristic is exact from the one where it overstocks. The comparative statics of §4.2 and the dynamic policy of §5 build on this single-cycle analysis.
The paper's proofs are in an online supplement. This mission produces a machine-checked version of the threshold result without density assumptions, and with a corrected statement. No part of this model is formalized elsewhere: the platform's newsvendor results concern models without local supply, random budgets or a budget cap.
The cost couples three nonsmooth effects: the cap on local purchases, which depends on through the budget, the split of the shortage between prepo and unmet demand, and the expectation over a joint law with no density. The obvious argument, "above the cap never binds, so and eq. (4) applies", proves only that and agree on . For the cap can bind, so could in principle dip below to the right of . Ruling this out needs the global inequality . Eq. (4) itself is a newsvendor argument at a generalized fractile: is convex but not differentiable at atoms of , and the case , where the inverse is , must be handled.
All quantities are real; expectations are Bochner integrals over a probability measure . The standing assumptions, bundled in Params.Standing and Env.Standing, are: , , , , ; measurable, integrable and almost surely nonnegative; independent of (stated on p. 6, unused by the statements). The conventions are:
IsMinOn), since is convex but not strictly.is defined as the expectation of the operational cost (the first line of the display on p. 7), and as the separate closed expression of p. 9; a formalization defining by its closed form, or as above the threshold, would make the milestones trivial and is excluded.
Not formalized: the second clause of Proposition 1 (it needs the densities and derivatives (2)–(3)), Proposition 2(a), (c)–(e), the comparative statics of §4.2 and the dynamic model of §5. The development needs only Mathlib's integration and independence API; the newsvendor lemma at a generalized fractile (milestone 3) is reusable for other newsvendor models. Proofs of any milestone are welcome, as are a proof of Proposition 2(a) from the same definitions.
Many services are discretionary: the provider chooses how long to spend with a customer, and a longer service is worth more to the customer. Medical consultations, legal and tax advice, repair and diagnostic work, and personal services such as hair styling all have this shape. A firm offering such services designs a service line, a menu of service durations with a price for each, and runs it on one shared resource. Longer services are more valuable, but they also slow the queue for everyone else, and customers dislike waiting.
L. Debo and C. Li, in Design and Pricing of Discretionary Service Lines (SSRN 3054741, 2017; later published in Management Science, doi:10.1287/mnsc.2020.3670), study this problem by combining a Mussa–Rosen style product-line model with a single-server queue. A central question is whether congestion alone, with all customers identical, can make variety optimal. Under first-in-first-out (FIFO) service the answer is no: with homogeneous customers the optimal line collapses to a single service. Under the shortest-processing-time (SPT) priority rule the paper shows that the optimal line does offer variety. This mission formalizes that result.
Customers arrive as a Poisson process of rate . A customer who receives a service of duration gets value with , and pays a waiting cost per unit of sojourn time, waiting plus service. All customers have the same quality sensitivity : the paper's heterogeneity parameter is . The standing assumption is .
A service line is a shortest duration , a longest duration , and a demand measure on . When demand has a density , customers choosing durations in arrive at rate . Its moments are
so is the throughput and the load on the server. A line is feasible if (customers may be turned away) and (the queue is stable).
The server uses non-preemptive SPT: whenever it frees up, it starts the shortest waiting service. By Phipps and Van Voorhis (1956), a customer with duration waits in queue for
on average, which is eq. (7) of the paper. The expected queue length is . With the paper's mechanism-design problem (its Proposition 1) reduces to the firm's problem
and the price of duration is
which leaves every customer zero surplus.
For every , problem (9) has an optimal service line, and every optimal line has
There are also thresholds , depending on , such that
The thresholds are existential, so the goal does not commit to their values.
The result separates two sources of variety. Classical product-line theory obtains variety from heterogeneous tastes. Proposition 5 obtains it from operations alone: under SPT, short services jump the queue, so a spread of durations lowers total waiting below what any single duration achieves (Corollary 1 makes this exact). This outweighs the loss in service value from moving away from a single duration. The price result is the operational counterpart. Customers who choose the longest services wait the longest, so the price falls at the top of the line, and in small markets it falls along the whole line. This contrasts with FIFO, where the price always increases in duration.
Formalizing these results adds the following. The paper's proofs are long first-order-condition calculations over a constrained calculus-of-variations problem. They take existence of an optimum for granted, and they argue the bottom-end sign through Taylor approximations in the limits and . A machine-checked proof would establish existence, rigorously derive the optimality conditions over all demand measures, and turn the asymptotic sign argument into a proof. As far as is known, none of these results, nor the SPT waiting-time formula, has a machine-checked proof.
The obvious approach is to optimize pointwise in . This fails because at duration depends on the whole demand below through the cumulative load, and on , so the objective is a nonlocal, nonconvex functional of the demand schedule. A second obvious idea is to compare with the best single service. That comparison shows only that some non-degenerate line beats one particular collapsed line. It neither produces an optimum nor rules out an optimum with an atom. Existence also needs an argument: the feasible set of measures is not compact in any naive sense, because the support can drift and the load constraint is strict. Finally, the sign of depends on where the root of the transcendental equation (A–35) lies, and the paper controls this only asymptotically.
Everything is real-valued. A service line is a Lean structure with endpoints lo, hi and a measure μ : Measure ℝ. Admissibility requires:
Feasibility adds . The waiting time is
with and the loads of durations and . This is eq. (7) for densities. At atoms it is Cobham's non-preemptive priority wait, with ties served FIFO, and for a single service it is the M/D/1 value .
Point masses are allowed on purpose. If demand were restricted to densities, a collapsed line would be infeasible and would hold by construction. Letting the endpoints float freely, beyond the support, would trivialize it in the same way. Both encodings are therefore excluded.
The following conventions are committed:
A complete development needs: integration against finite measures on ; existence of optimal measures under moment and load constraints; first-order conditions for the nonlocal functional ; and real analysis of . The SPT waiting-time functional and Corollary 1's queue-length bound are reusable for other priority-queue design problems. Contributions are welcome on any milestone, in particular Corollary 1 and the existence part of Lemma A7.
A manufacturer that receives evidence of a product defect must decide whether to disclose it. A regulator that receives a report must decide whether to investigate immediately. The regulator's announcement can itself change consumer demand while the investigation is under way, so a policy intended to reveal defects may change the manufacturer's incentive to report. Cho, DeMiguel, and Hwang study this interaction for vehicle defects, comparing a U.S. policy that announces an investigation with a U.K. policy that keeps it confidential. Their analytic model identifies circumstances in which the manufacturer conceals a signal even though the expected harm is substantial. This mission formalizes the U.S. equilibrium characterization in Proposition 2 of the authors' accepted manuscript.
A product is either defective, , or nondefective, . The prior probability of defect is . A manufacturer receives a private signal indicating a possible defect. Its reliability is , and after this signal the manufacturer's posterior probability of defect is
The product sells at price over a unit-length life cycle. Consumers arrive at unit rate and have valuations uniformly distributed on . A defective unit causes expected harm . The ordinary demand rate is . When the U.S. regulator announces an investigation, consumers account for possible harm during its mean duration , so the temporary demand rate is . The model assumes , ensuring positive demand even during an announcement. These choices follow §3 of the manuscript.
After a positive signal, the manufacturer chooses report () or no report (). After a report, the regulator chooses immediate investigation () or no immediate investigation (). A later voluntary investigation can occur if the product is defective. Its time has constant density on , while the probability of no such investigation is . An investigation costs the regulator . If a defect is found, the manufacturer recalls previously sold units at unit cost and compensates consumer harm. A discovered cover-up carries penalty with discovery probability . If no investigation takes place, the manufacturer bears fraction of consumer harm. These payoffs determine three U.S. manufacturer profits, , , and , from equations (1), (3), and (5) of the manuscript.
The regulator maximizes social welfare , the manufacturer's profit plus consumer surplus minus investigation cost. The two welfare values after a report are and . The regulator chooses when these values tie. The manufacturer chooses when its profits tie. The regulator's action after is , since there is no report to investigate at time zero. These conventions are stated in §§4–5 and the proof of Proposition 2 of the manuscript.
The regulator's threshold result, the U.S. half of Proposition 1, says that there are and a curve on , with values in and , such that
Proposition 2 adds and a reporting curve with the analogous domain and endpoint value. The goal is the unique subgame perfect equilibrium for every admissible and :
The last profile records the regulator's response if a report had arrived; on the realized path the regulator does not investigate immediately. The milestone list follows the source's two welfare and profit identities, the two harm thresholds, Proposition 1's U.S. response, and the reporting rule in Step 1 of Proposition 2's proof. Each formula comes from the accepted manuscript, pp. 13, 15, 28, and 30–31.
The characterization locates the cover-up region in the harm–reliability plane. Under the U.S. announcement policy, a report can depress sales during an immediate investigation, while concealment risks a later penalty. The model shows how these forces produce an intermediate-reliability band in which the manufacturer conceals even a high-harm signal. The result can therefore be used to compare disclosure incentives under investigation policies using the same payoff primitives. The authors prove the result in the paper; the remaining task here is to formalize its stated assumptions, integral payoffs, threshold identities, and equilibrium claim in Lean. The local prior-art search found no existing formalization of this particular game.
The regulator's and manufacturer's choices each depend on a difference between payoffs defined by several integrals. The closed forms are cubic expressions in harm, and the threshold claims require their signs to be controlled on the full interval . Checking a few parameter values does not establish those interval-wide claims. At the equilibrium boundaries, both actors' tie rules matter: without them, the claimed unique strategy profile is not determined. The proof must also keep the thresholds independent of the point being classified.
The development uses real numbers for all model parameters and values. One Params record contains ; neither nor is a field of that record. Params.Standing collects the source's sign and range restrictions, including , , , , and . It also requires : the paper's definition of reliability divides by , and its threshold fractions divide by .
Profit and consumer-surplus expressions use intervalIntegral for the manuscript's valuation and voluntary-investigation integrals. Their integrands are polynomials or constants on finite intervals, so the usual nonintegrability default is irrelevant here. The posterior formula represents the signal law at the point needed by the theorem; the full joint signal distribution is not reconstructed. Likewise, the investigation lead time enters through its mean , as it does in the paper's expected-payoff formulas. The polynomial closed forms are named separately and linked to the primitive payoffs by milestone theorems.
IsSPNE is the tie-broken sequential best-response condition for the two decisions, with fixed after no report. Proposition 2 quantifies the four thresholds before all and , constrains their relevant domains, and characterizes every equilibrium profile in each region. This prevents thresholds chosen separately at each point, a vacuous regulator curve, or an existence-only restatement. The reusable work is the interval-integral algebra and interval-wide polynomial threshold arguments. Contributions on those identities, the threshold theorems, and their equilibrium assembly are all within scope. The U.K. equilibrium and later welfare comparisons are separate results in the paper.
An experiment may compare two ways to select initial participants in a social network. Each selected seed set can lead to a different outcome, and the experiment observes only the outcome for the seed set actually selected. Chin, Eckles and Ugander study how known selection probabilities let observations from one experimental design estimate the outcomes of two other seeding strategies. Their setting includes one hop targeting and random targeting, but their statistical results apply to any two stochastic strategies with known probabilities. The central result here is their Proposition 2: the Hájek estimator, which normalizes the observed importance weights separately for the two strategies, is consistent and asymptotically normal. These properties are needed to interpret a large experiment's estimated difference and its uncertainty. Chin, Eckles and Ugander, §§2–3.3 and Proposition 2.
Let be a countable space of possible seed sets, including any network information that varies across the superpopulation. Strategies and give probability mass functions and on . An experimental design distribution gives the law of each observed seed set. A fixed function records the potential outcome for each possible seed set. For a draw , the observed outcome is . The design supplies independent draws with common law ; the outcome is a deterministic function of each draw. The paper allows outcomes such as counts and fractions and does not require a finite seed space. Chin, Eckles and Ugander, pp. 8–9.
The strategy means are and . Their difference is the superpopulation contrast . For a seed set with positive design probability, its importance weights are and . Write , with analogous notation for . The paper's estimator in equation (7) separately normalizes the two sets of weights:
The design can be a mixture of and , but the proposition also addresses other designs. The formal statement therefore leaves general. Chin, Eckles and Ugander, equations (2), (4), (5), (7), pp. 9–10.
The first targets are the weight moment identities, the limits of the four sample averages, and almost sure consistency of . The joint central limit theorem for those averages and the variance identity connect these to the goal. These targets follow the displays and sentences in the proof of Proposition 2, Appendix A.2. Chin, Eckles and Ugander, pp. 39–40.
The goal is the corrected full strength of Proposition 2. Under full support of the design on the support of either strategy and finite second moments for the four weighted coordinates,
where the variance is the value specified by the paper's equation (15),
The variance is determined by the two strategies, the design, and the outcomes; it is not a free variance parameter. The almost sure limit records the strong form supplied by the sample average law. Chin, Eckles and Ugander, Proposition 2 and equation (15), p. 14.
The result identifies both the value approached by the normalized estimator and its leading large sample variance. The two normalized terms are correlated because a single observed seed set contributes information about both strategies. Equation (15) retains that dependence, so the uncertainty of their difference is not obtained by adding two separate variance formulas. The paper uses this result to motivate inference for a superpopulation contrast rather than a finite collection of villages, for which a single observation per village does not identify each village's variance. Chin, Eckles and Ugander, §3.3, p. 14.
The mathematical result is published in the cited preprint. This mission asks for a machine checked statement and proof of its corrected version, plus reusable facts about weighted moments, strong laws for transformed samples, and a four coordinate central limit theorem. The proof infrastructure can serve other comparisons of two policies under a common sampling design. The Horvitz–Thompson result in Proposition 1 is related but is a separate theorem and is outside this mission. No proof of Proposition 2 is currently included in the mission's local formalization.
The estimator is a difference of two random ratios. At small sample sizes, either normalizing sum can vanish, and the two ratios are dependent. Applying a variance formula for one self normalized estimate twice would discard their covariance. There is also a source level obstacle: the printed positivity assumption permits the design to omit a seed set on which both strategies assign equal positive probability. Such a set does not affect the strategy contrast pointwise, but it changes the separate means and the normalizing weight expectations. The printed hypothesis therefore does not imply the moment identity used in Appendix A.2. Chin, Eckles and Ugander, Assumption 1, p. 11, and proof of Proposition 2, p. 40.
For example, take three seed sets with , , and . The paper's Assumption 1 holds, but and the Hájek estimator approaches . This mission labels the replacement support condition as a correction. The printed intermediate expansion of the delta method variance also has a sign error in a cross term; equation (15) itself is retained. Chin, Eckles and Ugander, pp. 11, 14, 40.
Lean represents by an arbitrary countable type with measurable singletons, by PMF, and the sample by measurable independent maps from one probability space, each with law . The natural number is the number of sampled villages: Lean uses draws in place of the paper's . Probabilities enter real arithmetic through ENNReal.toReal; a PMF assigns finite mass to each point. Full positivity says whenever or . It is stronger than the paper's contrastive Assumption 1 and is needed for the separate means and normalization identities.
The four second moment conditions apply to , , , and under . They make the joint covariance finite even when is unbounded. The consistency milestone uses only the first moments it needs. The variance is the real integral from equation (15), then converted to a nonnegative real variance for Mathlib's Gaussian law. Lean's total division assigns zero weight when ; such a seed set is not observed under the design. The estimator is zero at , and a finite sample with a zero normalizing sum uses Lean's division by zero value. The almost sure and distributional limits address the paper's asymptotic claim.
The intended statement includes every countable seed space and every qualifying independent sample. Restricting to a finite seed space, assuming the estimator's limit or a central limit theorem, or selecting an arbitrary Gaussian variance would change the claim. The development needs Mathlib's probability measures, integration, strong law, Gaussian laws, distributional convergence, and moment theory. Contributions that establish the listed milestones or develop the general joint limit and ratio tools are in scope.
Traffic, packet and evacuation networks are often studied with atomic dynamic flows: individual agents move through a network over time, queue at congested links, and each wants to reach its destination as early as possible. The deterministic queuing (Vickrey) model makes the queue at every link explicit: a link has a capacity, and agents beyond it wait in a queue. In the atomic, discrete-time version, simultaneous arrivals at a queue must be ordered by some tie-breaking rule, and that rule decides whether the resulting routing game has an equilibrium.
Hoefer, Mirrokni, Röglin and Teng (2009, 2011) and Werth, Holzhauser and Krumke (2014) studied atomic routing over time in deterministic queuing models, and found non-existence of equilibria and computational hardness in several variants; Harks, Peis, Schmand, Tauer and Vargas Koch (2018) studied competitive packet routing with priority lists. Scarsini, Schröder and Tomala (Operations Research, 2018) proved that a Nash equilibrium exists when priorities are placed on agents, in single-origin, single-destination networks. Cao, Chen, Chen and Wang (Operations Research 2021) showed that with agent priorities and several origins an equilibrium can fail to exist (their Example 3, a rock–paper–scissors cycle). They proposed instead to break ties by edge priorities at each vertex, and proved that equilibria then always exist. This mission formalizes that existence theorem.
A network instance consists of the following data.
The agent set is the disjoint union of all these, and may be infinite.
Each agent chooses at time a path from his starting vertex to . For the path must begin with ; this is his strategy set . At every time unit only the head of the queue on an edge leaves it, and it reaches the head of the edge one unit later. Agents entering an edge are ranked by the edge-priority DQ rule, applied in this order:
denotes the time agent reaches vertex under the profile , and is if he never does.
The normal-form game has players , strategies , and cost . A profile is a Nash equilibrium (NE) if for all and . It is an iteratively dominant NE (IDNE) if the agents can be reindexed such that for every , every vertex on and every profile of the agents outside ,
The goal makes no finiteness assumption on and fixes no constants.
The result. Theorem 1 gives an equilibrium for every network with edge priorities: multiple origins, initial queues and an unbounded stream of inflows are all allowed. With agent priorities, equilibrium can fail to exist in exactly this setting. The IDNE carries more structure than an NE. Arrival times along each agent's path are independent of later agents' choices, and no agent who enters later at the same origin overtakes an earlier one. The paper uses these properties in its study of subgame-perfect equilibria for adaptive agents (p. 12; §5).
Formalizing it. The result is proved in the paper; nothing here is open mathematically. To our knowledge no part of it is formalized in any proof assistant. The mission produces:
The paper proves Lemma EC.2 in a transformed game on an infinite graph (Lemma EC.1). The mission instead states everything directly in , so a complete development must either carry out the transfer or reprove the lemma natively. For infinitely many agents, the claim that every agent is eventually indexed (milestone 3) is asserted in the paper without a separate argument; the formal proof has to supply one.
The obvious argument fails at the no speed-up property. Adding agents to a network can make some other agent arrive earlier. The paper's Example 4 (pp. 15–16) has such a chain effect: removing an agent delays another. So the claim that agent 's arrival times are unaffected by everyone after him is not monotonicity of congestion. It holds only for the specific order and paths produced by the selection procedure, and it must be proved by an induction that carries invariance (equality in (EC.2)) and domination (inequality in (EC.2)) together.
The tie-breaking is the second difficulty. The selection compares candidates backwards from : by arrival time, then by incoming-edge priority, then one edge further back. The argument has to show that this order matches the queue rule (R0)–(R4) at every vertex, including (R3) for agents starting mid-network.
Everything lives in the namespace AtomicDynFlow.IDNE.
Network and agents. Instance V E A carries the graph as finite types V, E with tail, head, d, and the priorities as lists inc v of incoming edges, highest priority first. Initial queues Q0 e are listed head first, and inflows inflow r v highest original rank first. The standing hypotheses are fields:
The agent type A is arbitrary and may be infinite.
Dynamics. queue π s e is a computable, list-based simulation of the queue on each edge at each time, under a partial profile π : A → Option (List E), where none means the agent is absent. arrival π i v : ℕ∞ is , with ⊤ for (p. ec4). The starting-vertex time is for initial-queue agents and for (Algorithm 1, Step 2).
Equilibria. The reindexing of Definition 2 is an injective whose range is an initial segment, with agent receiving index . Definition 2 quantifies over every vertex of the path, the starting vertex included.
Selection. The pruning (S1)–(S3) is a backward pairwise comparison of candidate pairs (Before, IsSelected). Milestones 2 and 4 are -native versions of the e-companion statements, and Lemma EC.1 is not formalized.
Ruled out. Three encodings would trivialize the goal, and none is used:
A sorry-free check of the paper's Example 2 shows that agent waits at and reaches at time , and that removing agent lets him arrive at .
Welcome contributions: proofs of the milestones in any order. Milestone 5 needs only the definitions. Milestones 1 and 2 are the technical core, and general lemmas about the queue simulation (FIFO within an edge, monotonicity in entry times) are reusable throughout.
A firm's accounting disclosure affects what traders know. The price produced by their orders can then affect the firm's own investment decision. In this setting, the timing of bad news changes both the speculator's incentive to trade and the information conveyed by market prices. Chen, Huang, Jiang, Zhang and Zhang study this interaction in a finite trading game, asking how timely loss recognition changes gross trading profits and the ranges of trading costs that support trading or no trading. Their result is Proposition 4 of the held working paper, later published under a different title in Management Science (published article).
The model builds on the feedback-effect framework of Edmans, Goldstein and Jiang (AER 2015), in which a firm learns from its own stock's order flow and, as a result, a speculator gains less from selling on bad news than from buying on good news; their firm has no private information of its own. The present paper adds a privately informed firm whose reporting system may disclose good and bad news with different timeliness, a theme of the accounting literature on conservatism. The paper relates its profit comparisons to the strategic-trading intuition of Kyle (Econometrica 1985).
The comparison matters because a disclosure rule that makes bad news public more often also changes what a null disclosure means. A null report can alter the market maker's valuation, while order flow can lead an uninformed firm to change investment. The question is therefore about prices and real decisions together, under the same reporting rule.
The underlying state is either good, , or bad, , each with prior probability . The firm may increase investment, decrease investment, or keep its current level. A correct change adds to terminal value and costs ; a wrong change loses and costs . Without a change, terminal value is or . The model assumes and .
The firm privately learns the state with probability ; otherwise it has a null signal. An informed firm discloses its state with probability in state and in state . Write and , so and . Positive means bad news is disclosed more promptly than good news. A feasible disclosure rule has .
After a null report, a speculator may buy one share, sell one share, or abstain. She learns the state with probability ; otherwise her private signal is null. An independent noise trader submits an order of , , or with equal probability. The market maker sees only the total order flow and prices the share at expected terminal firm value conditional on the report and . The firm also observes the order flow before its investment decision. When it has no private state signal, it invests only if its posterior exceeds , divests only if it falls below , and otherwise keeps its investment.
Two speculator strategies are compared. Under no trading (NT) she abstains; and are gross profits from deviating to a buy on good news or a sale on bad news. Under trading (T) she buys on good news and sells on bad news; and are the corresponding gross profits. Each profit averages over the three noise orders and uses the market maker's Bayesian price and the firm's response under that strategy. Let and . These are the trading cost thresholds reported by Propositions 1 and 2 of the working paper.
The goal is Proposition 4. For every feasible , selling on bad news becomes more profitable as rises, under both profiles:
In a neighborhood of neutral reporting, the trading threshold rises with :
For every feasible , the no-trading threshold under timely loss recognition exceeds both the neutral threshold and the threshold under the mirrored timely gain policy:
The milestone chain establishes the firm's investment rule, the null-report posterior and the probability of an informed firm behind that report, the relevant trading-profile posteriors, the two profiles' gross profit formulas, and the neutral-policy comparisons. The target does not assert that increases across the entire feasible range: the smaller of buying and selling profits can switch away from selling as grows.
The first claim identifies a strict incentive effect of asymmetric reporting on trading against bad news. The second concerns the trading threshold locally around symmetric reporting, and the third compares the no-trading threshold with neutral reporting and its mirror policy. Together they express how a reporting choice can change the regions of trading cost in which the two profiles are candidates for equilibrium (Chen et al.).
The result is proved in the held working paper. The formalization task is to connect it to an explicit finite Bayesian trading model in Lean. This includes the order-flow likelihoods, the market maker's posterior expected value, the firm's posterior investment rule, and the gross profits averaged over noise orders. Those definitions can support later work on the paper's other trading profiles and on disclosure choices. No machine-checked proof of this mission's goal is claimed here.
The reporting parameter changes more than the posterior probability of after a null report. It also changes the probability that a firm which made a null report privately knows the state, and hence the value traders expect after the firm's investment decision. The same order flow affects the market maker's price and an uninformed firm's investment. A direct comparison of null-report beliefs alone therefore does not establish the profit inequalities. The minimum defining adds a local regime change: near selling is the smaller profit, but that need not remain true at a larger feasible .
The Lean development uses two finite state constructors, three investment decisions, integer order flows, and real-valued probabilities, values and profits. Disclosure and order-flow posteriors are explicit Bayes ratios. Off-path order flows with zero Bayesian denominator receive the paper's belief convention: at positive , at negative . The firm's tie-break chooses the status quo at either investment threshold. The speculator's trading cost is excluded from gross profit, as in the paper.
Every theorem carries the paper's standing restrictions , , , and . The formalization also makes explicit and : both are probabilities, and endpoint choices destroy strict conclusions used here. Claims about a given require . The neighborhood claim is stated as a positive derivative throughout some open interval about zero. In particular, the profits are calculated from the Bayesian prices and the firm's response; they are not defined to equal the closed forms that the milestones ask solvers to prove.
Reusable work includes finite likelihoods, posterior calculations, the optimal investment rule, and algebraic profit reductions. Contributions toward the source-labelled milestone statements and the full derivative comparison are welcome. The held source is the authors' 2018 working paper; its pages and numbering have not been reconciled with the retitled 2021 journal article.
Durable life-improving products such as solar lamps, water filters and clean cookstoves reach few households in the base of the pyramid (BOP), the low-income markets of developing economies. Two frictions explain much of the gap. Customers cannot afford the product (low ability to pay, ATP), and they are uncertain whether an unfamiliar product is worth its price; being poor, they are also risk averse. Distributors and the foundations that fund them must decide how to spend a fixed budget: on subsidies that make the product affordable, on marketing and demonstrations that inform customers, or on return policies that remove the risk of trying.
Calmon, Jue-Rajasingh, Romero and Stenson (M&SOM 24(4), 1887–1905, 2022; accepted manuscript SSRN 2882402) model this decision, motivated by the Indian distributor Essmart. Their headline finding concerns a funder's dilemma: in the BOP, the allocation that maximizes the distributor's profit is often the one that gives customers the lowest average consumer surplus, and the misalignment disappears when the ATP is high. This mission formalizes that finding and the chain of results the paper proves on the way.
A unit mass of customers values the product at with probability , and lower otherwise. A fraction of customers is informed and knows its valuation. The rest know only the population distribution. Customers have CARA utility with risk aversion , and all of them can pay at most , the homogeneous ATP. A distributor buys at wholesale cost , salvages returned units at , and values consumer surplus with weight .
The distributor has a budget per customer. It can raise the ATP by a subsidy , and it can raise the education level from to at marginal cost . A downstream retailer then sets prices and refunds. The resulting pricing outcome is given in closed form by the paper's Proposition B.1:
Each strategy has its profit and consumer surplus . The budget constraint is , where the demand is under (a) and under (b).
Theorem 1 reduces the allocation problem to four strategies:
Each strategy has an explicit allocation , profit and consumer surplus . The ATP thresholds are
and the parameter bounds are and .
There is a threshold such that for every , MR maximizes consumer surplus with , and
If and , then . There is also a threshold such that
and F is both profit-optimal and worst for consumers iff and . Finally, MR is profit-optimal for all when .
In attack order:
The result separates two regimes:
For a funder whose grant the distributor allocates (p. 10), this means that profit-seeking allocation serves customers well only outside the BOP. The paper's §4.3 goes on to show that an operational commitment, free returns, reduces the misalignment; that extension is not part of this mission.
The results are proved in the paper by direct case analysis; none of them has a machine-checked proof. A complete formalization would make the hypotheses explicit. For example, the paper's list of ATP thresholds includes , which fails for . The proof also claims that alone makes MR more profitable than F; a counterexample before is recorded in the moderation notes. Formalization would pin down the tie-breaking and degenerate cases that the prose leaves implicit, and provide a reusable model of CARA-refund pricing with budgeted subsidy and education.
Each strategy value is a composition of positive parts, minima, indicator tie-breaks and a log-exponential refund. The comparisons in the strategy map are therefore piecewise in , and the obvious approach, writing the closed forms and comparing, breaks into many cases. The threshold statements are harder than inequalities. "F is optimal iff " asserts that the set of good is a closed upward ray, so one needs monotonicity in of every competing value. That includes , whose allocation jumps when the tie-break flips. One also needs closedness at the jump. The consumer-surplus threshold rests on being non-decreasing in , and on the refund term staying within .
Everything is real-valued, in the namespace BOPDistrib.Misalign, with the definitions in one file. The parameters are a structure Params with fields ; and are explicit arguments.
The formalization commits to the following conventions.
Added standing hypotheses relative to the page:
A formalization in which the thresholds are chosen after (so that is trivial), or in which is compared with closed forms that build in the conclusion, would be vacuous; both are excluded by the statement shapes. The heterogeneous-ATP model of §5, the free-returns setting of §4.3, and the regime or are out of scope.
The work needs elementary real analysis: monotonicity of in , limits at and , and piecewise-linear optimization over a polygon. Contributions of proofs of any milestone are welcome, as are lemmas on the monotonicity of the refund in , which every threshold uses.
Many digital goods are sold as bundles assembled from the output of many independent producers: a streaming service carries films from many studios, a music subscription carries many labels, a news or software aggregator carries many publishers. One retailer (the aggregator) prices the bundle and keeps a share of the revenue. The producers split the rest in proportion to how much content each contributes. Two questions follow. How much does each producer contribute when it competes with the others for the shared revenue? And how many producers can survive with positive output when their costs differ?
H. K. Bhargava's Bundling for Flexibility and Variety: An Economic Model for Multiproducer Value Aggregation (Management Science, 2021, doi:10.1287/mnsc.2020.3662) answers both questions in a stylized model with an explicit equilibrium. Its central result, Lemma 1, gives the retailer's price, the number of active producers, and every producer's output in closed form. The paper's propositions are then derived from these formulas: how outputs respond to costs, how participation responds to the bundle-size elasticity , and the effects of mergers and of the revenue share . This mission formalizes Lemma 1 from the author's accepted manuscript (2020).
There are producers, indexed in ascending order of unit cost, . Producer chooses an output , measured in value units. The bundle has size .
Retailer. For a bundle of size the retailer charges a price . Demand is
with zero demand when . The retailer's distribution cost per unit of demand is (the paper writes this coefficient as ). The retailer keeps a fraction of the surplus, so its profit is
The sharable surplus is the largest value of over all prices , which is the surplus at the retailer's optimal price. Throughout, .
Producers. Producer receives the share of the surplus and pays , so its profit is
Producers choose their outputs simultaneously. A profile is a Nash equilibrium if no producer can increase its profit by changing its own output to any other .
Write .
Let
Then . The retailer's unique optimal price is . A profile is a Nash equilibrium if and only if it equals . Moreover, , every , and the producers with positive output are exactly those with . When , . When , holds exactly when .
Lemma 1 is the basis of the paper's comparative statics. Its formulas show that output falls with a producer's own cost and rises with the revenue share. They also show that the number of active producers is set by a single threshold condition rather than by an iterative entry process. Under proportional sharing, several producers with different costs can all remain active, and the condition for at least two active producers is the paper's headline insight about variety.
The paper establishes the closed form by summing first-order conditions. It does not argue that the stationary points are maximizers, that no inactive producer gains by entering, or that the equilibrium is unique. A machine-checked proof of the full characterization, uniqueness included, makes the model a verified base for the paper's later propositions and for variants with other demand curves or sharing rules. No formalization of this model was found on the platform.
The first-order conditions give each active producer's output as a function of the aggregate , and summing them over a guessed active set gives . The obvious argument stops there. Turning that computation into an equilibrium characterization requires several further facts.
Finally, is defined as a supremum over prices, so the closed form (3e) itself requires solving the retailer's problem, including prices above the choke price.
Producers are Fin I with 0 < I, so Lean's producer i is the paper's producer . The paper's distribution-cost coefficient is named w, and every of the paper is A - b * w. Costs are ordered by Monotone c and are positive. The standing hypotheses are , , and . The paper uses , and implicitly; they are needed for the formulas to be finite and well-defined. All powers are real powers. Demand uses Real.sqrt, which returns above the choke price. Outputs are arbitrary nonnegative reals with no upper bound. The Nash equilibrium is the published predicate CachonCoord.Proportional.IsNash (nonnegative real strategies, unilateral deviations) applied to the producers' payoffs. Because the retailer's optimal surplus is folded into , this is the subgame-perfect reading of the paper's backward solution. The share at evaluates to in Lean; the all-zero profile is still not an equilibrium.
Two readings of the page are fixed explicitly. "The equilibrium" means the unique Nash equilibrium. "The set of producers with positive output" is stated exactly, because with the weak inequality of (2a), a producer whose cost ties the threshold has output . Three slips of the page are corrected rather than copied. The page calls "the average"; the formalization uses the average . The share formula printed in the proof is wrong and is not formalized. The proof's "" holds only weakly under ties.
The producers' payoff uses the surplus at the retailer's optimal price for the realized bundle size, a supremum over prices. It is not the closed form (3e), so none of the closed forms holds by definition. , , and are fixed by the page's formulas and are not quantified as arbitrary objects satisfying (6).
Everything needed beyond Mathlib is in one definitions file in CoProdBundle.Equil. Contributions are welcome on every milestone. The retailer's square-root pricing problem (milestone 1) and the concavity of the proportional-share payoff behind milestone 2 can be reused in other aggregative games with proportional revenue sharing.
An impulse control changes a system's state at a chosen instant, rather than continuously adjusting its drift. When several decision makers can intervene in the same state process, an intervention changes both the acting player's future cost and every opponent's. This makes the equilibrium question different from separate single-player control problems. Basei, Cao and Guo formulate a multidimensional, -player stochastic impulse game and give a verification theorem for Nash equilibria in their preprint. This mission formalizes that theorem, Theorem 2.12, and the path and QVI statements on which its proof depends. It is the cost-minimizing, -player generalization of the two-player impulse game of Aïd et al., posed independently because the conventions and equilibrium inequalities differ; that two-player verification theorem is itself an open target on the platform.
There are players and a state in a nonempty open domain . Between interventions the state follows an Itô diffusion with drift , volatility , and an -dimensional Brownian driver. Player chooses a strategy : a closed action region and a continuous impulse rule . When the state enters , that player shifts it from to . The process stops at its exit time from . The action regions of an admissible profile are pairwise disjoint, although consecutive interventions at one instant can still occur when an impulse lands in another player's region. These rules are given in Definitions 2.1, 2.2 and 2.7 of the source.
Every player minimizes cost. Player pays a discounted running cost , an own-intervention cost , a cross cost when player intervenes, and terminal cost if the game exits. With and denoting player 's intervention times and impulses, the expected cost is
An admissible profile satisfies the source's integrability, moment and nonaccumulation conditions. A Nash equilibrium is an admissible profile for which no player can lower their own cost through an admissible unilateral change Definitions 2.6–2.8.
For candidate values and minimizing impulses , define the own intervention operator and the cross intervention operator . Put , , and . The QVI system requires a boundary limit , nonnegative own intervention gaps, zero cross gaps when an opponent acts, and the diffusion condition
Here is the generator of the diffusion with the same and equations (2.10)–(2.13).
The goal, Theorem 2.12, says that if every uniquely minimizes the own intervention expression, the solve the full QVI system and have the stated smoothness and boundary regularity, and is admissible at , then (with one added hypothesis, explained under Formalization scope)
The milestone list follows the proof's path: the controlled-process representation and jumps in Lemma 2.3; the candidate opponents' waiting and intervention properties in (2.15); the smooth approximations of (a)–(c), which the paper takes from Øksendal, proof of Thm. 10.4.1 and App. D; the three pointwise comparisons (2.19)–(2.21), a thin bridge from the QVI to the proof; the deviation bound in Step 1; and the value identity in Step 2. The localized Itô identity (2.18) is not a separate milestone: as printed, its expectation is not shown to be finite near the boundary of , and with simultaneous interventions its jump terms must be read stage by stage, so a faithful statement needs choices the page does not make. It remains the natural intermediate target between (a)–(c) and Step 1.
The theorem turns a regular solution of a coupled, nonlocal QVI system into a certificate for an equilibrium and its expected costs. It supplies the bridge from analytic candidate value functions to the original stochastic game. The result is proved in the preprint; the Lean declarations here are open statements, so the remaining work is a machine-checked development of the path construction, Itô formula across interventions, approximation near action boundaries and limiting arguments. The stochastic basis and diffusion generator reused here are published definitions from the two-player development, while the -player game and its minimizing QVI are new reusable interfaces.
Applying a smooth Itô formula directly to fails because jumps at interventions and is only across . The source therefore uses smooth approximations and localizes before taking limits Theorem 2.12, proof. The analytic challenge is to control the generator of the approximants near a Lipschitz surface; the probabilistic challenge is to justify the expectation and the limits from the exact admissibility conditions. Treating the QVI as an inequality everywhere in would impose a generator value where the second derivative need not exist.
Lean represents the state as a Euclidean space, players as Fin N with , costs and values as real numbers, and times as . The published SolvesFrom predicate encodes the restarted SDE through a Brownian Itô integral; the filtration satisfies the usual conditions and supports an -Brownian motion. The source names the Brownian natural filtration, so this is a disclosed generalization. An admissible realization is a family of diffusion pieces solving that same SDE. Membership in asks for at least one realization, while cost identities and Nash comparisons cover every admissible realization. The expected cost includes an integrability requirement, and admissibility asks that the running-cost integrand be integrable in time along almost every path, which is how "provided that the right-hand side exists and is finite" (Definition 2.6) is read. This prevents Lean's integral default on a nonintegrable payoff from making the theorem empty.
is open: the page calls it "a non-empty subset", but p. 9 says that "is not defined in ", which is openness, and the condition (ii) and the generator in (2.13d) need an open domain. One hypothesis is added to Theorem 2.12, Step 1 and Step 2: along every admissible deviation, the time the state spends on has Lebesgue measure zero almost surely. This is the occupation-time hypothesis of Øksendal's Theorem 10.4.1, the result whose proof the paper cites for (a)–(c); the passage from (2.17) to (2.18) uses it, because (c) controls only off . The page omits it, and the theorem fails without it when is degenerate: a path can run along , where (2.13d) imposes nothing on . For a nondegenerate diffusion the hypothesis holds automatically. In (a)–(c), is assumed open, as the page's presupposes; in the proof it is open because is open and the are closed.
The path construction uses entry into closed action regions, choosing the least index when multiple entry times agree; exit from uses the next stage's exit time. Discount at infinite time is zero. The path norm in the moment condition is taken through , because a process continued beyond game exit could have an infinite global supremum and make empty. Cross costs use player 's intervention time. Boundary data in (2.13a) are limits from within ; the generator equation and derivative bounds are required where the derivatives exist, off . The common waiting region includes , so it remains for one player. Action regions are built from and , not free variables. The source's printed formulas also call scalar costs vector valued and state some jump identities without accounting for consecutive interventions; the definitions and Lemma 2.3 follow the operational readings described in the item notes. In Lemma 2.3 the avoidance of the action regions is stated at positive times, since the initial state may lie in an action region without an intervention at time . A statement that drops the QVI clauses, fixes one realization for the conclusion, restricts the deviations, or reads (2.8) as a supremum over all times (which makes empty for bounded ) would trivialize the goal and is ruled out by the definitions.
The definitions of the N-player path, admissibility, cost and QVI are intended for reuse. Contributions that establish the localized Itô identity, smooth approximation and dominated-convergence steps are especially useful. Every proposed proof must preserve the full QVI system, all admissible unilateral deviations, and the source's standing assumptions.
Diversification is the oldest prescription of decision theory. Bernoulli (1738) used the example of a merchant, Sempronius, who can send his goods on one ship or split them over two ships, and showed that an expected-utility maximizer with concave utility prefers to split. Portfolio choice, insurance and supply-chain sourcing all rest on the same principle: when the risk of loss is known, spreading exposure helps a risk-averse decision maker.
Most real diversification decisions are made without knowing the probability of loss. A common intuition in the ambiguity literature holds that ambiguity aversion, a dislike of not knowing the probabilities, should add a second motive to diversify on top of risk aversion. Epstein (2010) and Klibanoff, Marinacci and Mukerji (2012) debated whether the smooth ambiguity model of Klibanoff, Marinacci and Mukerji (2005) captures a preference for diversification at all.
Berger and Eeckhoudt (iRisk Working Paper 2021-iRisk-02; Management Science 67(3), 2021, doi:10.1287/mnsc.2020.3823) return to Bernoulli's two-ship problem with two experts who disagree about the probability that a ship perishes. They show that ambiguity can lower the value of diversification: under ambiguity neutrality it is below the value for the corresponding known risk (their Proposition 2), and in the smooth model, under constant or increasing absolute ambiguity aversion, it is below the ambiguity-neutral value (their Proposition 4.1). This mission formalizes the second result.
A decision maker has sure wealth and ships cargo of value . A ship perishes with probability . Her utility is . Shipping everything on one ship, or splitting the cargo over two ships that perish independently, gives the expected utilities
The value of diversification under risk is .
Under ambiguity, two experts give probabilities . The decision maker holds the prior , with . Write for the value of diversification according to expert . The ambiguity-neutral decision maker averages the experts' expected utilities, so that
The smooth ambiguity model aggregates them through an ambiguity function and takes the certainty equivalent:
A concave expresses ambiguity aversion. A linear gives back . The coefficient of absolute ambiguity aversion is . The decision maker exhibits DAAA, CAAA or IAAA (decreasing, constant or increasing absolute ambiguity aversion) when is strictly decreasing, constant or strictly increasing.
Let be nondecreasing and concave, and let be , concave, with . Suppose that (i) IAAA holds and , or (ii) CAAA or IAAA holds and . Then
Proposition 4.1 shows that the smooth model does not automatically turn ambiguity aversion into a stronger taste for diversification. Under CAAA, the exponential case used throughout applied work, together with experts who both consider a loss at least as likely as not, the smooth value of diversification never exceeds the ambiguity-neutral one. Together with Proposition 2 this says that, in Bernoulli's own example, ambiguity weakly lowers the incentive to diversify. Applied models that use the smooth criterion to explain hedging or portfolio spreading by ambiguity aversion rely on the opposite comparison. The result marks the conditions on and on the experts' beliefs under which that comparison fails.
The paper's proofs are short, but they compress several steps. Lemma 1 is Pratt's (1964) characterization of decreasing, constant and increasing absolute aversion through certainty equivalents, cited without proof. Case (ii) relies on the sentence "it is easy to show that, under the concavity of , inequality (A.8) is satisfied if ", and (A.6)–(A.8) are stated through an expectation over a random whose law is never specified. A formal proof fixes the exact hypotheses: risk aversion and monotonicity of , the regularity of , and the weak form of the conclusion. The mission also yields a reusable Lean statement of Pratt's comparative-statics lemma for two-point lotteries. As far as is known, none of these results has a machine-checked proof.
The algebra (milestones 1, 3, 5, 6) is routine. Lemma 1 is not: its hypothesis is a pointwise condition on , a local quantity, while its conclusion compares certainty equivalents, which are global quantities involving . Mathlib has no theory of absolute risk aversion or of Pratt's comparison for this to rest on.
The natural first attempt at the goal applies Lemma 1 directly, but this only works when every expert's utility rises by the same amount, which is case (i). In case (ii) the shifts differ, and comparing with the weighted average requires knowing which expert gains more. It also requires that this expert is the one with the higher no-diversification utility, and that is where and the monotonicity of enter.
All quantities are real. The utility and the ambiguity function are functions , so outcomes are allowed and logarithmic utility is outside the model. The two experts are two real parameters with prior weights , exactly as the proofs write them. is Function.invFun φ. Every argument it receives is a -mixture of two values of a continuous, strictly increasing , so it lies in the range of and the inverse is the true one.
The following hypotheses are added to the page and disclosed in each item:
IAAA, CAAA and DAAA are monotonicity of , not a sign condition on . "Decreases the value of diversification" is the weak inequality , the comparison (A.4) of the proof. The strict inequality is false at , at , or for linear .
The values of diversification are defined as differences of expected utilities. The closed forms (A.1), (A.2) are milestones, so they cannot become definitions under which those milestones hold by rfl. IAAA is defined through , never through certainty equivalents, which is the conclusion of Lemma 1. Milestone 7 is a repaired two-expert reading of the (A.8) step, not (A.8) as printed.
Not formalized: Proposition 2, the -maxmin results (Propositions 3.1, 3.2), Proposition 4.2, the converse of Lemma 1 and its version for general random variables, and the numerical examples.
Welcome contributions: proofs of the milestones, a general Pratt comparison theorem for certainty equivalents in Lean, and the omitted companion results.
In sequential social learning, agents act one after another. Each agent observes the actions of its predecessors and a private signal about an unknown state of the world. The model explains herd behaviour, information cascades and the adoption of products, technologies and opinions when people imitate one another. The basic question is whether the population eventually acts as if it knew the state, or whether public information can lock agents into a wrong action.
The answer depends on the setting:
A social learning model consists of the following:
A state is drawn once. Agents act in sequence. Agent observes the history and a private signal , drawn conditionally i.i.d. given . It then chooses an action by a mixed strategy . All agents share a utility from the class of bounded measurable functions that are continuous in the action. The profile , the prior and the kernel determine the play measure on states, signals and actions.
A profile is a perfect Bayesian equilibrium (PBE) if no agent can raise its expected utility by changing its own strategy. Write and .
Let be the posterior probability of an event after one signal . The information structure has totally unbounded signals if the support of the law of contains both and for every event with .
The statement is an equivalence between two properties of the model. It has no constants.
The milestones are the results the paper's proof uses, in attack order:
Theorem 1 separates two questions. Whether learning succeeds for a particular utility depends on the utility, and for finite actions the paper gives weaker sufficient conditions (its Theorems 2 and 3). Whether learning succeeds for every utility depends on the information structure alone, and total unboundedness is exactly the condition. The theorem extends Smith and Sorensen's binary characterization to arbitrary separable complete metric state spaces. It also shows that their convex-hull condition does not carry over to more states. Lemma 1, the vanishing value of private information, holds in every sequential social learning game and is a reusable tool beyond this paper.
The results are proved on paper. To our knowledge none of them has a machine-checked proof. Formalizing them requires:
The paper's proofs pass over some of this measure theory, for example the measurability of best replies and of the maximal posterior payoff. A formal proof has to supply it.
Necessity is a direct construction. The difficulty is sufficiency. The natural first idea is to copy the binary argument: the public belief is a martingale, so it converges, and at a limit belief in the interior of the simplex unbounded signals would give private information positive value. With a general state space and a general utility this breaks in two places:
The paper handles this with three ingredients:
Each step uses facts about conditional distributions that hold only almost everywhere.
Everything is in the namespace SeqSocialLearning.Adequate on top of Mathlib. The conventions are:
Fin t → A.Kernel ((Fin t → A) × S) A, so they are mixed, as on p. 4. Restricting to pure strategies would change the equilibrium set.Kernel.trajMeasure on trajectories of triples . The state is copied into every coordinate.posterior and condDistrib. "The support contains and " is stated in the equivalent -form.Nonempty Ω appears as a hypothesis; it follows from being a probability measure.Two formalizations would make the goal trivial, and both are excluded:
Contributions are welcome on two kinds of work:
condDistrib along a filtration, and the identification of the play measure's marginals;Theorems 2 and 3 (finite actions), Lemma 6, the second part of Lemma 5 and Example 1 are not part of this mission.
A medical visit, a hotel stay or a bank onboarding is not one transaction but a service process: a sequence of steps (check-in, waiting, examination, payment), each delivered by the provider and each experienced by the customer. Practitioners design such processes with descriptive tools such as customer-journey maps and service blueprints, which list the steps and their touchpoints but do not say how much effort each step deserves. Two features make this allocation non-obvious. First, customers judge the experience as a whole, and the experiences at different steps are correlated: a long wait colours the examination that follows. Second, effort changes not only the average quality of a step but also its variability, and the direction depends on the step: at a routine step (check-in) more effort makes the outcome more predictable, while at a non-routine step (a diagnostic procedure) it may make it less so.
Bellos and Kavadias (Management Science, 2020) give a model in which the optimal effort per step has a closed form, and characterise when the efforts at two steps move together (are complementary) or in opposite directions (are substitutable) in response to a change in one step's characteristics. The answer depends on the two step types and on one entry of the inverse of the correlation matrix, not on the correlation itself. This mission formalizes that characterisation.
There are steps . The provider chooses an effort at every step and one price .
The paper's analysis assumes that each lies in an explicit interval built from the other parameters, the cofactors of and (the interior condition), and for its comparative statics it sets the technical couplings between distinct steps to zero.
Fix a step . Under the interior condition and without technical coupling, the effort at step satisfies
and for every the effort at step responds to , and in the same directions if and only if
and in the opposite directions otherwise (when ). The derivatives are of the optimizer of the design problem, in one parameter at a time.
The result. Proposition 3 says that a change at one step propagates to every other step through the inverse correlation matrix. An entry is, up to a negative factor, the partial correlation of steps and given all other steps. So two steps whose experiences are positively correlated can still have substitutable efforts once the rest of the process is accounted for, and two uncorrelated steps can have coupled efforts. Pairing a routine with a non-routine step reverses the direction. The paper's later results, on antedependent and autoregressive correlation structures and on the first versus the last step, use this characterisation as their starting point.
Formalizing it. The result is proved on paper. As far as is known, it has no machine-checked proof. Formalizing it means: a verified closed form for the maximizer of a box-constrained concave quadratic with a correlation-matrix Hessian; the identification of the optimizer with that closed form near the base point, so that the optimizer is differentiable there; and the sign analysis. Along the way the formalization corrects two printed slips: the auxiliary quantities and in the proof of Proposition 3 (as printed, the displayed identity for fails), and the printed "Otherwise", which is false when .
The sign algebra at the end is short. The work lies in the step before it: Proposition 3 differentiates the optimizer of a constrained problem, not a formula. To differentiate it one has to show that under the interior condition the optimizer exists, is unique, and coincides with on a neighbourhood of the parameters in each direction of perturbation. This needs strict concavity from positive definiteness of , the identification of the interior condition (stated through cofactors of ) with , and the openness of that condition in the parameters. Differentiating directly and reading off signs proves a statement about the closed form, not Proposition 3.
Steps are Fin n, 0-based. All quantities are real. The utility is defined by its mean-variance expression; no random variables appear. is assumed symmetric, positive definite, with unit diagonal and off-diagonal entries in . The cofactor is Matrix.adjugate P i j. Two hypotheses are added to the page and disclosed: (the model allows , but Proposition 1 divides by ) and (every step is routine or non-routine). Proposition 3 assumes for , the paper's own simplification for §4. A partial derivative is Lean's deriv of the optimal effort along one parameter, the others fixed ( fixed when moves, fixed when moves). The optimal effort is a choice of maximizer of the §3.3 problem, with junk value when none exists.
Stating Proposition 3 for the closed form instead of the optimizer of the design problem would trivialize it, and that formalization is ruled out. Likewise the interior condition is the page's interval on , not the assumption .
The development needs Mathlib's positive definite matrices, adjugates and determinants, strict concavity, and one-variable derivatives. Reusable by-products: strict concavity and the unique maximizer of a concave quadratic with Hessian ; positivity of principal cofactors of a positive definite matrix. Contributions are welcome on any milestone, and alternative proofs of Proposition 1 by convex duality or KKT are welcome too.
Proof-of-work mining allocates a fixed reward among miners whose investments determine their chances of receiving it. The resulting distribution of mining power matters for decentralization: if a few miners control most of the investment, the economic mechanism does not support a diffuse set of participants. Arnosti and Weinberg study this question in a contest model where miners have different unit costs and rewards may rise more than proportionally with investment. Their proportional model has an explicit equilibrium; the economies-of-scale model asks what can still be said about market shares when that explicit characterization is unavailable.
The authors' result is a bound for each miner who invests, measured against the cost of any other miner who invests. It applies even when unit costs are asymmetric. The claim is conditional on a pure equilibrium: for sufficiently strong economies of scale, such an equilibrium need not exist, as the paper observes. The mission concerns the quantitative restriction on every equilibrium that does exist, not an assertion that all parameter choices have one.
There are miners and a prize worth one. Miner chooses a nonnegative investment and pays , where the unit cost is strictly positive. A parameter determines how investment affects rewards. At an investment profile , the market share of miner is
when some miner invests. When every investment is zero, the model assigns every miner share zero. The utility of miner is . The prize value is fixed at one throughout; there is no extra reward parameter.
A pure Nash equilibrium is a nonnegative profile at which no miner can increase its own utility by replacing with another nonnegative investment while all other investments remain fixed. This global comparison matters because, with economies of scale, a local first-order condition alone does not characterize a best response. The paper's phrase “equilibrium in the EoS model” has this pure-strategy meaning. A miner participates when ; at the equilibrium profiles of interest this is equivalent to having positive market share.
The paper states the cost vector in increasing order without loss of generality in its earlier proportional-model section. The share bound is invariant under relabelling, so its formal statement permits any assignment of positive costs to the miners. No pair of miners has to be distinct.
The goal is Theorem 2 of the arXiv preprint. For every pure equilibrium and every pair of participants , including , it states
The bound depends on both the scale exponent and the relative costs. Setting gives the symmetric threshold for each participant. The target therefore retains the exact cost ratio and the paper's quantifier over all participating pairs. It does not require a selected or unique equilibrium.
The milestone list follows the authors' named results and one explicit analytic statement in their proof. Lemma 3 gives the equilibrium identity and a separate inequality that still applies to a nonparticipant. Corollary 4 gives when . In the proof of Proposition 1, the function is decreasing on the open interval ; the milestone states strict decrease, matching the negative derivative shown there. Proposition 1 then says that if , then , with equality exactly when . These are the source's results that support Theorem 2, rather than substitutes with weaker conclusions.
The theorem turns a claim about scale effects into a checkable limit on equilibrium concentration. When costs are equal, every participant has share at least . Thus, as the paper notes, sufficiently strong scale effects limit the number of participants in any pure equilibrium. With unequal costs, the same result gives a pairwise share guarantee that accounts for each miner's cost relative to another participant's. A bound only in terms of would lose that comparison.
The mathematical result is proved in the cited paper. This mission asks for machine-checked Lean proofs of the statement and its source milestones. The definitions and theorem statements here are local drafts; compilation of a statement confirms that Lean can parse it, not that a proof exists. The reusable global pure Nash predicate is imported from an existing formalization. The paper-specific layer consists of the contest success function, utility, equilibrium specialization, and share-shape function. Together they make it possible to compare formal proofs of the same economic claim without silently changing the game.
For , the utility from a unilateral investment change can have a shape that is not captured by a single local optimum test. An argument based solely on setting a derivative to zero can miss a better distant deviation or the boundary action . The first-order relations of Lemma 3 are consequences of global equilibrium, not its definition. The main share bound also compares two miners at once: knowing only a participant's own first-order identity gives an expression involving its own share and investment, while Theorem 2 asks for an exact ratio of two different costs. Proposition 1 supplies the ordering information needed by the authors' argument. At , the model meets the proportional case, so formulas involving must still make sense at zero investment.
Lean indexes miners by Fin n; its zero-based labels correspond to the paper's miners without changing any statement. The model uses real-valued investments and costs, with the strategy constraint , and real exponentiation for . Standing assumptions are , , and for every miner. The model explicitly assigns zero share at the all-zero profile, rather than relying on a convention for division by zero. The imported feasible-strategy Nash predicate is specialized to the set of nonnegative real numbers and therefore quantifies over every nonnegative unilateral deviation. No theorem adds positivity of the aggregate investment as a premise: that property must follow from equilibrium where it is needed.
These choices rule out a trivializing formalization in which equilibrium is defined by Lemma 3's first-order equations or the goal is weakened to the equal-cost case. The exact exponent, the unit prize, and the ratio are part of the target. The real-power convention gives at in Lemma 3's inequality; the theorem's denominator is positive at equilibrium. Formal proofs will need finite-sum and real-power facts, unilateral-deviation reasoning, real analysis for the shape function, and inequalities linking investment, share, and costs. Proofs of the four milestones, alternative proofs of the goal, and reusable game-theoretic lemmas are within scope. The paper's separate proportional-equilibrium characterization and countably infinite-miner model are outside this mission.
A cloud provider buys servers in preset configurations, while its demand for processing and memory grows at different rates. Each server configuration supplies both resources, so adding capacity for one resource also changes the unused capacity of the other. Purchases incur a charge for the servers, a charge for making an expansion, and an ongoing cost for unused capacity. The choice between buying configurations together and staggering their purchases is therefore a cost decision even when demand is known. Arbabian, Chen, and Moinzadeh study this decision for two resources and two server configurations over a finite planning horizon. Their Proposition 1 identifies a threshold in the fixed cost of a joint expansion.
The result was stated in the authors' April 14, 2019 manuscript and published in Manufacturing & Service Operations Management in 2020. This mission uses the manuscript's theorem numbers and pages. The result is a known mathematical claim; the remaining work is to give its definitions and proof in Lean, with the source's policy classes and cost accounting represented explicitly.
There are two capacity attributes, indexed by , and two cluster types, indexed by . A unit of cluster supplies units of attribute . Demand for attribute increases at a nonnegative rate over , and is its growth between and . The provider starts with both attributes at their minimum desired excess capacity, normalized to zero. It must meet demand at every time and return both excess capacities to zero at the end of the horizon. Replenishment takes effect immediately. These are the base-model conventions in §3 of the manuscript.
A capacity expansion cycle begins and ends when both attributes are leveled. In a sequential cycle, one cluster type leads: it is bought one or more times, followed by one purchase of the other type. Each expansion costs . In a simultaneous cycle, both types are bought at each expansion, whose fixed cost is for . Cluster has unit purchase cost , and unused attribute has holding rate . If is the excess capacity after the expansions at time , total holding cost is . Total cost also includes all fixed and purchase costs. Sequential policies may have any positive number of cycles, any positive number of leading expansions within each cycle, and either leading type. For joint policies, the intervals between consecutive joint expansions form a partition of .
The main target is the unique fixed-cost threshold of Proposition 1. Write for the infimum of costs of all feasible sequential policies and for the corresponding simultaneous infimum. The threshold satisfies, for every ,
This makes equality at explicit, in line with the paragraph following Proposition 1. The milestone list records the source's sequential and simultaneous cost identities, the fixed-time holding comparison, the split comparison from the appendix, the two endpoint inequalities, and monotonicity in . Equation (8), which fixes the final sequential expansion time inside a cycle, is another milestone because the authors use its uniqueness in their analysis.
The threshold gives a precise decision rule for the model: a lower relative joint expansion charge favors buying both types together; a higher charge favors staggered purchases. It compares optimized policies, whose cycle boundaries and expansion times may differ, rather than only two schedules held at the same times. The result therefore captures the interaction of the fixed charge and the time spent holding unused capacity. The paper also analyzes specialized one-cycle schedules under exponential demand; those results are separate from this mission's general comparison.
A completed Lean development would make the policy definitions, cost identities, and threshold claim machine checked. It would also provide reusable definitions for finite-horizon bundled capacity expansion, including a time-dependent excess-capacity trajectory and its integral holding cost. The manuscript supplies a mathematical proof, but this proposal's theorem files currently contain open sorry proofs. The mission invites proofs of its listed statements and the analytic facts needed to connect them, including existence of optimal schedules.
The straightforward comparison uses identical expansion times. That comparison identifies a holding-cost difference, but it does not compare the two optimized classes: the least-cost sequential schedule and the least-cost joint schedule may choose different times and different numbers of expansions. The paper's endpoint arguments also rely on strict inequalities for optimal costs. A strict inequality for every fixed schedule does not automatically become strict after taking an infimum. Showing that the relevant optima are attained, or supplying an equivalent uniform argument, is part of the formalization burden. The fixed expansion charge bounds how many expansions a near-optimal policy can afford, but the interval lengths remain continuous variables.
Lean represents the attributes and cluster types by Fin 2, with index 0 corresponding to the paper's 1 and index 1 to its 2. The matrix entry a i j is capacity of attribute per unit of cluster . Times, demand, quantities, and costs are real. Replenishment times are strictly increasing, and a purchase at time contributes to the right-continuous excess capacity at . Policy validity requires no shortage and balance at cycle endpoints. The positive determinant records the nondegenerate, attribute-intensive cluster configurations needed by the paper's division formulas. The optimal costs are real infima over full policy classes, with no attainment built into their definitions. Holding cost is computed from the integral of actual excess capacity; defining it by the displayed closed forms would erase the content of Lemmas 1 and 2.
The theorem assumes continuous demand rates and the strict demand-ratio guard and throughout . The manuscript states Assumption 1 only for chosen leading intervals. Its Proposition 1 needs more: without the guard, taking , , , , , and on then permits one joint expansion at for at most 202 while every feasible sequential policy costs at least 300. Demand continuity supports the cost integrals; the strict guard makes every subinterval satisfy Assumption 1 strictly and keeps the appendix's sequential split feasible. Neither regularity nor this guard is claimed as a printed hypothesis of Proposition 1.
The appendix prints an extra outside the sum in its Case 2 holding-cost difference; the Lean milestone uses , consistent with the preceding integrals. The paper also prints in its last monotonicity sentence, while its fixed-cost parameter is defined on ; the milestone uses the model's interval. Useful contributions include formal integration identities for these finite replenishment schedules, existence and finiteness of the policy optima, and the comparison claims in the milestones.
Firms that hold a large, divisible asset (a commodity inventory, a block of shares, a stock of natural gas) often financed it with debt and must sell it over time to repay that debt. Without debt, the timing problem is classical: Karlin (1962) showed that a non-divisible asset facing independent prices should be sold the first time the price exceeds a reservation price. Debt changes the incentives in two opposite directions. Limited liability caps the shareholders' loss at zero, which rewards gambling on high future prices and delays selling. Bankruptcy also destroys the value of the unsold asset, an indirect bankruptcy cost, which rewards selling early to secure the debt payment. Ahn, Wang and Wu (SSRN 3472345, published in Operations Research 69(4), 2021, doi:10.1287/opre.2019.1961) solve the resulting dynamic program with Markov prices. This mission formalizes their central structural result: the optimal first sale under a single debt payment due before the end of the horizon.
A seller holds an amount of a divisible asset at the beginning of period , with . The selling price follows a Markov process: the law of given is a probability kernel , with finite conditional mean. Write for the expectation given the current price. The discount factor is , the per-period selling capacity is , and unsold asset is worthless after period .
The debt-free value solves, with ,
The debt-free critical price is .
Debt. A schedule , , is due at the end of periods , with maturity . The seller's working capital starts at and grows at rate . In period , a quantity is feasible if and . If no quantity is feasible, the seller is bankrupt and the equity value is . Otherwise
For a single payment (and otherwise), write and , with . The net effect of debt is
It is the value of limited liability net of the bankruptcy cost. The two critical prices are
Assume , a single payment at , a period before any sale (, ), and a price . Then , and:
After the debt-securing sale, the optimal quantities coincide with the debt-free ones. Moreover:
When , all three prices coincide.
In attack order:
Proposition 4 is the paper's headline. Under debt, the first sale follows a control band. Below the seller waits. Between the two critical prices, the seller sells exactly the quantity whose revenue covers the discounted debt; in that band a higher price means a smaller sale. Above the seller sells everything. Part (ii) separates the two economic forces by the sign of one number, . When the bankruptcy cost dominates, part of the asset is sold earlier than without debt. When limited liability dominates, selling is delayed and done all at once. The same structure underlies the paper's later results on threshold debt levels and general installment schedules.
The result is proved on paper but has not been formalized; the platform has no asset-selling, reservation-price or debt-constrained selling model. The mission contributes three things. The first is a finite-horizon Markov-price dynamic program with an explicit bankruptcy branch and limited liability, built on Mathlib's probability kernels. The second is Karlin-type debt-free stopping results for a divisible asset. The third is the full convexity argument behind the control band.
Part (ii) is signed algebra once footnote 4 is known; the work is in part (i). Because of the bankruptcy branch, is neither convex nor concave in general (Lemma 1(iii)). So the first-order reasoning that settles the debt-free problem, a linear objective in , does not carry over. Two facts reduce the optimum to three candidate quantities. The first is convexity of in below the debt-covering region, proved by backward induction together with the debt level. The second is linearity above that region. The induction must carry the debt level as a variable.
Every value function is integrated against a kernel. Before any identity between expectations can be used, and must be shown measurable and integrable, and both are suprema over a continuum of quantities. The strict inequality of footnote 4 is a separate induction: at every positive price.
Everything lives in the namespace AssetDebt.ControlBand.
Representation.
κ t p is the law of given , a Mathlib Kernel ℝ ℝ.Added hypotheses.
Excluded trivializations. is never defined by its closed forms (A.6), (A.8) or (A.9), which would make the goal an unfolding exercise. The critical prices are not existentially quantified: a price-dependent existential could be witnessed by thresholds read off the optimal action itself.
Infrastructure. A complete development needs measurability of suprema of kernel integrals, sup-shift lemmas for bounded intervals, and the backward-induction convexity argument. The debt-free results (Proposition 1) and the sup and measurability lemmas apply to other finite-horizon selling and stopping models. Contributions are welcome on any milestone, in particular on the measurability layer.
A seller can disclose privately known product quality, but credible disclosure costs money. In a market with competing sellers, disclosure changes both what consumers believe about a silent seller and how aggressively the sellers can price. Zhang and Li study this interaction when consumers are loss averse about quality: learning that a product falls below an expected standard hurts more than learning that it exceeds the standard helps. Their duopoly result says that stronger consumer loss aversion makes firms disclose more often and raises each firm's profit before quality is known, even though disclosure itself remains costly. The model and result appear in the SSRN preprint, §§3.1–3.3 and Proposition 2.
The paper first gives a monopoly benchmark and then analyzes two firms facing the same consumers. The duopoly question is distinct because a firm's disclosure affects the gap between its own product's perceived value and its rival's. The paper's Proposition 2 is a comparative statement about the equilibrium of this disclosure game, not a claim about a distribution chosen for a numerical example. The formalization targets the general quality distribution used in the paper.
Two symmetric firms, A and B, each have one product and a privately known quality . Their qualities are independent draws from a common cumulative distribution with a continuous, strictly positive density and . A firm may pay a common disclosure cost to reveal its quality truthfully. Otherwise, consumers infer quality from nondisclosure. With a common disclosure threshold , firms reveal quality above and remain silent at or below it. The inferred quality of a silent firm is the conditional mean .
When a product's quality is disclosed, a consumer values it at , where is its price. When quality is hidden, the consumer experiences a gain or loss relative to . With gain sensitivity and loss sensitivity , equation (1) gives utility
The degree of consumer loss aversion is . The paper assumes and also discusses the loss neutral benchmark . It uses two functions of the quality distribution,
They express the belief as and the expected gross utility of a silent product as , by equation (2). After disclosure decisions, firms set prices against homogeneous consumers. Under the paper's participation condition, the Bertrand outcome awards the firm with the higher gross consumer value the difference between the two values as revenue; the lower valued firm earns zero. Disclosure cost is then subtracted from the revealing firm's revenue. A symmetric equilibrium threshold means that both firms use the same and each firm's disclosure choice is a best response at every quality.
Fix and compare at fixed , with . For the corresponding symmetric best response thresholds , Proposition 2 asks for both strict comparisons:
Here is either firm's ex ante profit, averaged over its own quality before the draw. The result does not prescribe a numerical disclosure threshold or profit. The preprint's Proposition 2, p. 18, states the two directional claims; its proof on p. A7 gives strict signs.
The milestones preserve the paper's intermediate statements: the nondisclosure belief and expected utility, growth of , the two disclosure profits, the equilibrium equation (6) and its unique root in Claim 3, the ex ante profit identity (7), and the derivative of the integral . In particular, the game defined above determines the threshold and profit; equations (6) and (7) are claims to establish about those objects.
The result identifies a setting in which a consumer preference that lowers the perceived value of undisclosed goods can benefit competing firms. A stronger aversion to disappointed quality expectations changes firms' disclosure decisions and, through those decisions, the price differences available in competition. Proposition 2 gives a statement about each firm's expected profit, while the paper separately discusses cases in which an individual firm's realized profit can rise or fall. These distinctions are explicit in the preprint's §3.3, pp. 15–18.
The economic result is established in the paper; this mission seeks a machine checked Lean proof of its symmetric equilibrium claim and the paper's supporting identities. The statements here compile as open targets, and no proof is asserted to have been formalized. The work also develops reusable interval integral facts for conditional means and costed disclosure games with a general continuous quality density.
The central difficulty is the link between the original disclosure game and the integral expressions used in the paper's comparative statics. The profit of disclosing depends on the rival's random quality and its disclosure decision. The profit of silence depends on a belief formed from the same threshold that firms choose. A formula about a root of equation (6) alone does not establish that the root is a best response threshold in this game. Likewise, the compact profit expression (7) must agree with the profit obtained by integrating the game's conditional Bertrand margins and paying disclosure cost.
The general density also matters. A calculation for the uniform distribution in the paper's numerical footnote does not cover the paper's proposition. Establishing strictness requires keeping the positive density, the monotonicity assumption on , and the consumer participation domain visible throughout the development.
Lean represents and as real valued functions relevant on , together with a proposition asserting that is continuous and positive there, that on the interval, and that . Every expectation against is an interval integral against . The firms' independent, identical draws are encoded by using that same density separately for own and rival quality; no probability space is introduced. The standing assumption that is increasing is expressed as strict monotonicity on . The threshold lies in that interval, so division by cannot create a boundary statement about an undefined conditional mean.
Lean's utility function is gross of price. Its pricing layer represents the paper's homogeneous consumer Bertrand outcome by . The symmetric equilibrium predicate requires the silent product's gross utility to be nonnegative, and the strategic payoff identities carry the same condition. This is the bound in footnote 3 of §3.3, p. 15. The comparison fixes and increases ; it includes to cover the paper's loss neutral benchmark. The model's positive and assumptions are explicit in the economic statements. The milestone for exposes positivity on the full positive interval, beyond the page's explicit .
The symmetric equilibrium is defined by best responses in disclosure and the participation condition, with consumers using the conditional belief and firms receiving Bertrand revenue less disclosure cost. Neither the equilibrium threshold nor ex ante profit is defined by the simplified equation it is supposed to satisfy. Claim 3 gives a unique root of the threshold equation; an admissible root must also satisfy participation to represent an equilibrium. The paper's Claim 2 about the absence of asymmetric equilibria is outside this mission: Proposition 2 is framed for the symmetric equilibrium, and the printed argument for Claim 2 has an unresolved monotonicity step. Contributions to the model identities, equilibrium characterization, integral calculus, and goal proof are all within scope.
Suppliers often let buyers pay after delivery. If the buyer defaults, the supplier loses the credit sale revenue and may also face a financing cost from the resulting cash shortfall. Trade credit insurance transfers part of this loss to an insurer, but the insurer may possess information about the buyer that the supplier cannot observe. The insurer can use that information by canceling coverage before shipment. Yang, Bakshi, and Chen study how this option changes both the insurer's incentive to gather information and the supplier's decision to ship. Their Proposition 3 identifies a regime in which a simple cancelable contract recovers the entire value available to a centralized decision maker. Yang, Bakshi, and Chen (2021)
The question matters for contract design because a policy's deductible and refund affect different decisions. A deductible changes the supplier's loss if the buyer defaults. A refund changes the insurer's cost of canceling coverage. With a sufficiently attractive alternative sales channel, these terms can induce the insurer to reveal adverse credit information through cancelation while leaving the supplier fully covered when she ships. This mission states that claim precisely for the three-signal model in the authors' accepted manuscript. Accepted manuscript, §§3 and 6
A supplier receives an order for one unit at credit price . She may ship on credit or sell through an outside channel for . When the buyer defaults, the supplier receives no payment from the buyer. Her financing cost depends on end-of-period net cash flow :
Here is a cash flow threshold and is the marginal cost of falling short. At the time of contracting, the buyer's default probability is . An insurer can pay cost to monitor the buyer and observe one of three signals . Signal occurs with probability and has conditional default probability , where and . The paper assumes the outside channel is initially less attractive than the credit sale: . Accepted manuscript, §3 and Table 1
A cancelable contract is . The supplier pays premium ; if she ships while covered and the buyer defaults, the insurer pays the credit price minus deductible . Before shipment, the insurer can instead cancel coverage and refund . After this decision, the supplier chooses whether to ship. The contract must satisfy and . The insurer's monitoring decision compares its expected total cost with three alternatives: keep coverage without monitoring, cancel without monitoring, and decline the contract. The supplier's payoff includes her premium, any refund, default losses, and financing costs. Accepted manuscript, §§3 and 6, and Lemma B.1
The first-best payoff is the maximum available to a financially unconstrained planner who controls monitoring and, if monitoring occurs, can choose whether to ship at each signal. The paper's Proposition 1 identifies it as
The quantity is the value of using the signal to avoid credit shipments for which the outside sale is better. The supplier receives the full value of TCI when her payoff under a contract equals . Accepted manuscript, Proposition 1 and its proof
Proposition 1 gives the difference between the first-best and the no-insurance payoff:
This benchmark makes the phrase “full value” testable against a separate maximization over planner policies, rather than against a formula chosen to fit the contract. Accepted manuscript, Proposition 1, p. 11
The goal is Proposition 3. Under Assumptions 1 and 2, the paper's efficient-monitoring regime , and , it identifies
The insurer monitors and cancels at signals 2 and 3; the supplier ships only at signal 1. Her payoff equals , and no other admissible cancelable contract gives her more. Milestones establish the monitoring conditions, the first-best formula, feasibility and resulting decisions, attainment of the payoff, and the upper bound over other contracts. Accepted manuscript, Proposition 3, p. 18, and proof, pp. xi–xii
Proposition 3 identifies a regime where cancelation transmits the insurer's private credit information into the supplier's shipment choice. It gives exact contract terms, the induced actions at each signal, and a payoff that meets the centralized benchmark. The result thus pins down when the option to cancel coverage eliminates the loss from the two parties controlling different decisions. Yang, Bakshi, and Chen (2021), §6.2
The result is proved in the paper. The remaining formalization work is to prove the Lean statements, beginning with the finite three-signal model and ending with the optimality inequality over every admissible cancelable contract. A local prior-art search found no published declaration with this model and these conclusions. The finite contract and policy definitions can also support formal statements about the paper's other regimes, provided their distinct assumptions and timing rules are introduced explicitly.
The contract sits on several decision boundaries. In particular, the insurer's cost of monitoring can equal the refund, so replacing a weak incentive comparison by a strict one would discard the proposed contract. The supplier can be indifferent about shipping at signal 2 after coverage is canceled when . The paper's displayed threshold rule and its Proposition 3 proof make different tie choices there. The formal goal follows the proof's choice and records it in the model.
A second difficulty is showing global optimality. Computing the proposed contract's payoff alone does not compare it with contracts that generate different cancelation or shipping patterns. The upper-bound milestone covers all admissible cancelable contracts, while the first-best is defined from the planner's actual choices. The threshold cannot define shipping at the proposed contract, because its denominator is zero there. Accepted manuscript, equations (1), (6)–(9), and proof of Proposition 3
Lean uses real-valued prices, costs, probabilities, and payoffs, and a finite signal type with three members. Lean indices correspond to the paper's signals . The prior is defined by Table 1's weighted average . Standing hypotheses state nonnegative signal probabilities summing to one, ordered default probabilities in , , , and positive monitoring cost. The explicit additions and make financing cost nonnegative and meaningful. Assumption 1, Assumption 2, and remain separate hypotheses.
Decisions are defined by payoff comparisons. Shipping under coverage uses the weak inequality in (1); cancelation and shipping after cancelation use the strict tie choices in the proof of Proposition 3, equations (64)–(66). The first-best is a maximum over no-monitoring choices and all shipping policies after monitoring. Optimality compares the supplier's payoff with every valid cancelable contract that induces monitoring and actual cancelation at some signal. Defining the first-best as the desired formula, restricting competitors to contracts with the proposed policy, or using division by a zero threshold denominator would empty the intended claim.
The development needs finite sums, real inequalities, maxima, and a representation of sequential contract decisions. Contributions proving the monitoring characterization, planner value, feasibility, payoff identity, and global upper bound are within scope. The model's finite signal and contract interfaces may be reused in further results of the paper.
A firm that needs outside money to start a project knows more about the project than its investors do, and it can usually choose how much of that knowledge to reveal before raising funds: which audits to commission, which metrics to report, how informative an analyst's report will be. The security-design literature studies the security side of this problem, meaning what claim to sell given the information the investors have (Innes, 1990; Nachman and Noe, RFS 1994). The Bayesian persuasion literature (Kamenica and Gentzkow, Bayesian Persuasion, AER 2011) studies the information side, meaning what to reveal when a sender can commit to a signal in advance.
M. Szydlowski, Optimal Financing and Disclosure (Management Science 2021; working paper of March 2017), puts the two together. An entrepreneur who cannot finance a project on the prior alone commits to a disclosure policy so as to maximize her expected payoff, subject to the investors' competitive pricing. The main answer is simple and testable: the optimal policy is a pass/fail test, and the passing standard is set exactly where investors break even. This mission formalizes that answer and the chain of lemmas the paper's appendix uses to reach it.
The project pays . The investment cost is . The entrepreneur sells a security with payoff to competitive investors. is continuous, , and both and the residual are weakly increasing (equity, debt and options all qualify). The common prior over has a continuous density with support .
A posterior is a probability measure on . At posterior the security sells for (1), and the project is financed iff (2). If it is financed, the entrepreneur receives the residual, a private benefit , and a share of the excess cash, so her payoff (3) is
A disclosure policy induces a distribution over posteriors. By Kamenica and Gentzkow's equivalence, the feasible are exactly the Bayes-plausible ones, those whose mean posterior is the prior, (5). The entrepreneur's problem (6) is to maximize over Bayes-plausible . The threshold policy with cutoff reveals only whether . With probability it produces the posterior on , and otherwise the posterior on ; this is (17).
Throughout, the project cannot be financed without disclosure: (§4).
There is a threshold at which the financing constraint (20) binds,
such that the threshold policy with cutoff is Bayes plausible and attains the maximum of over every Bayes-plausible . The hypothesis is added, as explained under Formalization scope.
Proposition 1 gives disclosure a concrete shape: certify whether cash flows clear a bar, and say nothing more. The bar is the lowest one at which investors still break even, so the entrepreneur maximizes the probability of financing. The paper's later results build on it: the choice of the optimal security (Proposition 4), extensions to general utility (Proposition 5), and comparative statics of the threshold in the security's information sensitivity (Propositions 2–3).
The result is proved on paper but has not been machine-checked. A formalization adds three things. It checks a proof whose central step goes through an infinite-dimensional linear-programming duality (Levinson, 1966). It pins down hypotheses the printed statement omits, notably . And it provides a reusable Lean account of Bayesian persuasion over a continuum of states, with distributions over posteriors as measures on the space of measures.
The obvious argument is a bang-bang argument. Fix the probability of financing, put as much high-posterior mass as possible on the best states, then optimize over . Each step hides a gap. The reduction to two posteriors (Lemma 1) needs barycentres of a measure on the space of measures. The fixed- problem is a linear program over densities with a pointwise cap , so finite-dimensional LP duality does not apply. The paper uses an infinite-dimensional duality theorem plus a compactness lemma under an extra equicontinuity restriction (32).
Monotonicity of the value in is where the printed argument fails in general. The marginal contribution can be negative near the cutoff when . In that case a slack threshold beats the binding one, and the binding threshold is not optimal. A second trap is that the binding root of (20) need not be unique: for debt, every cutoff above the face value can solve (20) with equality. " solves (20)" therefore cannot by itself be the content of the theorem.
The state space is , and and are read only on . The prior is Lebesgue measure on with density . Support is encoded as positive prior mass on every nondegenerate subinterval. Posteriors are arbitrary measures on , and a distribution over posteriors is a measure on the space of measures with Mathlib's Giry σ-algebra. Bayes plausibility is: is a probability measure, almost every posterior is a probability measure, and 's monadic join is the prior. Posterior expectations are integrals over , written through positive and negative parts so that they are measurable in the posterior. As a result is never a junk value. Ties in the financing rule go to financing (). "Increasing" means weakly increasing. The fixed- problems range over integrable densities with pointwise, which encodes . The equicontinuity restriction (32) is dropped; it serves only the compactness Lemma 2, which is not formalized.
Two hypotheses are added, each disclosed in the items that carry it:
The goal quantifies over all Bayes-plausible distributions over posteriors, and its threshold is pinned by optimality, not only by solving (20). A version restricted to threshold or two-point policies, or one whose is any root of (20), would be a different and weaker theorem. Optimality is stated as "an optimal policy", since the optimum is not unique.
Not formalized: Lemma 2 (compactness); the continuity and differentiability parts of Lemma 5; the second case of Proposition 8 (); and the paper's later Propositions 2–6, 9 and 10. The general definitions of Bayes plausibility and of the reveal-a-cell policy are stated for an arbitrary measurable state space and are reusable for other persuasion missions. Contributions are welcome on any milestone. A barycentre construction for measures on the space of measures (Lemma 1) and a bathtub principle for densities under a pointwise cap (Proposition 7) are of independent use.
Wind and solar generation have near-zero marginal cost. In a wholesale electricity market where prices are set by the marginal producer, adding such capacity displaces expensive conventional generation and lowers the spot price: the merit-order effect. Regulators and system planners rely on this effect when projecting the price impact of renewable expansion, and empirical studies of European markets report it.
Most electricity, however, is not traded only in the spot market. Producers and retailers hedge in forward markets before demand and wind output are known, and forward trading changes how producers with market power behave in the spot market (Allaz and Vila, 1993). Peura and Bunn (Management Science, 2021) ask what happens to the merit-order effect once this channel is included. Their answer is that, when wind output is variable and positively skewed, additional wind capacity eventually raises the expected spot price and the forward price. This mission formalizes that statement, Proposition 2 of the paper, together with the equilibrium characterization it rests on.
There are two conventional producers with constant marginal cost , a set of price-taking wind producers with total capacity and zero cost, price-taking retailers who resell at a fixed retail price , and an elastic industrial demand , where is the spot price.
Two random quantities are drawn on a probability space: the total retail demand , bounded, and the wind yield , so that available wind output is . They are independent and both have positive variance. Write for the mean, variance and third central moment of , and for those of . The coefficient of variation of the yield is and its normalized skewness is .
Trading has two stages.
With and , the spot equilibrium is and (Lemma 1). The forward-spot equilibrium is and for explicit expressions in the parameters, the moments, and (Theorem 1).
If
then an equilibrium exists at every capacity , and there are thresholds and such that along every equilibrium selection
The value of comes from the paper's proof; the proposition itself only asserts that some works.
The result. Proposition 2 isolates a mechanism by which two pro-competitive forces, low-cost capacity and forward trading, can combine to raise prices. Variable and skewed wind output increases the risk that a producer is caught with a large forward position when wind is high and the spot price is low. Producers therefore sell less forward, which by Lemma 1 lowers their spot output and raises the spot price. For large enough capacity this forward effect outweighs the merit-order effect. The condition for the reversal involves only and .
Formalizing it. The result is proved in the paper but has no machine-checked proof. In a formal development the equilibrium has to be defined through the participants' optimization problems, not through the closed forms. Theorem 1 then has to show that this optimization-defined equilibrium exists, is unique, and equals the closed form. The polynomial coefficients have to be checked: the printed has a misplaced parenthesis, and the printed is off by a factor of . Both are corrected and disclosed in the milestone statements. Neither affects the conclusion.
The goal combines three layers. The probabilistic layer computes means, variances and covariances of products of independent bounded random variables. These computations produce the third central moments and justify replacing the utility of each participant by an explicit quadratic in its own position. The game-theoretic layer has to show that each first-order condition gives a global optimum, which needs strict concavity, and that the producers' best responses, each computed against a clearing price that itself depends on the deviation, meet at a unique point. The analytic layer studies the rational function of , whose derivative's numerator is a quartic with coefficients that are themselves polynomials in eleven quantities.
A tempting shortcut is to define the equilibrium by its closed form, which reduces the goal to a sign argument on a polynomial. That shortcut removes Theorem 1 entirely and is excluded here. A second tempting reading treats the forward price as fixed when a producer deviates. That makes producers price takers in the forward market, which is a different game whose equilibrium is not .
The market parameters are a structure with fields a, c, pR, lam (, a Lean keyword) and NR : ℕ; the retailers are indexed by Fin NR. The demand and the yield are real functions on a probability space , and the capacity is a separate real argument, so the joint law stays fixed as varies. The standing assumptions, a hypothesis of every model theorem, are: and are measurable and independent; is bounded and at every sample point; ; ; and . The last two come from the paper's statement that demand and supply are uncertain in the forward market. Third moments are central. The footnoted conditions and are not assumed, since the goal holds without them.
The spot inverse demand is the interior branch of the paper's , used for all and all realizations, with quantities ranging over the reals. This is what Assumption 1 (no blackouts or curtailment) licenses and what the paper's proof differentiates. The statement is therefore about the model with linear inverse demand. At realistic parameter values the turning point can lie where Assumption 1 fails for some realizations, so its economic reading inside the no-curtailment region is the paper's interpretation, not part of the theorem.
The forward-spot equilibrium is a predicate built from optimization alone: retailer optimality over all real positions, clearing, and each producer's optimality against every deviation evaluated at that deviation's own clearing price. The closed forms (13)–(16) and the quartic's coefficients live in a separate definition file used only in milestone conclusions. The goal imports only the model. The goal also contains an existence conjunct, so the statement about equilibrium selections is not vacuous.
A complete development needs moment calculus for bounded independent random variables (variance and covariance of products, third central moments), maximization of concave quadratics, and single-crossing arguments for real polynomials. The moment computations and the mean-variance optimization of an affine position are reusable beyond this mission. Contributions are welcome at every milestone, including partial results.
Networks of autonomous sensors — machines on a factory floor, vehicles, devices in the Internet of Things — each measure a common environment with their own noise and can improve their estimates by asking other sensors for theirs. Communication capacity is limited, so each sensor must decide whom to ask, and the answer it receives is useful only to the extent that it understands how the other sensor turns measurements into estimates. Saghafian, Tomlin and Biller (SSRN 3124417, version of October 16, 2020; published in Manufacturing & Service Operations Management, 2021) model this as a dynamic target-selection problem and ask which communication network forms in the long run. Their abstract leads with the answer: each sensor eventually settles on a constant target set, which is sample-path dependent. With known, pairwise distinct qualities this target set is a single sensor (Proposition 4, p. 21). This mission formalizes that result.
There are sensors . Sensor has a quality : its measurement of the state has noise variance . Sensor starts with initial familiarities with each other sensor , the precisions of its initial Gaussian beliefs about 's inference parameters. A sample path is the sequence of realized states, an arbitrary sequence of reals.
The familiarity function of with in period is a function . It starts at
In period , after is revealed, sensor targets the sensor of least signal variance
with ties broken toward the lower index (footnote 11). Writing if and otherwise, the familiarity grows by the stickiness factor:
The long-run contacts of along are (Definition 2)
In Lean these are Instance (q, v, w), psi1, sigma2, stick, lowArgmin, the joint recursion fam/target, count and longRunContacts in IoTFusion.KnownQuality.
If the qualities are asymmetric ( for , Definition 3), then for every sample path
No hypothesis on the state process is involved: the statement holds path by path.
Supporting items: for (long_run_contacts_nonempty); each sensor eventually targets one fixed sensor (eventually_constant_target, the wording of p. 5); and the rank-one precision identity (EC.66).
Proposition 4 says that, with known and distinct qualities, the long-run communication network is a functional graph — every sensor has out-degree one — although which graph forms depends on the realized states, and a sensor's eventual partner need not be the highest-quality sensor available. The paper builds on it its description of the long-run network as a random directed graph (Propositions 5–6) and its managerial discussion of early-period "momentum" in familiarity.
The result is proved in the paper; nothing in it is machine-checked. The work here is a formal proof of the deterministic core, including the existence half , which the printed proof (p. ec22) does not give: it shows only .
Every statement is elementary in isolation; the difficulty is that the target sequence is defined by a feedback loop. The target of period depends on familiarities, which depend on all earlier targets, which depend on earlier states. Statements about "infinitely often" therefore cannot be reduced to the behavior of any single function of fixed in advance.
The tempting argument "the highest-quality sensor eventually wins" is false: a sensor that becomes familiar early with a lower-quality partner can keep choosing it forever, so no fixed candidate for the unique contact exists. The uniqueness argument must instead compare two putative long-run contacts with each other, using a familiarity threshold that does not depend on the familiarity with the worse one (Lemma 2), and the existence half needs a separate counting argument over the finitely many possible targets.
Fin n (0-based) with on the existence statements; for there is no other sensor and .fam P i s k is .Filter.Tendsto … atTop atTop; is Set.ncard; asymmetry is Function.Injective q.Set.ncard bookkeeping would be reusable.Firms increasingly delegate the generation of new concepts (product designs, advertising campaigns, engineering prototypes) to outside providers such as design agencies and engineering consultancies. The client cannot dictate how hard the provider works; it can only decide when to stop asking for new solutions. Two practices are common. Under a flexible stopping policy the client keeps the right to stop or continue after each submitted solution. Under a committed stopping policy the client commits in advance to stop, and pay, as soon as a feasible solution arrives. Classical search theory says that keeping options open is never harmful, so flexibility should dominate. Yet committed contracts are widespread in practice.
Rahmani and Ramachandran (2021) explain this by two features that the classical benchmarks omit: a deadline on the number of rounds, and a provider who adjusts its effort from round to round in response to the client's policy. In two benchmark settings, an unlimited number of rounds or a fixed provider effort, flexibility (weakly) dominates (their Lemmas 1 and 2). With a deadline and strategic effort, commitment can be strictly better, and the paper characterizes exactly when.
A client delegates a project of rounds to a provider. In each round in which the client asks for a solution, the provider chooses an effort , at cost or , and submits a solution of quality . The client pays an evaluation cost for each submitted solution. When the project stops with a feasible solution (), the client implements the best solution received and pays the provider a fixed payment ; if no feasible solution is found by the deadline, nothing is paid.
Quality under effort has distribution function
where is the provider's capability: with probability the solution is infeasible (), and otherwise it has density on . The expected quality is . The standing assumptions are
Under the committed policy, the project stops after round 1 if . Under the flexible policy, after a feasible the client compares with the expected value of a second round and stops when stopping is at least as good. The provider anticipates this and chooses its efforts by backward induction: round-2 efforts , (after a feasible first solution), (after an infeasible one), then round-1 efforts , . Write and for the client's equilibrium expected profits under the two policies.
Fix satisfying the standing assumptions and a payment . There exist thresholds and such that for all and ,
Commitment is strictly better exactly for an intermediate range of evaluation costs, and never when the payment is below . The thresholds are left existential, as in the paper.
Proposition 4 reverses the conventional wisdom that retaining decision rights cannot hurt the decision maker. The mechanism is strategic: flexible stopping lowers the provider's expected reward for a good first solution, because the client may continue the search instead of accepting it, and so it weakens the provider's first-round effort (Proposition 3). When the payment is in , commitment induces high first-round effort that flexibility does not, and whether this outweighs the option value of a second round depends on the evaluation cost. The result gives contract designers in innovation procurement a concrete criterion in terms of evaluation cost, capability and payment.
The paper's proofs are in an online appendix. No machine-checked version of any result in this model exists. The mission produces a formal model of a dynamic principal–agent stopping game with an atom-plus-density quality law, a verified threshold structure for the client's stopping rule, and the full equilibrium effort characterization, all of which carry over to related delegation and contest models.
The goal compares two equilibrium profits, each determined by a nested backward induction in which the provider's round-1 effort depends on the client's stop rule, which in turn depends on the provider's round-2 effort. The obvious approach, comparing the two policies at the same efforts, proves only Lemma 2 and points the wrong way. The comparison must instead track which of the effort regimes of Proposition 3 each policy induces, as a function of and . The profits are piecewise in (the stopping threshold is zero for large ), and the claim that the strict-improvement set in is a single open interval requires a monotonicity argument across these pieces, uniformly in . The case must be shown to give no improvement at all.
The Lean development models exactly the two-round game (), the case the paper analyzes in §4. Effort levels form a two-element inductive type; parameters form a record, with and separate arguments. The standing assumption is written cross-multiplied; is the reading that costs are non-negative. The paper's Stieltjes integrals are Bochner integrals of against the density over the open ray ; the atom at appears in the separate terms, so no payment is charged on infeasible solutions. Ties are broken as on the page: the provider takes high effort, and the flexible client stops. The paper's restriction to payments "neither too high nor too small" (Lemma A-1 of its online appendix) is not available; every statement is posed for all , for which it remains true. Evaluation costs satisfy .
The model defines no stopping threshold and no effort in closed form: the stopping threshold is a theorem (Proposition 2), is computed from the provider's objective, and the goal compares profits at the efforts the model computes, not at efforts supplied as arguments. A formalization that defined , fixed , or compared the policies at exogenous efforts would make the milestones trivial or prove a different theorem, and is ruled out.
A complete development needs integrals of polynomial-times-exponential functions on rays, the closed forms of the round-2 values, and finite case analysis over effort profiles. Contributions to the comparative statics (Propositions 2 (c), 3 (c)) are welcome independently of the goal.
Not formalized: Proposition 4 (b) (its half fails under the main-text model, e.g. at , , , , , , ); Lemma 1 (infinite horizon); Proposition 1 (general finite ); Proposition 5 (dependent solutions); Propositions 6–8 (endogenous payments); the numerical study.
Online retail platforms such as Amazon, Alibaba's Tmall and JD.com host thousands of third-party sellers and observe every customer interaction with each of them. From these interactions the platform learns about market demand far better than any single seller can, and it sells or gives away part of that knowledge through analytics tools (Alibaba's Business Advisor is the example in the source paper). The platform earns a commission on every seller's revenue, so it cares about the sellers' total profit, and it has to decide what each seller is told.
The classic literature on information sharing in oligopoly points the other way. Gal-Or (1985) showed that Cournot competitors facing a common demand shock never voluntarily pool their private demand signals: shared information makes their strategies more correlated, and the resulting competition destroys more value than the better forecasts create. Li (2002) and others refined the conditions. Liu, Zhang and Zhang (Manufacturing & Service Operations Management, 2023; SSRN 3258109) change who decides: the signals belong to the platform, which chooses what each seller learns in order to maximize its commission. Their headline result for the unconstrained ("asymmetric full sharing") format is that the platform shares everything it knows, without any added noise, but only with a limited number of sellers, and that number is determined by the substitution between products alone.
There are sellers of substitutable products. Given quantities , seller 's price is
where is a common demand shock with prior variance . The platform observes, for each seller , a signal with , , independent of everything else.
A noise matrix with entries in is the platform's sharing strategy. Seller receives the noisy copy , independent, for every with ; is truthful sharing and means is withheld from seller . Seller 's information is the -algebra generated by what he receives.
Each seller chooses a quantity measurable with respect to his information to maximize his expected profit , where is the platform's commission rate. A Bayesian equilibrium under is a profile of such strategies from which no seller gains by deviating. The platform's expected profit is , and it chooses before the signals are realized.
Under Asymmetric Full Sharing (AFS) each seller receives all signals with one common noise level (for all ), and the levels may differ across sellers. The benchmark is no sharing, for all , with platform profit .
Let . Among all AFS noise matrices in and all equilibria, an optimal strategy is to share truthfully with sellers and nothing with the others, where
The platform and every seller do weakly better than without sharing, and every optimal truthful group has size or .
The result separates two levers of information design, precision and audience, and shows that in this linear-Gaussian Cournot setting only the audience matters: the platform never degrades a signal, it only chooses how many sellers see it. The optimal audience size depends only on the substitution parameter once the market is large, and equals one seller when products are perfect substitutes. This reverses the Gal-Or no-sharing result by changing who decides, and it explains why a commission-earning platform may rationally treat its sellers asymmetrically, which is the tension the paper's later sections on fairness and privacy constraints study.
The paper's proofs are in an online appendix. No part of this model has a machine-checked proof. The mission produces a reusable Lean layer for Bayesian games with designed Gaussian signals: information -algebras generated by noisy copies of shared signals, Bayesian Nash equilibrium over square-integrable strategies, and its characterization by first-order conditions in conditional expectations. Mathlib has Gaussian measures, conditional expectation and independence, but not the projection formula for jointly Gaussian vectors that eq. (5) needs.
The closed forms are routine once one assumes that equilibria are linear in the received average signal. The difficulty lies in what that assumption skips. First, eq. (5) is a statement about conditional expectation with respect to a -algebra generated by correlated Gaussian variables; it needs the Gaussian conditioning (projection) theorem, not a computation with densities. Second, the goal quantifies over all equilibria, so existence and uniqueness of the equilibrium must be proved for every noise matrix, including those with infinite entries; the paper solves the first-order condition and never discusses uniqueness. Third, Proposition 1 is an optimization over : the platform's profit is not concave in the noise levels, and the endpoint property for one seller (with the others fixed at arbitrary levels) is the step that rules out partial sharing. Restricting attention to truthful groups from the outset assumes away exactly this step.
All declarations live in the namespace RetailInfoShare.AFS, with one definitions file RetailInfoShare.AFS.Model. Conventions:
gaussianReal 0 σ), as eq. (3) of the paper requires.ℝ≥0∞; a signal with never enters the receiving seller's information -algebra.Fin N, so the paper's sellers are indices .Out of scope: the AIS half of Proposition 1, Proposition 3 and Lemma 2 (privacy-constrained sharing), the symmetric formats of §5, the pricing mechanism of §6, and the appendix extensions. Contributions of general infrastructure are welcome: the Gaussian conditioning theorem in Mathlib form, and existence and uniqueness of equilibria in linear-quadratic Bayesian games with Gaussian information.