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?
A firm with two operating divisions may let one division buy shared productive capacity while the other uses part of it. The firm wants capacity to be chosen for its total value, but each manager is judged by a divisional performance measure. If capacity is reallocated after revenues become known, the investing division may anticipate surrendering part of the benefit from its investment and buy too little. Dutta and Reichelstein study whether capacity rights, a transfer price, and depreciation can align these choices even when the managers put different weights on different periods. Their negotiated gatekeeper contract addresses the shared-capacity setting without fixing the revenue functions to a quadratic family (Dutta and Reichelstein, CESifo Working Paper 7968, §§2–4).
The main result is Proposition 3 of the November 2019 working paper. The later journal article appeared in Management Science in 2021; the statements and page numbers here refer to the working paper, whose PDF is the source of this mission. The dedicated-capacity rule and the symmetric-rights result are separate results in the same paper. This mission focuses on the negotiated rule for fungible capacity.
There are two divisions, indexed by , and operating periods. At the start, capacity costs per unit and can serve either division in each period. After the period's joint revenue shock is observed, the divisions choose nonnegative outputs with , where is installed capacity. Division earns revenue and incurs variable cost . The shocks have the same joint law in every period; shocks within a period may be correlated across divisions. The combined contribution margin is the maximum of the sum of the two margins over feasible outputs. The stand-alone value is defined similarly for one division.
The firm's cost of capital is , so its discount factor is . Its efficient capacity maximizes the net present value
The user cost of capacity is . A depreciation schedule creates a period charge per unit, where . Under the annuity rule, in every period. Division 1 is assessed the charge for all installed capacity. Division 2 is evaluated on profit and Division 1 on residual income.
The divisions can negotiate a right for Division 2 before investment. Division 1 then installs the total capacity, retaining units for itself, and receives a fixed payment each period. The stated transfer price for an output quantity is . After the shocks are observed, the divisions can renegotiate their initial rights and operate at the joint maximum . Division 1 receives a fraction of the renegotiation surplus; Division 2 receives . The default without an advance agreement is (working paper, pp. 20 and 25).
The first targets identify the marginal values of stand-alone and fungible capacity. For positive , the paper's shadow price is the derivative of the combined margin, and Lemma 2 characterizes an interior efficient capacity by
A further milestone states the marginal condition for Division 1's best response to a negotiated right . The final milestone asserts that some makes Division 1 choose for itself. These are the derivative claims, Lemma 2, equation (33), and the existence claim in the paper's proof of Proposition 3 (working paper, pp. 19, 36, 40, 43–44).
Proposition 3 is the mission goal. When the paper's positive dedicated-capacity condition holds for both divisions, there is a right and a fixed payment such that the transfer rule
makes a best response for Division 1 in every period. A best response exists at the default, and both divisions weakly prefer the contract to every default best response. Thus the firm installs and subsequent production is efficient. Period-by-period optimality supplies the paper's strong goal congruence for any nonnegative weights that managers place on the periods (working paper, Proposition 3, p. 26).
The result gives a way to assign initial rights over a shared asset without requiring the downstream division to fund its own share of the investment. The negotiated rights influence the upstream division's investment incentive; the fixed payment makes the resulting agreement acceptable to both sides. The annuity charge keeps that incentive aligned in each period, so it does not depend on a particular managerial discount schedule. The paper's comparison with a rule in which only the upstream division initially holds rights identifies the associated underinvestment problem (working paper, pp. 24–26).
The paper proves the result mathematically; this mission asks for a Lean proof of its precise claim. The development also yields reusable definitions of capacity-constrained value functions, their marginal values, renegotiated surplus shares, and expected residual-income best responses. The claims of Proposition 3 and its listed milestones are formalization targets here, not results already machine checked by this mission.
The obvious attempt is to give Division 1 all capacity rights and charge it the annuitized cost. With renegotiation, it then anticipates receiving only a share of the extra joint margin from its investment. Its marginal payoff mixes the stand-alone margin and the joint shadow price, so that right assignment need not produce . The gatekeeper result also needs a right strictly below and a payment that makes both divisions accept the agreement. The payment changes the distribution of surplus but does not change Division 1's marginal choice. The source's proof separates these two demands (working paper, pp. 24 and 43–45).
The Lean model uses real capacities, outputs, payments, costs, and values. Feasible capacities and outputs are nonnegative. The two revenue shocks have one compactly supported joint probability law; this represents the stationary period law while allowing correlation across divisions. Capacity and output optima are defined by maximization, and derivative equations are statements about those optima. Every assertion about an optimal output applies to any maximizer. The model never obtains the desired capacity by defining it as a solution of a first-order equation.
The paper assumes increasing, concave revenue with marginal revenue increasing in its shock. The Lean standing assumptions make concavity strict so the paper's uniqueness assertions are valid, and add differentiability, continuity of marginal revenue, joint continuity, to support integrability of the real-valued expectations and well-posed derivatives. The probability law generalizes the paper's density notation. A nonnegative cost of capital, at least one period, a nonnegative depreciation schedule totaling one, and are explicit. The quantity is a one-sided derivative on nonnegative capacity; for positive capacity the derivative claims identify it with the paper's maximizer formula. No sign restriction is imposed on beyond the source's positive-margin-at-zero condition. The annuity schedule gives the same capital charge in every period, and Division 1 bears the charge on all installed capacity.
A complete proof will need value-function continuity and differentiability, integrability under the compact shock law, the interior optimality characterization, and the capacity-right existence and surplus allocation steps. Those facts can be reused for other capacity allocation and transfer-pricing models. Contributions to the listed derivative, shadow-price, best-response, and contract targets are all within scope.
A firm may motivate a worker with pay, with a supervisor's praise, or with the threat of a supervisor's disapproval. A wage floor changes the mix: when base pay cannot fall, a worker can receive a rent above the value of an outside job. That rent affects whether the firm finds praise or scolding cheaper than a bonus. Dur, Kvaløy, and Schöttner study this question in a binary-effort principal–worker–leader model and characterize the least-cost style when the wage floor binds Dur, Kvaløy & Schöttner (2021), §§3–4. The model is useful for isolating how labor-market conditions affect a firm's choice of nonmonetary incentives, while keeping the worker's effort unobservable and output verifiable.
The worker chooses high or low effort. High effort costs and gives high output with probability ; low effort costs nothing and always gives low output. The principal offers a contract : worker base salary , bonus after high output, and fixed wage for the leader. The worker's reservation utility is , and the base salary must meet a wage floor . The leader's reservation utility is . The principal wants high effort and minimizes expected wage cost Dur et al. (2021), §§3–4.1, pp. 7–11.
The leader acts after observing output. Praise gives the worker value and costs the leader after high output or after low output. Scolding costs the worker and costs the leader or , according to output. The model assumes , , and . The leader is selfish and follows the announced style. The six leadership styles are monetary incentives alone (), praise only after high output (), praise after either output (), scolding only after low output (), scolding after either output (), and praise after high plus scolding after low output () Dur et al. (2021), §§3–4, pp. 7–10.
A contract is feasible for a style if high effort is at least as attractive to the worker as low effort, the worker's expected high-effort utility reaches , the base salary reaches , and the leader's wage covers plus her expected leadership cost. Strict preference between two styles means that a feasible contract of the first costs less than every feasible contract of the second. A style is optimal when one of its feasible contracts attains a weak minimum against every feasible contract of all six styles. Wage-setting is noncompetitive when Dur et al. (2021), §§4.1–4.5, pp. 11–18.
The milestones first give attained minima for the monetary, , , , and styles. For example,
The comparison milestones characterize when , , , and cost less than alternatives, establish that is dominated, and split condition (U) into the two tests used by the final classification Dur et al. (2021), §§4.1–4.4 and Online Appendix A, pp. 11–17, 34.
Write , , , and let condition (U′) be
When , the goal identifies an optimal style among all six: if and , monetary incentives; if , when and (U′), otherwise ; in the remaining case, when (U′), otherwise monetary incentives Dur et al. (2021), Proposition 2, p. 18. “Optimal” permits ties: a style named by the proposition need not be unique.
Proposition 2 gives an exact classification of the principal's least-cost incentive arrangement in the binding-floor regime. It distinguishes the expected cost of leadership actions from their effect on the worker's incentive and participation constraints. In particular, the rent can make conditional scolding attractive to the principal even though the worker dislikes it; whether combining scolding with praise helps is governed by separate thresholds Dur et al. (2021), §§4.3–4.5, pp. 15–20.
The economic result was proved in the paper. This mission seeks machine-checked proofs of the stated model and classification, including the cost minima and preference lemmas needed to support it. The proposed Lean declarations are currently open theorem statements; successful compilation of those statements does not constitute a proof. The model's reusable contribution is a small contract interface that represents outcome-contingent nonmonetary actions, worker incentive compatibility, both parties' participation, and a wage floor without assigning a closed-form cost to a style.
The bonus required for high effort and the base salary required for participation respond differently to an action. Praise after high output can replace part of the bonus; scolding after low output can also reduce the bonus but may require higher base pay. A direct comparison of the bonus changes misses the participation constraint, especially where the wage floor begins or ceases to bind. A complete classification must compare attainable costs for every style, including and , and handle equal-cost boundaries rather than assuming a unique minimizer Dur et al. (2021), §§4.2–4.5.
Lean represents all parameters and payments in . A style is a pair of actions selected by output. The worker's low-effort outcome is always low output, so the low-output action affects both the shirking payoff and the high-effort expected payoff. Feasibility contains exactly the high-effort incentive constraint, worker participation, , and the selfish leader's participation constraint. There is no extra constraint on the bonus, no independent floor on total compensation, and no leader incentive constraint. The paper's limiting convention is outside the real-valued model; the goal concerns a finite, binding floor.
The principal's preference for inducing high effort is fixed as the paper assumes; output value and the comparison with low-effort profit are outside this contract-minimization model.
The standing assumptions include positive effort cost, , positive action values and costs, the ordering of action costs by output, , and . The goal quantifies over all six styles and over their feasible contracts. It is not a comparison of numbers assigned to styles by definition: the closed-form costs are conclusions of separate attained-minimum milestones. Strict preference is reserved for the comparison lemmas; Proposition 2 asserts weak cost-minimality so that boundary ties are covered. The printed Lemma 4 has a false literal reading; its milestone is marked as corrected and formalizes the preceding paragraph's comparison of against monetary incentives, , and . Lemma 1's “if” is strengthened to an equivalence justified by the displayed costs; Lemma 3's equivalence is stated for all real wage floors, where both sides are false in the competitive regime; the §4.4 comparisons of with and with are stated without the paragraph's introductory suppositions "(U) holds" and "(F) holds", which the cost identities do not need. These readings are documented item by item in the audit notes.
Contributions are welcome on attained-cost lemmas, comparisons between styles, arithmetic of the threshold conditions, and the final case analysis. The contract definitions can also support separate work on the paper's competitive wage-setting proposition; the repeated-game and socially motivated-leader extensions require further model structure.
Scientific conclusions based on a fitted model can move when an analyst changes the model while keeping its fit to the observed data nearly as good. Coker, Rudin, and King call the resulting range of conclusions a tethered hacking interval. The range measures the sensitivity of a reported statistic to the choice among models under a fixed loss tolerance. Their 2021 paper develops this idea for several inference tasks, including treatment effects in least-squares regression. In that setting, a reader can ask how far the estimated treatment coefficient could move among all models whose residual sum of squares stays below a chosen threshold.
The motivation is concrete: two analysts can use the same observations and the same linear model class, yet choose different coefficient vectors that fit acceptably. A single least-squares coefficient reports the best-fitting vector, but it does not show the range admitted by a specified relaxation of the fit criterion. The interval makes that range explicit. Its endpoints depend on the data and the tolerance rather than on a distributional approximation for an estimator.
There are observations and confounder covariates. The confounder design has row , the outcome vector is , and indicates whether observation received treatment. The full design is . A coefficient pair predicts . Its quadratic loss is
For a fixed tolerance , problems (14) and (15) maximize and minimize over all coefficient pairs with . The two extrema are the endpoints of the tethered hacking interval for the treatment coefficient. The paper gives an average causal treatment-effect interpretation under overlap, SUTVA, and conditional ignorability. Those assumptions concern the interpretation of the coefficient; the algebraic optimization result itself uses only the finite data and the quadratic loss.
Several least-squares quantities describe the endpoints. Write for regression on confounders alone, for regression of the treatment indicator on confounders, and for regression on the full design. Let be its treatment coordinate and the corresponding diagonal entry of . In this mission, , the minimum loss for the constrained problems.
The goal is the complete solution-set statement of Theorem 1, p. 11. When the full design has linearly independent columns and , the unique maximizer and minimizer are, respectively,
The intermediate targets are both halves of Theorem 4, pp. 13–14, which gives the maximizer and minimizer of any nonzero linear prediction on a least-squares loss sublevel set, followed by the separate maximization and minimization formulas (16) and (17) of Theorem 1. Theorem 4 uses and ; the two solutions are . Here denotes the entire design of the general regression, so its SSE is the residual loss of that design.
The theorem gives both endpoint values and the full coefficient vectors that attain them. It shows how the tolerance controls the distance of an endpoint from the full least-squares estimate: the half-width is . That quantity allows the interval to be compared with a conventional confidence interval after a choice of , as the paper does in Theorem 2. The closed form also avoids treating the two constrained optimization problems as unrelated numerical searches.
The paper proves the result in its online appendix, which is absent from the PDF held for this mission. The Lean statements here are draft targets with sorry; no machine-checked proof of them is claimed. A complete formalization would add a reusable finite least-squares design, an exact characterization of linear objectives on its quadratic sublevel sets, and the treatment-column specialization. Theorem 2's calibration, Theorem 3's distributional analysis, and the support-vector-machine result are outside this mission's target.
The optimizer must be shown to exist, to be the stated vector, and to be the only solution, including when and the feasible set contracts to one point. A bound on the optimal objective value alone does not identify the remaining coefficients. Specializing the general regression formula to the treatment column also requires the coefficient block of the full least-squares solution to agree with the confounder-only expressions in (16) and (17). Keeping track of that block and the treatment coordinate is the main algebraic complication. The paper's printed definition of SSE in Theorem 1 uses the regression on alone; that value cannot measure the slack in the full-design constraint and gives incorrect endpoints.
Vectors are finite functions into , designs are Mathlib matrices, and the norm in Theorem 4 is the square root of a finite sum of squares. The treatment indicator is Boolean and is converted to or ; no intercept is inserted unless it is a column of . The treatment coordinate is the distinguished last column of . The goal describes each entire set of feasible maximizers or minimizers as a singleton, including its confounder coefficients.
The statements explicitly require invertibility of the relevant Gram matrix and . Theorem 4 also requires a nonzero prediction vector. These conditions make the inverse, square root, and quotient formulas meaningful and keep the characterization nonvacuous. The corrected full-design SSE in Theorem 1 is a deliberate change to the printed formula: with , treatment indicator , and , the true maximum of in (14) is , which the full-design SSE () reproduces, while the printed regression-on- SSE () gives . The regression on is an instance of the same generic least-squares design used for Theorem 4, so and SSE are that design's least-squares coefficients and residual sum of squares. Theorem 4 prints both signs without saying which solves which problem; the formalization assigns to the maximization, which is the correct pairing since .
A statement asserting only that is the optimal value of (14), for instance as the greatest element of the set of feasible treatment coefficients, would not be this mission's goal: the goal states that the solution set of each problem is exactly the given coefficient pair, so it carries the confounder vectors , existence and uniqueness. Contributions to the finite least-squares infrastructure and to either optimizer characterization support the mission.
An experience good is a product whose value a consumer learns only by consuming it: a new streaming service, a meal-kit brand, a novel drug. When two firms launch competing experience goods in a new product category, every first-period sale does two things. It earns a first-period margin, and it creates a repeat consumer whom the firm can price to in the second period, while the rival's first-period buyers become potential switching consumers. When firms can price by purchase history (behaviour-based pricing), the second-period prices to repeat and switching consumers differ, and the value of a first-period sale is set by how profitable each group is.
Z. Chen, C. Stanton and C. Thomas (Management Science 70(6), 2024) study this competition when trying one good is informative about the other (an information spillover, of strength ). Their Theorem 1 isolates what drives profits in every symmetric equilibrium, whatever the second-period equilibrium looks like: competition for first-period share pushes the first-period price exactly to the level at which a firm's total profit equals what it would have earned from switching consumers alone. The result connects to the literature on experience goods and introductory pricing (Bergemann and Välimäki, 2006) and on behaviour-based price discrimination (Fudenberg and Villas-Boas, 2006), where the role of switchers is usually derived in models without spillovers.
Two firms and have a common marginal cost . Firms and consumers discount the second period by . A unit mass of ex-ante identical consumers buys at most one unit per period.
The second period has already been solved. A firm earns in the second period per unit of its own first-period buyers (repeat consumers) and per unit of the rival's first-period buyers (switching consumers). Both are independent of first-period market shares, because consumers choose in the first period before learning their values.
In the first period the firms set prices simultaneously. Buying either good at price gives a consumer present surplus , where is the common gross value of a first-period purchase including its option value for the second period; not buying gives . Firm 's first-period share is if and , a given tie share ( for , for , with ) if the two surpluses are equal and at least , and otherwise. Firm 's two-period profit is
A price is a symmetric equilibrium when no firm can raise its profit by any unilateral deviation from to another real price.
For every symmetric price at which consumers buy (),
and in that equilibrium each firm earns , for every tie share .
Theorem 1 says that in any symmetric equilibrium a firm's total profit is the discounted profit from switching consumers. The first-period price fully dissipates the extra value of a repeat consumer over a switcher. Consequences drawn in the paper include: profits are positive only if the second-period equilibrium has switchers (); the result holds for every spillover strength, including ; and with firms and two periods (Appendix D) profits fall to zero. The theorem is the backbone of the paper's later comparative statics in .
The result is proved in the paper; nothing here is open. The mission produces the first machine-checked version of the argument, stated for both firms, for any real second-period profits, and for both directions: a covered symmetric price is an equilibrium exactly when it equals . To our knowledge no part of it has been formalized before.
The mathematics is elementary, and the difficulty is in the discontinuities. Demand jumps between , the tie share and as a price crosses the rival's, so profit is not continuous in a firm's own price. Undercutting by yields a profit that approaches but never reaches , so the "only if" direction cannot pick a single best deviation. It has to use deviations by arbitrarily small . The corner tie shares give one firm zero share at the symmetric profile, so the identity has to be pinned down by combining both firms' incentives, not one firm's. The printed proof also carries a slip (below) that a transcription would turn into a false statement.
Everything lives in the namespace SpilloverDuopoly.Switchers. The single definition file Model holds a structure Params (fields c, delta, lam, piR, piS, V, u0, all real), the predicate Standing (, , ), the surplus CS, the shares shareA, shareB, the profits profitA, profitB, the predicate IsSymEq and the price pStar. IsSymEq uses the platform's published two-player pure Nash predicate CrossLicensing.ExPost.IsNE with both strategy sets equal to .
Committed conventions:
The equilibrium predicate quantifies over every real deviation for each firm. It is not defined through or through the two deviations the proof checks, and the shares come from surplus comparisons, not from a "cheaper wins" rule. So the goal cannot be closed by unfolding definitions. Contributions welcome: proofs of the milestones and the goal, and a formalization of the paper's second-period equilibria (Proposition 1, Corollary 1) that would instantiate .
A drug regulator approves a candidate drug when its clinical trial rejects the null hypothesis of no effect at a fixed significance level . FDA guidelines recommend the same threshold, , for every disease (Bravo, Corcoran and Long, p. 2). A uniform threshold balances the wrong errors for some diseases. For a severe disease with no available treatment, wrongly rejecting an effective drug (a type II error) can cost far more than wrongly approving an ineffective one (a type I error). For a crowded therapeutic area the balance is the other way. Regulators have responded with expedited programmes (Fast Track, Breakthrough Therapy, Accelerated Approval), and decision-analytic work has asked how trial design should account for the harm of each error (Montazerhodjat, Chaudhuri, Sargent and Lo, 2017).
Bravo, Corcoran and Long (2021) add the drug development pipeline and the market to this question. Candidate drugs arrive in clinical trials, some are abandoned, the rest are reviewed, and approved drugs stay on the market for a while. The optimal then depends on operational quantities such as trial duration and attrition, and not only on the costs of the two errors. The paper's main analytical result is a set of comparative statics. The optimal level is higher for diseases with long trials, high attrition and few compounds in development. This mission formalizes that result together with the analytical steps of its proof.
A two-armed trial with patients per arm measures an outcome of standard deviation . The information of the sample is . Under the alternative hypothesis, which says the drug has effect , the Wald statistic is approximately normal with mean and variance one. A drug is effective with prior probability . With the standard normal distribution function, the probabilities that a drug is approved and effective (AE), approved and ineffective (AI), or rejected and effective (RE) are
Drugs enter trials at rate . Each trial is a race between completion at rate and abandonment at rate , so drugs reach review at rate , and the outcome streams have rates . Approved effective drugs fall into one of therapeutic classes and stay on the market at exit rate . Approved ineffective drugs leave at rate . With and , the paper's expected numbers of effective and ineffective drugs on the market are and .
Each effective drug on the market yields health benefit and each ineffective one costs , valued at per unit. Approving an effective drug yields , approving an ineffective drug costs , and rejecting an effective drug costs . The expected net benefit is
and an optimal approval policy is a maximizer of over .
The optimal approval policy is
Each clause compares two parameter vectors that differ in one parameter only.
Proposition 1 turns the model into policy statements. The approval bar should be lower for diseases with long trials (small ), high attrition (large ) or few compounds in development (small ), and for drugs whose rejection is costly. It should be higher where ineffective drugs linger on the market (small ). Part (c) shows that the natural intuition fails in general: more promising candidates (larger ) and longer effective market lives (smaller ) call for more lenient approval only when the market for effective drugs is not crowded, . Figure 3 of the paper shows decreasing in over most of the range when the condition fails. The paper's numerical study estimates for many diseases, and these monotonicity properties are what make those estimates readable.
The result is proved in the paper; nothing here is open. No machine-checked version of Theorem 1 or Proposition 1 exists. A formalization needs to supply what the paper calls "direct computation" and "straightforward differentiation": the concavity of the Gaussian power curve, the interior first-order condition, and the implicit-function argument. The printed derivatives (A.19) and (A.20) drop positive factors, and the formal statements give the corrected derivatives.
The obvious argument is to differentiate the first-order condition. That needs to be interior, unique and differentiable in each parameter, and the paper asserts all three without proof. Interiority depends on the behaviour of the power curve's slope at the endpoints: it tends to as and to as . That in turn needs facts about the normal quantile that Mathlib does not package.
For , and , has no sign at a general . Its sign is known only at the optimum, through the first-order condition. A pointwise sign argument therefore does not work, and one has to argue along the optimal path. In part (c) the side condition is a condition at the optimum, so it must hold at every parameter value between the two being compared. Checking it at the two endpoints only does not give the monotonicity.
All declarations live in the namespace FlexApproval.Statics. and on are the published Cohen2019.Robust.Phi and PhiInvReal. A parameter vector is a structure of real fields plus . The model fixes the following conventions:
deriv. Derivatives in a parameter are stated with HasDerivAt and an explicit value, never as a bare deriv sign, which would hold trivially wherever the derivative fails to exist. The derivative in is taken through , since .The optimal policy is never defined by the first-order condition (5). Doing so would make Theorem 1 a tautology and the comparative statics a statement about a formula. Every statement quantifies over maximizers of .
Useful infrastructure beyond this mission: smoothness and the endpoint limits of the normal quantile, concavity of Gaussian power curves (ROC curves of the equal-variance normal model), and a monotone comparative-statics lemma for strictly concave objectives. Proofs of individual milestones are welcome, and so are alternative routes to Proposition 1 that avoid the implicit function theorem.
Not formalized: Proposition 2 (ordering of in ), Proposition 3 (monotonicity and diminishing increments of the optimal value in ), the queueing derivation of (4), and the numerical study of §5.
Negative advertising (comparative advertising that points to a rival's flaw) is used both in product markets and in political campaigns, and its regulation differs across jurisdictions: until the 1990s it was not permitted in numerous countries of the European Union (Anderson and Renault, 2009). Many models of advertising take the products' positions as given. Bostanci, Yildirim and Jerath (Management Science, 2023) ask what happens when a firm chooses its product position knowing which advertising war that position will invite. Their main finding, Proposition 2, is that permitting negative advertising can make an entrant give up differentiation: it places its product next to the incumbent's, and both firms then advertise positively.
The mechanism is a spillover effect: products positioned close together tend to share attributes, so revealing that the rival's product has a flaw also raises the probability that one's own product has it. Co-location therefore disarms negative advertising.
There are two locations, and , each with a unit mass of consumers whose ideal product sits there. The incumbent (firm 1) is at ; the entrant (firm 2) chooses . A consumer at buying product at gets utility , where the distance is at the own location and at the other, and the reservation value is uniform on . Not buying gives .
Each product has a positive attribute , equal to with probability and otherwise, and a negative attribute , equal to with probability and otherwise; . The normalization makes . Under co-location ; apart, the attributes are independent.
The timeline: the entrant positions; nature draws the type profile , seen by the firms only; each firm simultaneously chooses (advertise its own positive attribute, advertise the rival's negative attribute, or nothing), truthfully; consumers update their beliefs by Bayes' rule and buy. The price is normalized to 1, so a firm's payoff is its demand. A perfect Bayesian equilibrium (PBE) consists of the entrant's location, advertising strategies at both locations, and consumer beliefs, such that consumers choose optimally, the ads form a Nash equilibrium of every advertising sub-game, the location maximizes the entrant's expected demand, and beliefs follow Bayes' rule.
A firm is a weak opponent of if it cannot advertise ( and ), and a strong opponent otherwise.
Under the standing assumptions, Assumption 1′ (, ), and
there is a PBE in which the entrant co-locates, every firm holding the positive attribute advertises it after co-location, and after locating apart a firm that can attack a strong opponent does so.
The result links two decisions usually studied separately. Positioning models predict differentiation to soften competition; Proposition 2 shows that when the advertising stage follows positioning, the entrant may prefer to co-locate, and that banning negative advertising (Proposition 1 of the paper) changes the positioning outcome. This bears on the regulation of comparative advertising and on the welfare comparisons of §4 of the paper.
The formalization produces a checked version of a result whose printed parameter region is wrong. The printed conditions are not sufficient: at , , , , , , every printed condition of the proof holds, yet the entrant earns by co-locating and by locating apart, so the described profile is not an equilibrium. The mission states the corrected theorem, and a machine-checked proof would settle that the corrected region is right. The result has not been formalized before.
The obvious argument fills in Table 1 and compares demands case by case, which is what the paper does; its slips sit in exactly that bookkeeping. Two places need care. First, demand is piecewise linear in the posteriors: whether a firm steals the rival's location depends on the sign of , and ties are broken differently under co-location (equal split) and apart (closer product), so each lemma is a case analysis whose boundaries matter (Lemma 4's printed strict condition fails at its boundary). Second, the entrant's location payoff is an expectation over 16 type profiles under a correlated prior; the paper's two closed forms both carry errors, so the comparison has to be recomputed rather than copied. The goal then requires checking every advertising sub-game at both locations, including those off the equilibrium path.
Everything is finite and real-valued; no measure theory is needed. Firms, locations and ads are small inductive types; a type profile is a pair of Boolean functions; the prior is the product of two correlated Bernoulli pairs. Consumer behaviour is built into the demand function: consumers choose the product with the larger posterior expected attribute minus distance, buy iff the reservation value is at least minus that maximum, and break ties as in footnote 11 of the paper. The uniform cdf is clipped to . Beliefs are probability mass functions on type profiles; the PBE definition requires Bayes' rule wherever the observed outcome has positive prior probability, and only consistency with the truthful ads elsewhere.
Corrections relative to the page, all disclosed in the item statements: in Assumption 1 (printed ); the added condition (the proof claims this region is excluded, but it is not, and there the profile fails); ; (A5′), (A6′), (A1d′) in place of (A5), (A6), (A1d); and Lemma 4 with a weak inequality.
The goal is an existence statement over all profiles satisfying every PBE condition; beliefs are computed by Bayes' rule, not defined as Table 1's numbers, and demand comes from consumer choice, not from the paper's demand tables, so neither the table nor the closed forms hold by definition.
All definitions live in one file, NegAdPosition.CoLocate.Model. Proofs of the milestones in any order are welcome; Table 1 and the closed forms are mechanical but long, and reusable tactics for sums over the 16 type profiles would help every item.
Call centers and other many-server service systems serve several classes of customers, each with its own service-time distribution, patience distribution and cost of waiting or abandoning. A customer who waits longer than its patience time abandons. The system manager decides, whenever an agent becomes free, which class to serve and which customer inside that class to serve.
Classical scheduling rules for such systems, such as the rule of Atar, Giat and Shimkin (2010) and the generalized rule of Long, Shimkin, Zhang and Zhang (2020), serve customers of the same class first-come, first-served (FCFS). Bassamboo and Randhawa (2015, published in Management Science 2016) showed that FCFS within a class is suboptimal when patience times are not exponential: as a customer waits, the conditional distribution of its residual patience changes, and serving by time in queue can reduce cost. Their fluid analysis showed that a single class should be split into at most two FCFS subclasses.
Bassamboo, Randhawa and Wu (Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2023.1190) combine the two decisions, across classes and within a class, in one fluid optimization problem. Their structural result is that the fluid-optimal schedule needs within-class differentiation for at most one class; every other class is served FCFS. This is the basis of their "mostly-FCFS" policy. This mission formalizes that result together with the two lemmas stated before it.
There are classes and a total capacity of agents. Class arrives at rate , has mean service time with , and its patience time has distribution with survival function . The offered wait of a customer is the time it would wait before service if it were infinitely patient; means the customer is never served. A customer offered wait incurs an average cost , obtained in the paper by integrating a cost over service time and patience (display (5)).
In the fluid model, class receives capacity and is divided into subclasses, each served FCFS. Subclass has arrival rate , offered wait and capacity . The within-class program (6) defines the class cost function
the infimum ranging over and all subclass rates, waits and capacities. The middle constraint says that the rate of customers of subclass who remain patient long enough to reach service does not exceed the subclass's service rate. The across-class program (2) is
A plan is a choice of capacities and, for each class, a subclass configuration feasible for (6) at ; a fluid-optimal solution is a feasible plan of least total cost .
The fluid-optimal solution to (2) with defined in (6) splits the classes into at most subclasses; in particular for at most one class , and for this class . Formally: every feasible plan is weakly improved by a feasible plan with
Proposition 1 is what makes the paper's policy simple. Lemma 1 alone would permit every class to be split in two, giving up to FCFS queues with their own priority rules; Proposition 1 says that one non-FCFS class suffices, so a fluid-optimal schedule can be implemented as a priority ordering of classes with time-in-queue differentiation in at most one of them. Combined with Lemma 2, which makes (2) a convex allocation problem, it underlies the index-based characterization of the optimum in Proposition 2 and the mostly-FCFS and multi-class time-in-queue policies of §4.
The paper's proofs are in an online appendix that this mission does not use. To our knowledge none of the three results has a machine-checked proof. The formal development provides a reusable encoding of the fluid model of a multi-class queue with abandonment, with offered waits that may be infinite, and a checked version of the sparsity statement underlying the mostly-FCFS policy.
The program (6) has an unbounded number of subclasses, offered waits drawn from , and arbitrary cost and survival functions, so the feasible set is not a fixed finite-dimensional polytope and the infimum need not be attained. Lemma 1 for each class separately does not give Proposition 1: splitting each class into two subclasses is consistent with Lemma 1 and violates Proposition 1. The bound in Proposition 1 depends on capacity being free to move between classes, with only the total budget shared; with each held fixed the claim fails. The statements must also respect the never-served subclass , which the paper uses to represent LCFS as the offered-wait vector .
Everything lives in the namespace HetImpatient.FluidSplit, in one definitions file HetImpatient.FluidSplit.Model and three theorem items.
Fin m; a class configuration carries its own number of subclasses J : ℕ, with subclasses Fin J, and feasibility requires J ≥ 1. The number of subclasses is otherwise unbounded.ℝ≥0∞, so is allowed. Rates, capacities and costs are real numbers.A statement that drops the comparison of costs, or builds "at most two subclasses" into the definition of feasibility, is trivial and is not what is formalized here: the improved plan must be feasible and no more costly, and feasibility permits any number of subclasses (a sanity check confirms that a plan splitting two classes is feasible).
Welcome contributions: proofs of Lemma 1, Lemma 2 and Proposition 1, and supporting lemmas about subclass configurations stated for this model.
A firm that owns a strong brand can use the brand name on a new product outside its core business. This brand extension can be produced in-house or licensed to a specialized firm against a royalty. Brand licensing is a large business: its revenues reached US$315.5 billion in 2022 (Licensing International, cited in the paper's endnote 2). The marketing literature has long documented a risk: a poor extension can damage the brand and lower demand for the core product. This risk is called brand dilution. The empirical literature surveyed in the paper's introduction (Colucci, Montaguti and Lago 2008; Jayachandran et al. 2013; Bărbulescu Robinson et al. 2015) finds that dilution is associated more with licensing than with internal development. The prevalent reading is causal: a licensee, who does not own the brand, has scope for opportunistic behaviour that damages it.
Bacchiega, Colucci, Denicolò and Magnani (Management Science 70(5), 2024) build a game-theoretic model of the brand owner's choice between no extension, in-house development and royalty licensing, with moral hazard on the licensee's side and a reciprocal effect of the extension's quality on the core product's demand. Their central result, Proposition 3, runs against the causal reading. Among parameter values where the brand owner is indifferent between the two modes, switching from in-house development to licensing always raises the quality of the extension. The empirical correlation must therefore come from selection, not from licensing itself.
There are two products, a core product and an extension, both sold monopolistically. Efforts and are the products' perceived qualities. The parameters are the perceived distance between the products, the technological distance , the core market size , the extension market size , the magnitude of the reciprocal effect and a benchmark quality ; the cost parameter is normalized to .
The intensive margin is the set of parameters where .
For every in-house equilibrium and every subgame-perfect licensing equilibrium with extension effort , if
then
with strict inequality when charges every nonempty open interval.
The goal is stated about the equilibria themselves, not about the closed forms the paper derives for them.
Proposition 3 separates two explanations of the same correlation. If licensing caused dilution, a brand owner who switched from in-house development to licensing would lower the extension's quality. In the model the opposite happens at the margin of indifference. The core product's quality falls under licensing, because the brand owner internalizes only part of the extension's effect on it. To stay as profitable as in-house development despite the costs of a vertical chain, the licensed extension must be of higher quality. Dilution under licensing then appears where licensing is chosen for other reasons, for example at the extensive margin (Proposition 2 of the paper), not because of the mode itself.
The result has been proved on paper, through explicit closed forms in Appendices A, B and F. As far as is known it has no machine-checked proof. The mission adds three things. It checks the closed forms of the equilibrium, including the global optimality and uniqueness of the first-order solutions. It handles the corners the paper treats in words: the royalty constraint , and the licensee's zero effort when exceeds the quality index. And it checks the sign computations, where the printed (F.4)–(F.6) contain slips. The comparison it builds, between a centralized optimum and a subgame-perfect equilibrium of a three-stage moral-hazard game, appears throughout the licensing and franchising literature.
The obvious comparison fails. In general and cannot be ranked: the licensee has a lower cost of effort, but it ignores the reciprocal effect and faces a royalty that erodes its margin. The ranking holds only on the intensive margin, which is defined implicitly by the equality of two equilibrium profits. Using that equality requires the full closed-form equilibrium of both modes, including that the first-order solutions are the global, unique optima on the non-negative orthant and in every subgame of the licensing game. One then eliminates through and signs a rational function of on the whole parameter box. The degenerate corners and , where the royalty is indeterminate and both modes earn the no-extension profit, are excluded only by the strict inequality , so they have to be handled explicitly.
All quantities are real numbers; a model is a structure Params with fields α θ μ ρ lam ε (lam is ), and Params.Standing bundles , , , , , . Every effort and royalty ranges over . The extension profit and output carry a positive part, so that nothing is sold when the royalty exceeds the quality index. The core profit is , as on the page. The in-house equilibrium is any maximizer of (7) on the non-negative quadrant. A licensing equilibrium is a strategy profile — the licensee's effort rule , the royalty rule and the core effort — optimal in every subgame. The licensee's participation decision is not modelled, because it never binds under a pure royalty. The no-extension benchmark enters as " exceeds for every ". The dilution clause is stated for an arbitrary probability measure on for the shock (weak inequality), and strictly for every such measure of full support.
The goal must not be restated with the closed forms (A.2), (B.2) in place of the equilibria, nor with in place of the profit equality, since either turns it into an algebraic identity about the paper's formulas. The milestones (F.4) and (F.6) state corrected forms of the printed expressions: the right-hand side of (F.5) is , and the numerators of (F.4) and (F.6) read .
A complete development needs elementary real algebra and two-variable concave quadratic optimization on orthants and half-lines; Mathlib suffices. The subgame-perfect equilibrium of a sequential game with continuous actions is reusable beyond this mission. Proofs of individual milestones, in any order, are welcome.
Continuous limit-order markets reward speed. When the fundamental value of an asset moves, a trader with a faster connection can trade against stale quotes before the quoting liquidity provider can cancel them. This practice, sniping, is a direct transfer from liquidity providers to fast traders, and it has been documented and analysed as a cost of the continuous-trading design (Budish, Cramton and Shim, 2015). One market-design response, used by the Investors Exchange (IEX), whose exchange application the SEC approved in June 2016, is a short, fixed delay on all incoming messages combined with midpoint peg orders: hidden orders that rest at the midpoint of the national best bid and offer and that the exchange re-prices before a delayed sniping order can reach them. The delay therefore protects pegged orders from sniping, while ordinary quotes at the best bid and offer remain exposed.
Aldrich and Friedman (2019, SSRN 2999059), published in Management Science in 2023 (doi:10.1287/mnsc.2022.4370), build a model of such a market in which impatient investors choose between protected midpoint pegs and immediate market orders, and proprietary traders choose between providing quotes and sniping them. Their baseline result is a closed-form, unique equilibrium describing how much order flow the protected midpoint attracts and how many market makers and snipers the market supports. This mission formalizes that baseline result.
A parameter vector consists of the flow cost of speed , the midpoint execution fee , the investor gross surplus , the discount rate of a resting pegged order, the arrival rate of investors on each side of the market, and the rate at which the fundamental value jumps up (and, separately, down) by one tick. The standing restrictions are , , , , , . The discount factor is .
The order imbalance records the hidden midpoint queue: means resting sell pegs, means resting buy pegs. A fraction of investors send pegs, the rest market orders, and each arrival is a buy or a sell with equal probability. A peg always joins the queue or executes against a contra-side peg; a market order executes against a contra-side peg if one rests and otherwise at the best bid or offer. One arrival maps a distribution to , with
The discrete Laplace law is .
Under , the expected net surplus of a midpoint peg order and of a market order are
With real masses of market makers and of snipers, their flow profits are
A market equilibrium (Definition 3.1) is a triple such that either and , or and ; and with .
Under the standing restrictions there is exactly one market equilibrium, namely
The goal asserts both that this triple satisfies Definition 3.1 and that every triple satisfying Definition 3.1 equals it.
The proposition gives the baseline against which the paper measures the effect of order protection. Its closed forms show that the peg share is independent of the sniping intensity , that it falls with gross surplus and rises with patience , and that the sniper mass does not depend on because the market-maker mass adjusts. The paper's later sections compare this benchmark with a market in which pegs are not protected, and its welfare and empirical comparisons with IEX data are calibrated on these formulas (Table 2 reports at the baseline parameters).
The result is proved in the paper; nothing here is open. A search of the Prove2Me catalog finds no part of it formalized: there is no machine-checked discrete Laplace stationary law, no limit-order-book equilibrium and no pegged-order model on the platform. The mission adds a checked version of the full argument, including the uniqueness half of Proposition 3.1, which the paper asserts but does not prove (its proof verifies only that is a fixed point).
The algebra of (3.2), (3.3) and (3.9) is short once the sums are evaluated, so the content lies elsewhere. First, the payoffs are defined as infinite series over a two-sided index, and their closed forms require summing geometric series on both tails, including the discounted tail . Second, uniqueness of the steady state in Proposition 3.1 is a statement about every nonnegative summable fixed point of on , not just a verification that is one. Third, uniqueness of the market equilibrium requires excluding every other triple: the interior branch and the corner must be shown to be mutually exclusive and exhaustive, and the case of a zero mass of market makers or snipers must be ruled out. The naive reading that "solving gives the equilibrium" misses the corner case and the requirement that the root lie strictly below one.
All quantities are real numbers, and the parameters are bundled in a structure Params with a predicate Params.Standing. The paper prints the restriction ; the formalization uses , as in Assumption A4a, which is among the proposition's hypotheses, because at the formula gives , which Definition 3.1 does not admit, and no equilibrium exists. The fee restriction is the proposition's , weaker than A4b's . The condition is derived from , not assumed.
One-sided sums are Lean tsums over , with indexed by ; a distribution on is a nonnegative family with HasSum p 1. is a natural-number power, so at is the point mass at , which is what the corner of Definition 3.1 evaluates. The payoffs , and the market-maker profit are defined by their series, not by their closed forms, so that (3.2), (3.3) and (3.5) are milestones rather than definitions. Division by zero returns zero in Lean; a zero mass then yields or , never zero profit, which matches the page.
A formalization that only checks that the formula triple satisfies the equilibrium conditions, or that defines by their closed forms, would drop the uniqueness claim or the steady-state analysis, and is not the target.
The development needs two-sided geometric series, tsum manipulation over and , and elementary bounds on Real.exp. The stationary-law uniqueness for a birth–death operator on is reusable beyond this mission. Proofs of individual milestones, in any order, are welcome.
Unused prescription medicines create disposal and public health costs, while a patient may use less medicine than a doctor prescribes. A regulator can make the pharmaceutical producer collect unused medicine, or charge a fee on dispensed medicine and use the proceeds to fund collection. These two policies charge the producer for different quantities. Alev, Atasu, Toktay and Zhang study how that distinction affects a producer's incentives to influence prescriptions and the regulator's choice of policy. The question matters when regulation changes both the amount prescribed and the share of unused medicine collected.
A patient has a need level and a preferred use level . They are independent and uniform on . The producer chooses a medicine price and two promotional effort levels, directed at the doctor and directed at the patient. Both efforts lie in . The doctor chooses a prescription to maximize
Here is the unit health benefit and is the doctor's reputational cost per unit of over-prescription. At indifference the model selects . The amount used is ; the remaining is unused. These choices and the tie convention reproduce the doctor's rule in Lemma 1, p. 15.
Under end-of-pipe control (EC), the planner sets a collection rate . The producer pays unit cost to collect that fraction of unused medicine. Under source reduction (SR), the planner charges the producer a fee for each dispensed unit and collects unused medicine at rate . The SR planner must fund collection without a deficit. For either policy, the producer maximizes expected revenue minus the quadratic promotion costs and its policy cost. The doctor must receive nonnegative utility for every need level.
The planner evaluates expected doctor utility, producer profit, and planner surplus, then subtracts two harms. Environmental disutility is ; social disutility from uncollected unused medicine is . The resulting expected total welfare is maximized subject to the collection, fee, producer participation, and no-deficit constraints. The planner may choose among producer actions tied for maximal profit. The full primitives and constraints are those of Section 3, pp. 8–14.
The producer thresholds in the appendix's stated regime are
Write and for the attained maximum welfare values under the two policies. Proposition 4 and Table 2, pp. 17–18, give the mission's goal: the models tie for ; they tie when and ; SR weakly wins when and . When and , a threshold divides SR's weak advantage below it from EC's weak advantage above it. Above that threshold, an EC welfare optimum eliminates over-prescription, encoding the paper's requirement .
The milestones cover the doctor's prescription rule, the producer's optimal profit in each prescription region, the health-benefit and collection-cost thresholds, the EC environmental threshold, and the appendix's SR replication claim. Together these are the named results and displayed steps used by the paper's welfare comparison.
The result identifies when a fee on every dispensed unit can match or improve a direct collection obligation, and when the direct obligation can weakly improve welfare because it acts on unused medicine. Its threshold form connects a medicine's health benefit and the cost and harm of its disposal to the preferred regulatory instrument. The comparison also separates the ability to discourage over-prescription from the value of doing so: a policy may allow its elimination without making it welfare maximizing.
The paper proves these claims analytically in its stated appendix regime; this mission asks for machine-checked proofs of the game model, equilibrium welfare comparisons, and threshold results. The proposed Lean theorems are currently open. The model definitions are reusable for the paper's producer-preference and advocacy results, which are outside this mission.
Comparing the two policies at a fixed prescription quantity misses the producer's response. Changing a collection rate or unit fee changes the producer's optimal price and promotion, which can switch the doctor's choice between prescribing need and over-prescribing. The planner must also respect producer participation, and SR must cover its collection costs. The welfare comparison therefore requires the feasible equilibria in both prescription regions and careful treatment of ties at the switching boundary. The online appendix, pp. 1–5, records the relevant region calculations.
Lean represents all parameters, actions, and policies by real numbers. It computes expectations by iterated interval integrals over independent uniform . The prescription response, producer profit, planner surplus, disutilities, and welfare are defined from the Section 3 formulas. Welfare is the supremum over feasible planner policies and producer optima, with attainment asserted in the goal. The model never defines welfare by an appendix closed form, and the three named thresholds are fixed to the appendix formulas rather than left as free witnesses. The environmental threshold must also lead to an EC optimum without over-prescription, so an empty or arbitrary switch does not satisfy the intended claim.
The goal states the appendix's , , and regime, together with , , and nonnegative disutilities. The restriction is the appendix's nonnegative-profit convention. In this regime , so the first column of Table 2 has no instance with ; it remains stated because it belongs to the printed table. Proposition 1's strict ordering of health-benefit thresholds requires , a disclosed strengthening of that milestone's premise. The doctor's tie goes to over-prescription; the planner can select among producer optima; price has no sign restriction. EC uses only its collection rate, so the unused fee field of the shared policy record has no effect. The participation condition is pointwise in need. The SR half of Proposition 3, later propositions, numerical study, and regimes outside the printed proof are outside this mission.
Many tasks on high-dimensional data ask not for the nearest neighbours of a query but for how many data points lie close to it. Density estimates of this kind feed outlier detection, kernel density estimation, classification by neighbourhood counts, and the tuning of nearest-neighbour search itself. Exact counting needs a scan of the whole dataset for every query, and uniform random sampling needs about samples per unit of relative accuracy, which is prohibitive when the neighbourhood is a tiny fraction of the points.
Locality-sensitive hashing (LSH) is the standard tool for finding near neighbours in sublinear time: a random hash function sends nearby points to the same bucket with higher probability than distant ones (Indyk–Motwani 1998; for angles, the random-hyperplane family of Charikar 2002). Wu, Charikar and Natchu (arXiv:1809.07471; Mathematics of Operations Research, 2022) turn LSH tables into a counting device. Their estimator LSH Count samples from the buckets near the query and corrects the bias of hashing by importance weighting, so that the number of samples depends on how well the hash concentrates the neighbourhood rather than on .
The dataset consists of unit vectors , and the query is a unit vector. For a set of angles, the neighbourhood is
and the target is its size .
A table is built from a random hash function , which stores in the bucket . For a set of Hamming distances, is the set of points of table whose bucket is at a Hamming distance in from the query's bucket , and is their number. The collision probabilities are
for one random table, , and is the expected pool size of one table.
LSH Count with parameters :
The table bias is the mean of given the tables.
For and , if
then
This uses tables and samples in total, the of the printed Theorem 1 (p. 6).
Theorem 1 bounds the cost of counting near neighbours with LSH: the sample complexity replaces the ratio of uniform sampling by the ratio of the expected pool size to the expected number of neighbours in the pool. When the hash concentrates the neighbourhood, this is a large saving, and the number of tables depends only on and . The same template (importance weights from known inclusion probabilities, a variance split into a sampling term and a design term, median of means) recurs in randomized estimation; Lemma 4's decomposition is the step that makes the two sources of error separately controllable.
The result is proved on paper. No machine-checked proof of it, or of any LSH-based estimator, is known. The mission produces a formal proof with explicit constants. Theorem 1 is printed with ; the constants here are the ones its proof determines, and one of them corrects the printed proof: the final display of Lemma 6 (p. 17) drops a factor that its own target inequality needs. The mission also produces reusable, generic pieces: the deterministic median lemma and a Chernoff bound for independent events with probability at most .
The arithmetic of each lemma is short; the difficulty is the probability model. The samples are not independent of the tables: their law is uniform on a random pool whose size is itself random, and the weight divides by that size. Unconditional moments therefore require conditioning on the tables and then averaging over them, and the cross terms in Lemmas 2 and 5 separate a single table from pairs of distinct tables . A tempting simplification samples uniformly from the set of distinct points in the probed buckets; it makes Lemma 1 false whenever a point is probed in several tables, because the weight then no longer averages to . A second tempting step treats as unconditionally independent, which would give an error of order and lose the table term , which does not decay in ; the samples are independent only given the tables. The Chernoff step needs independence across the estimators, which comes from building each estimator from fresh tables.
Fin n, so duplicates count separately; vectors live in EuclideanSpace ℝ (Fin d), and is InnerProductGeometry.angle.ProbabilityTheory.variance, Chebyshev's inequality (meas_ge_le_variance_div_sq), the moment generating function of a sum of independent indicators (measure_ge_le_exp_mul_mgf), and List.insertionSort. The median lemma and the Chernoff step are independent of LSH and reusable.Not in scope: Theorem 2 (Multi-Probe Count) with Lemmas 7–9; the running-time Theorems 3–4; the random-hyperplane collision formulas (Theorems 5–6, Lemma 12, (1)); the experiments.
After the financial crisis of 2007–2009, standardized over-the-counter derivatives were moved to mandatory central clearing: a central counterparty (CCP) becomes the buyer to every seller and the seller to every buyer, so that the original counterparties are insulated from each other's default. The CCP in turn protects itself by a default waterfall and collects two kinds of prepaid collateral from its clearing members: initial margin, which absorbs only the losses of the member who posted it, and the default fund, which is shared and mutualizes losses across members. Losses beyond both layers are borne by the surviving members through ex-post contributions. Regulators set both requirements, yet there was little theory of how the two collateral types should be combined.
Wang, Capponi and Zhang (Management Science, 2022) model this as a moral-hazard problem. Posting collateral raises a member's pledgeable income in the sense of Holmström and Tirole (1997) and so strengthens its incentive to manage risk; but because the default fund is mutualized, a member's incentive to hedge also depends on whether the other members hedge. The paper's headline result, Proposition 2, characterizes exactly when all members hedge as a function of the two collateral requirements. Its optimal-mix result (Proposition 3) and the policy discussion are built on it.
There are risk-neutral clearing members (dealers). A credit event occurs with probability ; in it, every dealer owes to its protection buyer. Each dealer holds an asset whose return is independent across dealers and of the credit event. It chooses an action : hedging () gives a bad-state probability and good-state return , risk-shifting () gives and , with , , and expected returns satisfying . A dealer starts with assets and receives the price from buyers of risk aversion , so its balance sheet is . The pledgeability is
and Assumption 2 requires .
Each member posts initial margin and default fund with , . Default-fund posting costs an extra per unit, and ex-post contributions are financed at unit cost with . If of the other members hedge, the number of defaults among them has law (the sum of independent binomials with parameters and ), and a surviving member's expected loss-sharing contribution and financing cost is
A member taking action earns
Members play a simultaneous game in pure strategies. A Pareto-dominant Nash equilibrium is a Nash equilibrium that gives every member at least its payoff in every Nash equilibrium.
The cutoff is the least default fund in at which hedging is a best response when all other members hedge, and is the least initial margin at which this holds with .
For every collateral pair with , , , there is exactly one Pareto-dominant Nash equilibrium, and
For every , is the unique solution in of
On the function is piecewise linear, strictly decreasing, continuous and convex, with slope at least , and with slope greater than whenever .
The proof in the paper's appendix gives the attack path. Lemma IA.1 gives the explicit ceiling-sum expression (A28) for and its properties (positive, strictly decreasing in , and , piecewise linear, continuous, zero at ) and the binomial moments . Inequality (A2) reduces "hedging is a best response" to . Step 1 shows that the cutoffs are unique, sorts the equilibria into three cases, and rules out asymmetric equilibria by (A4)–(A5). Step 2 computes the slope of off the kinks (A7), locates the kinks (A8), compares one-sided slopes at a kink (A9)–(A11), and Step 3 gives the closed forms (A15) and (A17).
Proposition 2 answers a regulatory question in closed form: given the initial margin, it names the smallest default fund that makes prudent risk management the outcome that members coordinate on. A slope of above means that a unit of default fund buys more incentive than a unit of initial margin, because the fund is mutualized. That trade-off is what makes the optimal collateral mix of Proposition 3 interior or a corner, and it drives the paper's comparative statics in the number of members and the financing cost.
The result is proved in the paper with an implicit-function argument; it has not been machine-checked. A formal proof would certify the equilibrium classification, including uniqueness of the Pareto-dominant equilibrium, which the paper argues case by case, and the shape claims. It would also make precise the regime in which the paper's "slope greater than " holds: when the prefunded default fund at already covers the shortfall of all other members (), the slope is exactly on an initial interval. The goal states the corrected claim. The binomial and piecewise-linear lemmas are reusable for other loss-mutualization models.
The equilibrium half is a finite game, but the natural argument "hedging is a strategic complement, so the extreme profiles are the only equilibria" needs strict monotonicity of in for every collateral pair, including the boundary where all vanish. It also needs weak inequalities handled carefully, since Nash equilibria here allow ties.
The shape half is harder. is defined implicitly by an equation whose left side is piecewise linear in with breakpoints that move with . A direct implicit-function argument gives derivatives only away from these kinks. Piecewise linearity, convexity and the slope bounds require locating every kink, showing that the ratio crosses each integer once, and comparing one-sided derivatives across a kink. The obvious claim that every slope lies in is false when the ratio exceeds .
All quantities are real numbers and members are indexed by Fin N. The paper's standing assumptions are bundled in Standing: conditions (1)–(3), Assumptions 1 and 2, , , , . To these the formalization adds , and , without which the model degenerates ( when ). Assumption 1 ( above the explicit bound (A18)) is a standing assumption of the paper that Proposition 2's proof does not use; it is kept. The expectation is the finite sum against the law of (A29), which encodes the paper's statement that depends on the other members' actions only through the number who hedge.
, and are defined as least incentive-compatible values (infima of nonempty sets bounded below), not as solutions of (18). Showing that they solve (18) and (A3), uniquely, is part of the targets, so the goal cannot be met by unfolding a definition. The Pareto-dominant equilibrium is not defined as "all members hedge": (17) is an equivalence over all profiles. "Piecewise linear" means finitely many breakpoints with affine between them, and "continuous and convex at the kinks" is stated as continuity and convexity on . The Nash equilibrium is the published generic pure-Nash relation CarbonDoubleCount.Planner.IsPureNash.
A complete development needs elementary binomial identities, one-dimensional implicit-function and monotone-root arguments, and one-sided derivatives of piecewise-affine functions; no measure theory is required. Proofs of individual milestones, in particular Lemma IA.1 and (A2), are welcome independently of the goal.
The U.S. Food and Drug Administration's accelerated approval pathway permits some drugs to reach patients before their clinical benefit has been fully confirmed. A manufacturer then promises a post-market study, but completion requires costly effort that the regulator cannot directly observe. If the study becomes overdue, withdrawal is a process rather than an instantaneous event. The time that process takes changes the manufacturer's incentive to finish the study. Xu, Zhao, and Petruzzi model this interaction and ask how withdrawal enforceability and the chance of a favorable study result affect compliance Xu, Zhao, and Petruzzi, SSRN preprint, 2019.
The question matters to a regulator setting a study deadline. A stronger withdrawal process can reduce the expected time a drug remains on the market after missing that deadline. A higher probability of confirming clinical benefit makes successful completion more valuable to the manufacturer. The paper's Proposition 2 compares these two changes through the largest study-cost type that a deadline can induce to comply.
A drug enters the market under accelerated approval at time zero. Its patent expires at time . Before expiry it earns a profit rate while accelerated approval remains in effect, and a rate after conversion to regular approval. The regulator chooses a deadline . If the study is still incomplete at , the regulator starts withdrawal; the additional withdrawal time is exponentially distributed with rate . Thus increasing shortens the expected withdrawal delay. Sales under accelerated approval stop at unless the study finishes earlier.
The manufacturer chooses a nonnegative effort , interpreted as the patient recruitment rate for a study requiring patients. For , the completion time follows a Gamma distribution with shape and rate . At the study never completes. A completed study confirms benefit with probability . If confirmation occurs before , the drug earns the regular-approval rate until ; otherwise it leaves the market at completion. For realized and , revenue is
The effort cost is , where is the manufacturer's cost type and . The resulting expected profit is for positive effort. With no effort, profit is . An effort is optimal if it maximizes this profit over all nonnegative efforts. The manufacturer complies at a deadline if some positive effort is optimal; a tie with zero effort counts as compliance, as in the paper's comparison . Let be the positive cost types for which some feasible deadline induces compliance, with the other parameters fixed. The compliance threshold is the supremum of that set.
The goal is the paper's Proposition 2. For fixed and admissible rates and probabilities, it asserts
The proof in the paper supports strict inequalities for a strict parameter increase when the initial compliant-type set is nonempty. This guarded strict version is included in the goal. If the set is empty, its Lean real supremum is zero, so an unconditional strict statement would be false.
The milestones record the integral representation of profit and the no-effort closed form, the single crossing of the deadline kernel, the threshold characterization from Proposition 1, and the two comparison steps used for enforceability and success probability. Together they connect the operational study model to the cost-type threshold. They are statements from Proposition 1 and the proofs of Propositions 1 and 2 in the same SSRN preprint.
The threshold tells the regulator which manufacturers can be induced to finish a required study by choosing an appropriate deadline. Raising it means that a manufacturer with a higher effort cost can still find positive effort optimal. The result concerns whether compliance can be induced; it does not assert a particular optimal deadline, a user-fee menu, or patient welfare. Those require further parts of the paper's mechanism-design model Xu, Zhao, and Petruzzi, §§4–5.
The mathematical result has a paper proof. This mission's Lean statements give it a precise computational interpretation: the completion and withdrawal distributions, the revenue rule, the no-study case, maximization over feasible effort, and the threshold are all explicit. The local index found no existing platform theorem with this model and conclusion. A complete development would add machine-checked proofs and reusable facts about Gamma completion probabilities, exponential delays, bounded expected revenue, and optimal effort. The present draft statements themselves are not proofs.
Comparing profit at the same deadline and effort does not settle the enforceability claim. Increasing changes both the return from completion and the benchmark profit from never completing, while the deadline that gives the best compliance incentive can move. Similarly, a positive payoff change at a fixed effort does not by itself identify the largest complying cost type: the optimum must still be taken over all efforts, and the supremum over deadlines must be justified. The proof must also control the zero-effort boundary and establish that the relevant set of cost types is bounded.
Lean uses real values for time, rates, profits, effort, and cost type, and a natural number for sample size. Params.Standing includes , , , , and . The paper gives and derives the profit-rate order from its demand assumptions. Positivity of , finite positive , and are disclosed restrictions needed for the stated threshold and the paper's limiting argument. Types satisfy , deadlines lie in , and the two boundary regimes and discussed as limits in the paper are outside the mission.
The withdrawal delay is Mathlib's exponential measure and positive-effort completion is its Gamma measure. Since Gamma measure at rate zero does not represent a study that never completes, the profit definition has a separate branch equal to . Revenue integrands are bounded on the distributions' nonnegative support under the standing assumptions. The threshold is computed as the real supremum of cost types for which an actual positive maximizer exists at some feasible deadline. A formulation based only on a positive-effort supremum would make compliance automatic and would not represent the paper's decision rule. If no positive cost type complies, the real supremum is zero; boundedness and the nonempty case are explicit in the milestones and goal.
A full proof needs integration against the Gamma and exponential measures, continuity and existence of an effort maximizer, a characterization of the cost-type set, and comparison of profit across deadline choices. Measure and optimization lemmas from this work can be reused beyond the drug-study application. Contributions to those components and to the stated milestones are within scope; the deadline-dependent fee menu and patient-welfare optimization of later sections are not part of this target.
Firms that track their customers can charge a returning customer according to what they have learned about her, while a newcomer pays an introductory price. Consumers can respond by identity management: deleting cookies, using new accounts or anonymising tools, so that they keep being treated as newcomers. The economics of this behaviour-based price discrimination with strategic consumers goes back to two-period models such as Fudenberg and Tirole (2000); the closest privacy models are the two-period monopolies of Acquisti and Varian (2005) and Conitzer, Taylor and Wagman (2012).
Laussel, Long and Resende (2023) study the question in an infinite-horizon setting; the formalization cites their CIRANO working paper 2021s-29. A monopolist gradually expands its market by lowering an introductory price, as a durable-good monopolist does in the Coase conjecture, and recognises every passive customer after her first purchase. Consumers decide once whether to pay a privacy cost to remain anonymous. The paper's main analytic result, Proposition 1, states that under full information acquisition the firm leaves part of the market unserved exactly when privacy is cheap enough, and gives the threshold in closed form.
Time is divided into contracting periods with discount factor . A monopolist sells a non-durable good at zero marginal cost. A unit mass of consumers has types uniform on ; type obtains utility per period of consumption.
Under full information acquisition (FIA) a passive consumer who has bought once is recognised and charged exactly in every later period. A consumer may instead pay a once-for-all privacy cost in period and become active: she remains anonymous and buys every period at the introductory price offered to new customers. Types in are active and types below the pivot are passive.
The firm uses a quasi-linear cut-off rule with : in period the new passive customers are the types in , starting from . The path converges to , and types below are never served. Consumers hold a quasi-linear expectations rule : the lifetime net utility of the period- marginal passive customer when the state is . The introductory price is , and the firm's period profit at state and choice is
A Markov perfect equilibrium (MPE) is a profile satisfying, at every state :
It must also satisfy .
With the threshold
every FIA MPE satisfies:
Proposition 1 shows that consumer privacy can stop a dynamic monopolist from serving the whole market. Without active consumers the firm keeps lowering its introductory price until everyone buys, in line with Coasian dynamics. With them, every price cut is also collected by the anonymous high-value consumers, so the firm stops at a strictly positive . The gap identity makes the effect quantitative: the share of passive customers who are eventually served is linear in the privacy cost. These statements underlie the paper's managerial recommendation that a firm facing cheap identity management should not aim at full coverage, and its comparison with the partial-history (PHI) information structure.
The result is proved in the paper, but by computer algebra with several printed slips. The prior-art search found no machine-checked formalization of this result. A formal proof would turn the closed-form calculation into a checked argument about a precisely defined equilibrium notion. The mission also provides a reusable encoding of an infinite-horizon pricing game with rational-expectations consumers, specified by arbitrage, Euler and indifference conditions. Nothing comparable is on the platform.
The equilibrium conditions couple the cut-off slope , the pivot and the expectation rule. The Euler equation leaves an algebraic condition on whose admissible root must be unique for every ; without uniqueness, two equilibria with the same discount factor could have different expansion speeds. At the pivot condition is an inequality, so a calculation valid at an interior pivot does not settle the threshold case. The pivot also contains an infinite price series whose convergence matters to the claimed threshold.
The Online Appendix's closed forms (29), (30) and (31) do not follow from the model as printed: the envelope expression (23) has a sign slip. For example, at the corrected Euler equation gives , whereas the printed (29) gives . The Lean statements use the derivative of the period profit and omit those printed formulas.
Everything is real-valued. The definitions file IdentityMgmt.FIA.Model has the following parts:
Profile structure with fields ;Arbitrage, Euler (via Mathlib's deriv), Pivot, IsMarkovEq and IsMPE;cbarFIA.The formalization commits to the following conventions:
tsum, which is summable under the standing assumptions.The boundary condition is not part of the definition: it is Proposition 1 (iii), and must be derived. Defining , or by formulas, or taking as a root of the printed (29), would trivialize or falsify the goal and is ruled out. Every equilibrium quantity is a field constrained only by the model's conditions. The existence part of Lemma 2 guards against vacuity.
Not formalized: Lemma 1 (the cut-off structure of the privacy decision, which the model builds in), the first sentence of Corollary 1, Corollary 2 (a graphical argument), the numerical Corollaries 3–4, and the PHI analysis (Lemma 4, Proposition 2).
Contributions are welcome at every milestone. The most reusable pieces are lemmas computing the derivatives of the period profit, the closed form of the expansion path, and the evaluation of the pivot series.
First-price sealed-bid auctions are used for procurement contracts, treasury securities, timber, and, since 2019, most display advertising. The classical advice for how to bid comes from Bayes–Nash equilibrium: each bidder knows the distribution of the others' values, and everyone plays the equilibrium. Practitioners rarely have that information. In a survey of auction consultants reported by Kasberger and Schlag, almost none of the respondents modelled equilibrium behaviour, and most named the distribution of rivals' bids as something they could not quantify.
Kasberger and Schlag (SSRN 3044438, version of 3 September 2022) propose a bid that needs no such prior. The bidder lists the bid distributions she considers conceivable and chooses the bid whose worst-case shortfall from the best response is smallest: the minimax loss bid (a criterion axiomatized by Milnor 1954, Hayashi 2008 and Stoye 2011). This mission formalizes the paper's choice-based recommendation, variation in bidding (§6.2), where the closed-form bid depends only on the number of bidders, a reserve level and one trust parameter.
There are bidders. Bidder 1 has value and bids ; the highest bid wins and pays its bid, and ties are broken uniformly at random. If bidders (bidder 1 included) tie at the top with , bidder 1 receives ; otherwise she receives .
A bid distribution is any joint law of the opponent bids. The expected utility of a bid is , and its loss is
Given an ambiguity set , the maximal loss of is , and a minimax loss bid minimizes it over all .
The ambiguity set of variation in bidding, , has three ingredients: a probability , a threshold below which no one bids, and a bid distribution . Each opponent is independently constrained with probability , and a constrained opponent bids an independent draw from . The unconstrained opponents bid a vector with an arbitrary joint law on , independent of who is constrained. Every such gives a member of . The salient choice is uniform on , with and
These are the utilities of bidding just above, respectively below, a common bid of all unconstrained opponents.
For uniform on , , and :
In the order the paper's proof uses them:
Proposition 4 turns a minimax problem over an infinite-dimensional set of joint distributions into a single equation in one variable. The resulting bid can be computed from , , and , and comes with a guarantee: against every environment in the loss is at most . The paper evaluates this guarantee at and tests the bid on field data. The monotonicity in is the robust analogue of the equilibrium fact that bids shade less as competition grows.
The result is proved in the paper; it has not been formalized anywhere. A machine-checked version adds three things. It fixes the ambiguity set: the printed set is too large, and the formal one is the version under which the statements hold. It records exactly which hypotheses the argument uses (, ). And it checks the analytic steps, whose printed versions contain small slips. The first-price model, the loss, and the minimax loss bid are reusable for the paper's other two recommendations (Propositions 1 and 5), which use different ambiguity sets.
The definition quantifies over every joint law of the unconstrained bids, including correlated and atomic ones. The crux is Lemma 1: one must show that, for each bid, collapsing all unconstrained mass to a single point (just below the best response when bidding too high, just above the own bid when bidding too low) does not decrease the loss. Some worst cases are limits of point masses approaching a tie, and the tie-breaking rule matters at those limits, so the argument has to work with suprema rather than maximizers.
A natural first idea is to argue coordinate by coordinate, moving one unconstrained bid at a time. It fails: the shift that raises the loss depends on the realized pattern of constrained bidders, and a profile that is worst for one pattern is not worst for another. Once Lemma 1 holds, the rest is one-variable analysis, but uniqueness of the root of (3) needs the strict decrease of , which uses in an essential way.
Opponents are indexed by Fin (n - 1); bids, values, and are reals and is a natural number with . The payoff splits ties evenly among all tied bidders, bidder 1 included. Expected utility is a Bochner integral of this bounded measurable payoff. Best utility and maximal loss are real suprema; they are finite because utilities of non-negative bids are at most and the ambiguity set is nonempty. The minimax loss bid is a predicate on bids , defined from the maximal loss and never from Equation (3); the goal quantifies over bids satisfying it.
is built as a pushforward: i.i.d. pairs (Bernoulli() coin, draw from ) for the opponents, independent of , with ranging over all probability measures on concentrated on . The printed definition (p. 20) lets the law of the unconstrained bids depend on who is constrained and allows bids below ; under it Lemma 1 and Propositions 3–4 fail for , so the corrected set is used and the affected items are labelled "corrected". Lemma 1, the p. 22 formula and Proposition 3 are stated for uniform; the paper states them for general , and for general continuous the claim of Proposition 3 that the minimax bid lies in fails numerically.
Restricting the ambiguity set to point masses, or defining the minimax bid as the root of (3), would make the goal trivial; neither is done. Contributions on the measure-theoretic layer (expected utility of a point-mass environment, the reduction of Lemma 1) are reusable for any first-price robust-bidding problem; the calculus milestones need only Mathlib's real analysis.
In many service systems a waiting customer is harmed not only by the time spent in line but also by the other customers met there. Contagion in a clinic, a pharmacy or a government office during an epidemic is the motivating example of Hassin, Meilijson and Perlman, Queueing with Negative Network Effects (SSRN 4097977, 2022; Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2023.1223). There the cost of joining a queue is a function of the number of meets, the customers present in the waiting room at the same time. A customer who joins a queue meets those ahead of her and those who arrive while she still waits. The second number is random and depends on the capacity of the waiting room, because arrivals that find the room full are turned away.
Strategic queueing in the tradition of Naor (1969) assumes a cost linear in waiting time; with negative network effects the relevant random variable is the count of meets, and equilibrium joining strategies and socially safe capacity regulations both require its exact distribution. Section 4 of the paper computes it: first as a row of a matrix power (Theorem 2), then in closed form, jointly with the number of arrivals that fill the room to capacity (Theorem 3). This mission formalizes that section.
An FCFS M/M/c/n queue has Poisson arrivals at rate , servers each working at exponential rate , and a waiting room of capacity : an arrival that finds customers waiting is lost. The server utilization factor is , and
is the probability that the next change of the queue is a service completion while all servers are busy.
A tagged customer arrives at position : customers wait ahead of her. The queue length is the number of waiting customers, herself included, not counting those in service. While she waits, every change of the queue is either a service completion (everybody moves up one place) or an arrival (which joins at the end if the queue length is below , and is lost otherwise). She enters service at the -th service completion.
For , and ,
with probability elsewhere; has the same law as ; and the expectation formula (4) for and the generating function (5) for , , hold. The statement depends on only through , as printed.
The result. Theorem 3 gives the exposure of a joining customer in closed form, as a finite sum of binomial terms in , instead of a power of an matrix. Through (5) it gives the expected utility of a customer facing the exponential loss , display (6), which is the input to the paper's equilibrium and safe-threshold computations for that loss function. The joint law with also records how often the room is filled to capacity during one customer's wait, the quantity that a capacity regulation acts on.
Formalizing it. The paper proves Theorem 3 in an Online Appendix that is not part of the preprint, and states (4) and (5) as straightforward corollaries. To the best of a search of the Prove2Me library, no transient result about a tagged customer in a finite-capacity queue, and no path count for a reflected walk with a capacity barrier, has been formalized. A complete development would give a machine-checked account of an embedded-chain argument, of the identification of the matrix , and of a reflection-type counting identity with two barriers.
The obvious route to is to enumerate the sequences of arrivals and completions until the -th completion. Two features break a plain ballot-type count. First, the walk is reflected at the capacity : an arrival at a full room is lost, so trajectories with the same number of joining arrivals do not have the same probability, as the paper remarks (p. 10). Only after also fixing do all trajectories become equally likely, which is why the closed form is a joint law. Second, the walk is absorbed when the customer enters service, so the count must also respect the lower boundary, and the subtracted binomial terms account for both constraints at once. Connecting the closed form back to the matrix of Theorem 2 requires identifying as the transition matrix of the queue size at consecutive service completions, a statement that itself relies on the memorylessness of the exponential clocks.
IsEventSeq). The reduction from the continuous-time queue to this sequence is the paper's own ("the probability that the next change will be a service completion", p. 9); it is disclosed, not formalized.Whether a customer joins a queue depends on how congested she believes it is. Classical strategic queueing studies two extremes. In the visible queue of Naor (1969) every arrival sees the queue length and joins exactly when her net payoff is nonnegative; in the invisible queue of Edelson and Hildebrand (1975) arrivals see nothing and act on the stationary distribution alone. Many service systems sit between the two: a call centre announces nothing, a restaurant can be inspected only at some effort, an online service shows a vague busy indicator. Customers there can learn about congestion, but learning costs time and attention.
Canyakmaz and Boyacı model this middle ground with rational inattention (Sims 2003; Matějka and McKay 2015): each customer chooses what to learn about the number of customers in the system, paying a cost proportional to the mutual information between what she learns and the true state, and then joins or balks. Because every customer's prior is the steady-state distribution generated by everyone else's joining behaviour, the model has a fixed-point structure, and the basic question is whether a consistent pattern of beliefs and behaviour exists and whether it is unique. Theorem 1 of the paper answers both questions affirmatively for every positive information cost. The paper's later results (comparative statics, revenue-maximizing prices, the limits of a visible and an invisible queue) are all statements about this unique equilibrium.
Customers arrive to a single-server first-come-first-served queue as a Poisson process with rate ; service times are exponential with rate ; . A served customer receives the reward , pays the price , and pays per unit of waiting time. A customer who finds customers in the system and joins gets the expected payoff
and it is assumed that , so . Balking is worth .
The customer does not see ; she holds a prior on it and pays per unit of mutual information acquired. The paper reduces her problem to a choice of the unconditional joining probability :
after which she joins in state with probability given by the generalized multinomial logit formula
If all customers use , the queue is a birth–death process with arrival rates and service rate . Its unnormalized weights are , ; when ( is admissible) the stationary law is .
An equilibrium (Definition 1) is an admissible such that, with and , the consistency equation holds and solves (9) under the prior .
For all parameters with and ,
No relation between and is assumed: when the equilibrium joining probability is strictly below one.
The milestones follow the paper's proof of Theorem 1 and its Lemmas 1 and 2:
Existence and uniqueness are what make the model usable. The paper's comparative statics in , , , (Proposition 1), its unimodal revenue curve (Proposition 2), and the limits and recovering Naor's and Edelson–Hildebrand's equilibria (Corollary 1) are all statements about "the" equilibrium; without Theorem 1 they would have no object. The result also shows that information frictions do not create multiplicity here, in contrast to many congestion games with strategic complementarities.
The result is proved in the paper; nothing in it is open. As far as a search of the Prove2Me library shows, none of it is formalized: there is no machine-checked treatment of rational-inattention choice in queues, of the reduced problem (9), or of the monotone comparative statics of birth–death stationary laws in a joining parameter used here. A formalization would produce reusable pieces for strategic queueing (product-form laws with state-dependent arrival rates, single-crossing of stationary distributions) and for rational inattention (the first-order characterization of binary choice with Shannon cost).
The obvious argument — the best response is continuous, starts at and ends at , so it crosses the diagonal — fails at the right endpoint when : then is not admissible, the stationary law does not exist there, and the inequality that the paper's intermediate-value argument uses is not available. The behaviour of the best response as has to be controlled by an argument the paper does not give.
The uniqueness step of the paper compares first-order conditions under two priors. Turning that comparison into a statement about maximizers requires handling the boundary solutions of (9), where the first-order condition is an inequality, and the endpoint , where is unbounded below and the derivative series may diverge.
All series are infinite: interchanging differentiation and summation, and continuity of in , need domination arguments that the paper does not spell out.
Everything is in OpaqueQueue.Equilibrium. Parameters form a structure Params with fields lam, mu, R, p, C, θ; the standing assumptions and are the predicate Params.Standing. Values are real; states are natural numbers; the logarithm is natural. joinProb P q n is , weight P q k is , Admissible P q is together with summability of , stat P q n is , obj P g x is the objective of (9) for a prior g, IsOptimal P g x says solves (9), and IsEquilibrium P q is Definition 1. stat divides by a series that Lean evaluates to when it diverges; every statement about it therefore assumes admissibility.
IsEquilibrium requires optimality of in (9) under the equilibrium prior, besides the printed equations (14)–(15). Those equations alone are satisfied by for every parameter value (and by whenever ), so reading Definition 1 without optimality would make Theorem 1 false. The paper's own proof uses the optimizer of (23) as the best response. Stating the goal as the existence of a unique fixed point of an arbitrary or choice-based best-response function would also be unfaithful and is ruled out.
Lemma 1 is stated for priors with finite mean, under which (9) is finite on all of . The paper states it for the joining policy of problem (6); the mission states it for problem (9), to which the paper reduces (6). The reduction itself (Matějka and McKay 2015; Caplin, Dean and Leahy 2016), Corollary 1, Propositions 1–4, Theorems 2–3 and the numerical sections are outside this mission.
A complete development needs: summability and continuity of parameter-dependent series, concave maximization on an interval with one-sided derivatives, and single-crossing and stochastic-dominance arguments for laws on . Proofs of individual milestones, alternative arguments, and general lemmas on product-form birth–death laws are all welcome.
Sell-side analysts are ranked against each other. Published rankings, such as Institutional Investor's annual "All-Star" ranking cited in the paper, and the career outcomes tied to them, reward an analyst for being more accurate than peers, not only for being accurate. A common intuition holds that such competition disciplines analysts and makes their forecasts more informative for investors. Sanjay Banerjee's paper Does Competition Improve Analysts' Forecast Informativeness? (working paper, Alberta School of Business Research Paper No. 2017-311, 2017; later published in Management Science, doi:10.1287/mnsc.2019.3544) asks whether that intuition survives a model in which analysts best-respond to each other strategically.
The paper places itself next to the multi-sender cheap-talk literature (Krishna and Morgan 2001, Battaglini 2002). There, several senders typically reveal more than one. Two features separate this model: forecasts are scored against the realised state, and analysts' private signals are correlated conditional on the state. Its main result identifies exactly when competition makes forecasts less informative.
A state has prior ; for measuring information, and , so . Two risk-neutral analysts each observe a private signal of precision . Given the state, the signals have correlation . With , each ordered pair of signals has conditional probability if both equal the state, if both differ from it, and if they disagree.
Each analyst forecasts . A symmetric strategy is , with and . Under competition, an analyst whose forecast alone matches the state earns , the other earns , and identical forecasts earn each, with . The payoff convexity is
and the payoff is convex if , concave if . In the benchmark, an analyst is paid for his own accuracy only.
A symmetric equilibrium is a with such that, for each signal, the prescribed probability of a truthful forecast maximises the analyst's expected payoff, computed by Bayes' rule, when the other analyst plays . It is pooling if and separating if . A most informative equilibrium is an equilibrium that is coordinatewise at least every other equilibrium of the same game. Forecast informativeness is the posterior precision normalised by the prior precision,
Finally, the separation threshold of the rank game is
Fix , and with , and restrict to , as the paper does ("Results for are symmetric"). Let and be most informative equilibria of the rank game and of the benchmark at . Then
and conversely, if and , then for every both most informative equilibria exist and every such pair satisfies .
The paper prints "". At informativeness still drops (for , , : ). On it does not drop, because the separating profile remains an equilibrium. The interval is the paper's own reading: " at " (p. 26).
The milestones are the paper's numbered results that the proof uses:
The result. Proposition 5 (B.1) is the paper's main counterintuitive finding. Convex rank incentives combined with correlated information make analysts understate their private signals in order to differentiate themselves, and the market learns less than it would from two analysts who ignore each other. The conditions are sharp: with uncorrelated signals or a concave payoff, competition never lowers informativeness at . This is relevant to the design of analyst rankings and of tournament incentives for forecasters more generally.
Formalizing it. The result is proved on paper through seven claims and a case analysis over regimes of . The case analysis contains slips, such as the empty interval in Lemma 1, a sign error in (B.28), and boundary cases and assigned to the wrong regime. A machine-checked proof would settle the exact statement. To the best of our knowledge none of these results has been formalized; the mission produces the first formal model of this game.
Each analyst's best response depends on the other's strategy through a conditional law of the other's forecast, which is affine in , and through Bayesian posteriors, which are ratios of such terms. The equilibrium conditions are therefore piecewise-affine inequalities whose sign pattern changes with . The obvious argument would compute a single equilibrium and compare informativeness. It fails because the goal speaks of the most informative equilibrium. One must show that no other equilibrium dominates it coordinatewise, and in the high-convexity, high-correlation regime the relevant equilibrium is fully mixed and is defined through an implicit root (). The "only if" half requires excluding a decrease in every other regime, including , where the benchmark pools and one needs .
States, signals and forecasts are Bool (true = H, h, ĥ). A strategy is a pair σ : ℝ × ℝ, and the equilibrium set carries the restriction of p. 9. Expected payoffs are conditional expectations of the rank payoff (3) under the joint signal law and Bayes' rule. The equilibrium condition is that the prescribed mixing probability maximises the expected payoff over all of . The benchmark pays for a correct forecast, a positive rescaling of the paper's . A forecast pair of probability zero contributes zero to the expected posterior variance. The paper's standing restriction is part of the goal: below one half the decrease occurs on the mirror interval , and the condition would be vacuous.
The trivializing formalizations are ruled out. The net payoffs and informativeness are computed from the primitives, never from the paper's closed forms (A.13)–(A.14) or Lemma 3. The "if" half asserts that the most informative equilibrium exists. The benchmark value is the benchmark game's own most informative equilibrium, not written into the statement.
The "Furthermore, the decrease in information revelation increases with payoff convexity" clause is not part of the goal. Neither are Proposition 5 (A) and (B.2), Propositions 2 (B) and 3 (B), Lemmas 2–3, Proposition 4, Claim 6 and Appendix C. Corrected milestones are labelled in their titles:
A complete development needs:
Bool;The finite Bayesian-game layer (symmetric equilibria of a two-player game with binary types) is reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of the goal from the milestones.
Naive Bayes is one of the oldest and cheapest classifiers for text and count data: given word counts for documents in two classes, it fits one multinomial distribution per class by maximum likelihood and classifies by the likelihood ratio. Its cost is a single pass over the data. In high-dimensional applications (text, genomics) one also wants the classifier to depend on few features, both for interpretability and to discard noise. Imposing that the two class distributions differ in at most coordinates turns maximum-likelihood fitting into a cardinality-constrained, nonconvex problem.
Askari, d'Aspremont and El Ghaoui (arXiv:1905.09884, Mathematics of Operations Research, 2024) show that the Lagrangian dual of this sparse problem is a one-dimensional convex problem solvable by bisection at essentially the cost of naive Bayes itself, and that its value is within a shift of four features of the true optimum. The shift comes from a duality-gap bound for separable problems in the line of Aubin and Ekeland (1976) and Ekeland and Temam, based on the Shapley–Folkman lemma.
There are features. A nonnegative data matrix with labels enters only through the class sums (the total count of each feature in each class), assumed entrywise positive. Write and .
The sparse multinomial naive Bayes problem (SMNB) at sparsity level is
where counts the coordinates in which the two class distributions differ. Without the last constraint the problem is ordinary naive Bayes.
For a vector , is the sum of its largest entries. Let
and . The relaxation (USMNB) has value
It is a convex problem in one variable. Its dual (D) is a concave maximization over with , which plays the role of a fractional feature-selection vector.
For ,
The constant four does not depend on , or the data. Numerically it is not tight (a shift of one suffices on random instances), but the goal keeps the paper's constant.
Milestones 1–6 follow the paper's proof of Theorem 3.6; milestones 7–9, on top of 1–4, are the paper's second, constructive route to the upper bound .
The theorem certifies that a convex problem of negligible cost brackets a nonconvex, combinatorial maximum-likelihood problem: the relaxation's value at lies between the true values at and . Whenever varies slowly in , which the paper observes past the "elbow" in the number of relevant features, the duality gap is small, and Propositions 3.8–3.9 turn the relaxation's solution into a sparse classifier with at most four extra features. The paper uses this to run feature selection on data sets with millions of features.
The results are proved in the paper (Theorem 3.5 is quoted from the literature). None is formalized. Formalizing them yields the perturbation-function duality-gap bound for separable nonconvex problems as a reusable statement, a verified variational formula for top- sums, and a check of a printed formula: the dual (D) as printed carries a spurious term , and the formal statement uses the corrected objective.
The lower and middle inequalities are weak duality once the dual is computed, and computing it is a separable calculation. The upper inequality is the content: it bounds a duality gap, and nothing in the one-dimensional structure of (USMNB) gives it. The naive approach, rounding the fractional of (D) to its top coordinates, has no a priori control on the loss. Both of the paper's routes need a Shapley–Folkman type argument, in which the number of nonconvex contributions is bounded by the number of constraints plus one. The Shapley–Folkman lemma itself is not in Mathlib (it is an open goal on the platform), and Theorem 3.5 also requires conjugates of extended-valued functions and the convex envelope of a sum of separable terms.
Features are indexed by Fin m, with fp fm : Fin m → ℝ entrywise positive. This positivity is stated on p. 7 and is needed because the formulas take . The standing assumption of §3.1 is carried by every statement about (SMNB). The commitments are:
EReal-valued functions on Fin d → ℝ. The conjugate is a supremum (p. 9 prints an infimum), and finiteness of each is added in Theorem 3.5 so that is a real vector.Proposition 3.8 is stated with the additional conclusion that the constructed point's value is at least the optimum of (D). Its proof establishes this, and without it the statement is met by a maximizer of and says nothing about (D).
A complete development needs Lagrangian duality for a separable problem, the perspective of , top- sums and their LP dual, Fenchel conjugates of extended-valued functions, and a Shapley–Folkman lemma. The last three are reusable well beyond this mission, and contributions there are welcome.
A seller of a product that gives immediate pleasure and delayed harm faces consumers who may plan to limit consumption and then consume more than planned. This setting applies to the paper's examples of cookies, soft drinks, cigarettes, and alcohol. A personal consumption goal is one way a consumer may restrain overconsumption. The question for the seller is whether that restraint calls for a lower or a higher price. In Amaldoss and Harutyunyan's model, both answers are possible: the direction changes with the harm from one unit of the product.
This mission formalizes the paper's comparison between the monopoly price when consumers set personal goals and the price when they have no goals. The comparison is Proposition 1 of the September 2022 SSRN version, p. 14 (PDF 15). The model is intentionally narrow. Consumers are identical, the seller has a single product, and all uncertainty is absent. These restrictions make it possible to isolate how a goal changes consumption and willingness to buy without attributing a price change to market heterogeneity or a change in production cost.
A unit mass of identical consumers obtains consumption value from quantity , where is the initial marginal value. Each unit causes delayed harm . A unit costs to buy. The seller's marginal production cost is normalized to zero. At the consumption stage, consumers discount harm by a present-bias factor with . Earlier, when deciding whether to buy and when choosing a goal, they count the harm without this discount. The quadratic coefficient is fixed at , as in §3 of the paper, pp. 7–9 (PDF 8–10).
A consumer may choose a personal goal . Consuming more than incurs goal disutility , with ; consuming no more than incurs none. Thus the benchmark utility when quantity is chosen is
and the utility with a goal is . The earlier planning-stage utility without a goal replaces by . With a goal, the same penalty is present at the goal-setting stage. These are the utilities in §4.1–4.2 of the paper, pp. 10–12 (PDF 11–13).
The sequence is price, purchase plan, personal-goal choice, quantity choice, and delayed harm. At the planning stage, a consumer correctly anticipates the subsequent goal and quantity choices. The consumer buys exactly when that anticipated utility is at least zero. Because the consumer mass is one, aggregate demand is the quantity purchased by one consumer. The seller chooses a nonnegative price that maximizes price times demand. The benchmark omits the goal and its penalty; the personal-goal regime includes both.
The supporting targets characterize the consumer's optimal quantity without a goal, benchmark demand, and the benchmark monopoly price; then optimal quantity at a fixed goal, optimal goal, the personal-goal reservation price, demand, and the personal-goal monopoly price. Each is indexed to an equation or paragraph in §4.1–4.2 of the SSRN version, pp. 10–14 (PDF 11–15).
The goal is Proposition 1. Define the comparison threshold
For , both monopoly problems have equilibrium prices. For any benchmark equilibrium price and personal-goal equilibrium price , the target is
The comparison does not assert a strict ordering at . The paper's statement describes more and less unhealthy products relative to ; its standing section range is (Proposition 1 and preceding paragraph, p. 14, PDF 15). The formal goal uses a strict upper endpoint for the price-uniqueness reason explained below.
The result identifies two opposing price outcomes under one behavioral change. A personal goal reduces the quantity purchased conditional on buying. It can also raise the price at which the consumer is willing to buy. Proposition 1 identifies which effect determines the monopoly price as harm varies. For a product below , the goal regime has the lower price; above , it has the higher price. The threshold is an explicit expression in valuation, present bias, and goal sensitivity, so the comparison is a parameter statement rather than a numerical illustration (Amaldoss and Harutyunyan, pp. 13–14, PDF 14–15).
The result is already proved in the paper, including a separate proof in the Web Appendix, pp. 2–4 (PDF 34–36). The proposed Lean statements have no machine-checked proofs yet. Formalizing this result would connect the paper's sequential consumer decisions to both monopoly optimization problems under one consistent set of definitions. The quantity, goal, participation, and price characterizations are useful beyond the final comparison: they state exactly where purchase on indifference and zero demand matter. They also provide a small reusable example of present-biased planning in a sequential pricing model.
The quantity choice changes formula at the goal: the goal penalty is active only above . Goal choice therefore depends on an anticipated optimum of a piecewise utility, while purchase depends on the utility of the resulting choice. A price that maximizes revenue must account for a jump from positive demand to zero demand at the consumer's reservation price. The tempting intuition that reduced conditional quantity always lowers the seller's optimal price fails because the purchase threshold also changes. The paper's two price formulas each have separate parameter regimes, and the comparison reverses only at the stated (§4.2 and Web Appendix, Proof of Proposition 1, pp. 12–14 and WA pp. 2–4).
All model quantities are real. Feasible purchase quantities, goals, and prices are nonnegative. The standing parameters satisfy , , , and ; Proposition 1 additionally assumes . The cost normalization and satiation coefficient are fixed. The goal penalty uses the strict indicator . A consumer buys when anticipated planning utility is nonnegative, including equality. This tie rule matters when the seller sets a reservation price.
The main comparison assumes . The paper takes in the remainder of the section, but at equality benchmark demand is zero at every nonnegative price, so every such price maximizes the same zero revenue. A comparison quantified over all equilibrium prices would then be false. The strict bound records this endpoint issue explicitly. Similar zero-consumption or zero-demand endpoints are excluded only where a milestone claims a unique goal or price.
The Lean definitions specify optimal quantities, optimal goals, demand, and monopoly prices through global maximization over the stated domains. Demand is derived from utility and the purchase rule. It is never defined by the closed-form equations that the milestones are meant to establish. This prevents the target from becoming true merely by defining prices to equal the paper's answers. The generic revenue-maximizer relation is a separate definition; the paper-specific model supplies its demand relations. A complete proof can use Mathlib's real-order and square-root theory together with reasoning about piecewise quadratic functions. Contributions that establish the consumer choices, purchase threshold, demand, or either price characterization are within scope.
Charity watchdogs rate nonprofits by their program expense ratio, the share of spending that goes to programs rather than to administration and fundraising, and donors reward a high ratio. Practitioners have long argued that this pressure produces a nonprofit starvation cycle: organizations underinvest in administration, the infrastructure that sustains their capacity to deliver services, and their capacity erodes (Goggins Gregory & Howard, Stanford Social Innovation Review, 2009). Whether a nonprofit that maximizes the needs it meets should in fact starve administration is an optimization question, and Kotsi, Aflaki, Aydin and Pedraza-Martinez pose it as a two-period budget-allocation problem (SSRN 3460795; later published in Manufacturing & Service Operations Management, DOI 10.1287/msom.2020.0660). Their main structural result, Proposition 1, says that the answer depends on the nonprofit's current capacity through two thresholds.
A nonprofit lives for two periods. In period it has budget , needs and capacity . Each program dollar meets dollars of needs, with . Keeping capacity costs the required administration , convex and nondecreasing. Spending on discretionary administration raises next period's capacity to , where , is strictly concave and strictly increasing, and . Spending on program, on discretionary administration and on fundraising raises the donations
where is concave and nondecreasing on , with and for . Donations depend on the program expense ratio .
The second-period needs are a random variable with a density. The net budgets are and , and the program ceiling is . Throughout, . Lemma 1 reduces the two-period dynamic program to problem (2):
subject to , , and . The last constraint says the second-period budget never exceeds what the second-period capacity can use. The allocation exhausts capacity when that constraint binds, and leaves capacity unused when it is slack.
Fix all data except . Problem (2) has an optimal allocation for every admissible , and there are thresholds such that every optimal allocation satisfies the following.
The thresholds are asserted to exist; no formula for them is part of the goal.
The milestones follow the appendix proof:
Proposition 1 gives the structure of the optimal policy. Spending on administration is optimal at low capacity. At moderate capacity, the nonprofit spends on administration only when the program ceiling binds. Starving administration while leaving capacity unused is optimal only at high capacity. This turns the starvation-cycle debate into a statement about where a given nonprofit sits relative to and . The paper's case study and numerical sections build on this classification.
The paper proves the result by hand, with implicit-function calculus over several threshold functions of . No machine-checked version exists. A formal proof would confirm the case analysis, including the boundary cases that the printed statement gets wrong (see Formalization scope). It would also produce reusable facts about the concave function and about one-parameter families of concave programs.
Problem (2) is not concave in , because the donation term divides by the total spending. So the Karush–Kuhn–Tucker conditions are neither necessary nor sufficient, and no general convexity argument applies. The proof splits on whether the capacity constraint binds. Each branch has its own maximizer and its own thresholds in (, , ), and these move with . The goal then requires comparing the two branches uniformly in . A threshold in exists only if certain differences of these maximizers are monotone in , and that monotonicity comes from second-order implicit differentiation of the root of equation (4). A pointwise analysis at a fixed does not give the thresholds.
All quantities are real. The data form a structure Params, and is the law of . The capacity is a separate argument, quantified over the paper's range , . The expectation is an integral against . An optimal allocation is a feasible point whose objective is at least that of every feasible point. The goal asserts existence separately and then quantifies over all optimal allocations.
Added hypotheses. The formalization adds the following to the page's assumptions:
Strictness and full support are needed for the uniqueness claims. Without them, can be flat at its maximum, and optimal allocations can fall in two cases at once. Full support is how "Ψ can take any value in " is read.
Repairs to the printed statements. Each is disclosed in the item concerned.
The comparison "" is stated as a condition on , not as a defined number. The thresholds , the root and the maximizers enter as variables characterized by hypotheses.
Ruled out. The thresholds are chosen once for all admissible , and the goal includes existence of an optimum. So the goal cannot hold vacuously, and it cannot be met by thresholds that depend on .
Infrastructure. A complete development needs the following:
The first and last are reusable beyond this mission. Contributions toward any milestone, or toward these general lemmas, are welcome.
When a financial institution fails, its counterparties on over-the-counter derivatives are exempt from the automatic stay of bankruptcy: they may terminate their contracts at once, accelerate what is owed to them, and seize posted collateral. Whether this exemption stabilizes or destabilizes the system has been debated since the 1990s, and the failure of Lehman Brothers in 2008 sharpened the question. Termination turns contingent contract values into immediate payment obligations, which can push further institutions into default. But it also brings cash into the system and frees collateral, which can let other obligations be met.
Ghamami, Glasserman and Young (Management Science, 2022) build a clearing model in which payments, collateral seizure, returned collateral and contract termination interact over successive rounds. They compare two policies. Under full termination the default of a node accelerates every derivative contract it is party to, in both directions. Under selective termination (creditor "cherry-picking") only the obligations of the defaulted node become due. Their headline comparison is that, under a bound on aggregate derivatives leverage, full termination leaves no larger system-wide payment shortfall than selective termination.
A finite set of nodes. For nodes : is the payment due from to , with total ; is the cash of ; is the collateral posted by for its obligations to ; is the value to of its derivatives with , owed by on termination, with . Diagonals vanish and obligations are netted (). Collateral has constant value .
Round 1. Given payments , node has assets and defaults if ; is the default set. A creditor of a defaulted first seizes , and the rest of 's assets is shared pro rata over the residual claims . Clearing payments are the nonnegative solutions of these fixed-point equations. Excess collateral is returned after Round 1: a defaulted node gets back what was not seized, a surviving node gets back what it had posted to defaulted nodes.
Proposition 2.1 also treats a Round 2 without derivative termination: remaining obligations are , paid from returned collateral and incoming payments. Its total-payment identity (15) is included.
Rounds under full termination. A default in round creates the obligation between the defaulted node and each counterparty that has survived; unpaid obligations carry over; two survivors owe each other nothing. A node's assets in round are its cash , its returned collateral and the payments it receives; it defaults in round if they fall short of its round- obligations, and payments again solve a pro rata fixed-point equation. is the full-termination default set.
Selective termination shares Round 1, and in Round 2 only defaulted nodes owe: for , else . No node defaults after Round 1, and payments solve the Round-2 equation.
The payment shortfalls are
with the total paid by over all rounds and its total over the two selective rounds. The net worth at the end of Round 1 is .
With constant collateral price, common first-round payments, and both models taken at their largest, or both at their smallest, second-round clearing payments ((37) or (38)), the aggregate derivatives leverage condition
implies
The result. Proposition 5.2 is the paper's formal answer to the policy question raised by the safe-harbor debate: it identifies a balance-sheet condition, derivatives liabilities bounded by equity in aggregate, under which the stay exemption does not worsen the total amount of unpaid obligations, even though full termination always produces at least as many defaults (Proposition 5.1). The paper's Example 5.1 shows that without such a condition the comparison can go either way and by arbitrary amounts.
Formalizing it. The paper gives proofs; none is machine-checked. A formalization fixes the accounting of a multi-round collateralized clearing model precisely. This matters here: read literally, the cash recursion of §4 drops unsold returned collateral, and with it Proposition 5.2 (i) fails on a four-node network. The mission states the repaired accounting under which the paper's argument goes through. It also produces reusable statements about extremal fixed points of Eisenberg–Noe-type clearing maps with collateral and their monotone comparison.
The two models are compared at fixed points of different maps, and fixed points need not be unique; a pointwise comparison of arbitrary solutions is false in general. The comparison has to be made at extremal fixed points, through monotone comparative statics in the parameters (obligations and pro rata proportions), and both the largest and the smallest cases are needed. Second, full termination runs up to rounds with new defaults in each; the shortfall bound requires tracking each node's cash, returned collateral and payments across rounds, and showing that a node defaulting after Round 1 has paid out at least its Round-1 net worth. The tempting shortcut, assuming that full termination creates no new defaults (), turns the goal into Corollary 5.1, a different and weaker statement.
All values are real numbers; nodes form a Fintype with decidable equality. One definitions file CollatNet.Termination.Model holds the network, its standing assumptions, Round 1, the §2.3 freed-collateral Round 2, a round state (cash, returned collateral, obligations, survivors), the full-termination round map, the selective Round 2, default sets, shortfalls and net worth. Conventions:
IsGreatest/IsLeast in the componentwise order on each model's round-2 clearing set; later full-termination rounds may be any clearing payments.Case (ii) of Proposition 5.2 (illiquid collateral, no excess collateral) is not posed: it is false as printed, because returned collateral is sold below its Round-1 value.
The goal must keep (40) as its hypothesis. Replacing (40) by , or dropping the later full-termination rounds (which forces by construction), would state Corollary 5.1 instead.
Needed infrastructure: Knaster–Tarski on boxes in (Mathlib's OrderHom.lfp/gfp), a monotone comparison of extremal fixed points, and finite-sum bookkeeping over rounds. The extremal-fixed-point comparison and the node-total property of pro rata clearing are reusable for other clearing models. Proofs of any milestone are welcome; the shortfall identity and the dominance of round-2 parameters are the most self-contained.
Firms that collaborate on research and development must share proprietary knowledge to make the collaboration work, yet the knowledge they share can later be used against them: a partner that has learned from the alliance can walk away and use what it learned on a rival project. Management research calls this the appropriability hazard of alliances. Arora, Belenzon and Patacconi (Management Science, 2021) model knowledge sharing as a property-rights problem in the tradition of Grossman–Hart and Hart and Moore (1990): knowledge sharing is an ex ante investment that shifts the partners' ex post outside options, and payoffs are fixed by bargaining after the investment is sunk.
The paper's main structural question is whether a firm can mitigate the hazard by organising its collaborations as a portfolio of alliances rather than as a single alliance. The answer it gives, Proposition 6, is that it can: there is a range of parameters in which a single alliance cannot sustain knowledge sharing while a portfolio of two alliances can.
Single alliance (§2). A focal firm and a partner each pay a private cost , with , to share knowledge. After sharing, implementing the project together creates value ; if the alliance is terminated prematurely, and obtain their ex post outside options and . It is assumed that . Bargaining follows the Nash solution with equal weights, so firm obtains
Firm 's knowledge-sharing constraint is . Knowledge sharing is efficient if .
Alliance portfolio (§4.1). The focal firm now has two partners and , on the player set . The partners' outside options are normalised to . After knowledge sharing in both alliances, the value created by a coalition that implements together while its alliances with outsiders are terminated is (Table 1)
with . The parameter is the synergy between and in implementation, measures substitutability in implementation and measures substitutability in rival benefits. Gross payoffs are the Shapley value
and since bears in each of its two alliances, the net payoffs are , and . Knowledge sharing in a configuration is feasible when every firm's knowledge-sharing constraint holds.
Under the standing assumptions, suppose . If
then knowledge sharing in the portfolio is feasible (), while knowledge sharing in the single – alliance (with ) is not.
The result. Proposition 1 shows that in a single alliance, efficiency () does not imply investment: shifts in bargaining positions, measured by , create underinvestment. Proposition 6 identifies a structural remedy. A second partner changes the bargaining game: the synergy is created only when all three firms cooperate, and substitutability in rival benefits weakens the focal firm's threat point, both of which raise the weak partners' Shapley payoffs. The paper uses this to argue that alliance portfolios with the right characteristics can sustain knowledge sharing that a dyadic alliance cannot, and that substitutability among partners is not uniformly harmful.
Formalizing it. The proofs are relegated to an online appendix that is not part of the source manuscript, so the mission produces the first complete, checked derivation of the portfolio result from the model's primitives: the Table 1 game, the Shapley value and the cost allocation. A search of the platform found none of these statements already formalized; the Shapley value itself is reused from an existing platform definition.
The computations are finite and elementary, so the difficulty lies in carrying out the Shapley sum over all coalitions of a three-player game honestly, rather than by quoting the closed forms (9)–(10), and in tracking the asymmetric cost allocation: the focal firm pays , the partners each. A second point is that the paper assumes the focal firm's constraint "to facilitate the comparison"; the formal goal concludes it from and the standing ranges, so it must be derived, not assumed.
Players are Fin 3 with , , ; all parameters are real numbers. The game game V b πF sImp sRB assigns to every coalition without and, to a coalition containing , the Table 1 value determined by its size, with . The gross payoffs are the platform's published Supermodularity.Cooperative.ShapleyValue applied to this game. Single-alliance payoffs follow eq. (1), and both notions of feasibility are defined from the payoffs: SingleFeasible is , PortfolioFeasible is for every player. The standing assumptions , , and are bundled in Standing. "Feasible" refers only to the knowledge-sharing constraints; the coordination problem of the investment game (footnote 10) is ignored, as in the paper.
A trivializing formalization would define by the closed forms (9)–(10) or feasibility by the inequalities (5) or (11), which would make the milestones true by definition and the goal a linear inequality between its own hypotheses; the definitions here are the Shapley sum and the payoff constraints, so those closed forms must be proved.
No probability, measure theory or analysis is needed; a development needs finite sums over the powerset of Fin 3 and linear arithmetic over ℝ. A reusable by-product is a computation of the Shapley value for three-player games with a distinguished player, which recurs in property-rights models. Proofs of the milestones and of the goal, in any order, are welcome.
A client who needs to buy a security may hire a dealer to execute the purchase. The client can observe market prices and trading volume but cannot observe the dealer's trades or the market conditions known to the dealer before trading. A contract based on the closing price or another benchmark can therefore change the dealer's incentives. Baldauf, Frei, and Mollner study when a familiar benchmark, the volume weighted average price (VWAP), implements the outcome the client would choose if the client could control the trades directly (Baldauf, Frei, and Mollner, 2022, §§3–5 of the August 8, 2020 working paper). The question matters wherever a benchmark price determines the payment for an order that an intermediary also influences through its execution.
A client asks a dealer to acquire one share over a finite number of periods. A trading schedule is a vector with and . Before trading, the dealer sees a vector of positive market conditions ; the client does not. Neither party observes the price shocks in advance. In the specialized model, the dealer chooses a static policy , so the whole schedule depends only on and cannot react to prices realized during trading. These information and policy restrictions are stated in §§3.1 and 4.1 of the working paper.
Period has price and total market volume . The paper assumes that is strictly increasing, is strictly convex, is positive on the relevant domain, and for , where is strictly decreasing. Every shock has the same conditional mean: almost surely. The paper imposes no independence or identical distribution requirement on the components of or . The dealer's utility is strictly increasing and concave.
A contract specifies the client's payment using only the observed price and volume vectors. The dealer's monetary payoff is , and the dealer's expected utility must be at least , the utility from rejecting the contract. Incentive compatibility means that the recommended policy maximizes the dealer's expected utility among static policies. The client chooses a contract and a recommended policy to minimize subject to those two constraints. This is the paper's second best problem; an optimal contract is part of a solution. The VWAP contract pays the realized volume weighted average price, (working paper, pp. 10–12, 21–22).
The paper identifies the first best policy, the schedule the client would choose with direct control of trading:
Its expected trading cost is , and its share of each period's total market volume is . The mission includes Lemmas 10 and 11 on conditional means (their static case 1), both parts of Lemma 12's weighted inequality, the Jensen step of the proof of Lemma 3, the three sentences of Lemma 3 (the first best policy and its uniqueness, its expected cost, and its volume shares) as separate statements, and the sufficiency part of Lemma 4. It also records the full insurance and strict incentive claims stated in the proof of Proposition 5. These are the results the paper uses to reach its main assertion (working paper, pp. 21–23, 44–47, 50–53).
Proposition 5 says that the VWAP contract itself solves the client's second best problem:
The comparison covers every measurable contract on prices and volumes and every admissible static policy. The goal does not select an impact function, a volume law, or a utility curve beyond the paper's assumptions (working paper, Proposition 5, p. 22).
Proposition 5 gives a condition under which a common benchmark contract reaches the same expected payment as direct control of the dealer's trading. The result links the first best schedule, the realized VWAP, and the dealer's incentives without specifying a distribution for market conditions or independent price shocks. Under the contract, the first best schedule leaves the dealer with zero realized monetary surplus, while other static schedules yield strictly lower expected utility in the paper's model (working paper, pp. 22–23 and proof on p. 53).
The published paper proves these statements. They do not yet have machine checked Lean proofs. A complete development would supply reusable definitions for static execution policies, price and volume outcomes, contracting constraints, and conditional cost comparisons, together with proofs of the paper's auxiliary inequalities.
A direct comparison of expected VWAP payments across schedules does not establish incentive compatibility: the dealer cares about expected utility of payment minus trading cost, and both terms change when the dealer changes the schedule. The relevant volume weights depend on the same schedule that changes price impact. The key difficulty is the strict equality case in Lemma 12's weighted inequality, including periods in which the dealer trades zero shares. Conditional means must also be carried through schedule dependent but measurable weights, while the final client comparison ranges over all feasible measurable contracts. Dropping that broad comparison would state a substantially weaker result (working paper, Lemmas 10–12 and proof of Proposition 5).
Time is indexed by Fin T, with paper period represented by Lean index . The probability space is arbitrary, its measure is a probability measure, and . Market conditions are positive at every outcome. Shocks are integrable and have conditional mean given the sigma algebra generated by . The model assumes measurability of , , , and ; it also assumes integrability of so the stated first best cost is finite. These measurability and integrability clauses make explicit conditions used by the paper's expectations but not separately listed there.
Policies are measurable maps from to schedules on the positive market condition domain; Lemmas 10 and 11 (case 1) are stated, as in the paper's appendix, in a general framework with only their own hypotheses: Lemma 10 for measurable functions of summing to one almost surely (with integrable), Lemma 11 for measurable nonnegative functions of that need not sum to one and any positive measurable volume function . Contracts are measurable functions of the price and volume vectors; their values off positive volume vectors are irrelevant. Feasible contract policy pairs require finite expected payment, cost, and dealer utility. Incentive compatibility compares against static deviations with integrable utility; under VWAP the omitted deviations cannot improve the dealer's expected utility, while this convention makes the competing contract class at least as demanding for optimality. First best is expressed by almost sure comparison of conditional expected costs. The properties of and are imposed on the nonnegative and positive arguments actually used by schedules. Positivity of volumes makes the VWAP denominator nonzero on realized outcomes. These conventions exclude empty schedules, division by zero at realized conditions, and Lean's default zero integral for nonintegrable payoffs.
The mission needs Mathlib's measurable functions, conditional expectations, Bochner integrals, finite sums, convexity, and almost everywhere relations. Its model definitions and the deterministic statements (Lemma 12, the Jensen step and the volume-share identity of Lemma 3, stated for arbitrary , , and every number of periods) are meant to be reusable. Contributions may prove the conditional mean lemmas, the deterministic inequality and equality case, the first best characterization, the sufficiency criterion, or the proposition. The goal must retain all measurable contracts and feasible static policies; restricting competitors to benchmark contracts or asserting only incentive compatibility would trivialize the intended optimality claim.
How many ways can a closed orientable surface of genus be "coloured" by a finite group ? Precisely: how many group homomorphisms are there? The answer is the partition function of two-dimensional Dijkgraaf–Witten theory with gauge group . That theory is the simplest topological quantum field theory (TQFT) in the sense of Atiyah and Segal, and the standard test case for gauge theory with a finite gauge group (Dijkgraaf–Witten 1990, Freed–Quinn 1993). The count has a closed form in terms of the dimensions of the irreducible representations of alone. It is known as Mednykh's formula.
Timeline. Frobenius (1896) counted pairs with a prescribed commutator, , in terms of characters, which is the genus-one case. Frobenius and Schur (1906) treated the non-orientable analogue. Mednykh (1978) proved the formula for every genus using character theory and the standard presentation of . It was rediscovered in physics as the partition function of 2D and 3D finite-gauge-group TQFTs (Freed–Quinn 1993), and reproved with matrix integrals (Mulase–Yu 2005) and with lattice TQFTs (Snyder 2007). The last paper fixes the form of the statement used here.
Let be a finite group. A surface tuple of genus in is a family . Its commutator product is
multiplied left to right. For let (commCount G g z). The surface group (SurfaceGroup g) is the presented group
the standard presentation of the fundamental group of the closed orientable surface of genus , whose Euler characteristic is .
A complete irreducible family (IrrepFamily G ι) is a finite family of finite-dimensional complex representations of that are irreducible, pairwise non-isomorphic, and such that every irreducible finite-dimensional complex representation is isomorphic to some . Write and for the character.
For every finite group , every complete irreducible family and every ,
which is Mulase–Yu, Thm. 1.1 and Snyder, eq. (1) with . Equivalently, . Exponents are integers: at the formula reads .
The milestones follow the algebraic proof of the counting formula recorded in Mulase–Yu 2002, §4, which goes back to Frobenius and Mednykh. Write for the convolution of functions on .
The result. The formula says that the number of -coloured genus- surfaces is a function of the multiset of irreducible dimensions alone. Two groups with the same character degrees (for example and , both with degrees ) have equally many homomorphisms from every surface group, even though the groups are not isomorphic. In TQFT language the left side is the evaluation of the Frobenius algebra , where is its handle element. The right side is the gauge-theoretic state sum. The identity is the two-dimensional instance of the agreement between the Atiyah–Segal gluing description and the path-integral description of a TQFT. It also gives the volume of the moduli space of flat -bundles on , and it underlies counts of covering spaces of surfaces.
Formalizing it. The theorem is classical and fully proved; to our knowledge it has no machine-checked proof. Mathlib has characters of finite-dimensional representations, their orthonormality (FDRep.char_orthonormal) and Maschke's theorem. It lacks the completeness of irreducible characters, the column orthogonality relation (M2), and any statement linking class sums to characters (M3). These are reusable well beyond this mission. The mission also produces the first formal link between a surface-group presentation and representation theory.
The available orthogonality is the row relation between two irreducible characters. Every step here needs the column relation M2, . That relation is equivalent to the decomposition of the regular representation , and in particular to the finiteness and completeness of the irreducible family. Mathlib has no such decomposition. The convolution identity M4 must also be established in its non-isomorphic case, which the row relation alone does not give in convolution form. The passage from to tuples (M1) depends on the universal property of PresentedGroup and on using one ordering of the commutator product throughout. A proof that bypasses characters by brute counting is not available for general .
All representations are over : FDRep ℂ G with G : Type a Group with [Fintype G]. Characters are FDRep.character and is Module.finrank ℂ (V i). Counts are Nat.card. Powers with exponents depending on are integer powers (zpow) in , so is included and no natural-number truncation occurs. is PresentedGroup on generators Fin g × Bool, with , and the single relator (List.ofFn fun j => ⁅a_j, b_j⁆).prod. This is the standard presentation and stands in for , since Mathlib has no fundamental groups of closed surfaces. The goal quantifies over every complete irreducible family. M0 shows that such families exist, so the goal is not vacuous. Because the family must be complete and pairwise non-isomorphic, it cannot be chosen to make the sums trivial.
Out of scope: the non-orientable formula of Frobenius–Schur (it needs Frobenius–Schur indicators), positive characteristic, and the bordism-category formulation of TQFTs. Reusable contributions are especially welcome: the decomposition of the regular representation, column orthogonality, and the class-sum Schur lemma.