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?
Online platforms (labor marketplaces, review sites, crowdsourcing services) rely on feedback from their users: did the plumber arrive on time, is this image labelled correctly. The answers cannot be checked against ground truth, so a platform that rewards feedback must reward it by comparing it with other users' answers. This is the problem of peer prediction, or information elicitation without verification. The classical mechanisms of Miller, Resnick and Zeckhauser (2005) and Prelec (2004) make truthful reporting an equilibrium, but they either need the designer to know the joint distribution of the users' observations or ask users for extra reports (predictions of others' answers). Both requirements are unrealistic on a large platform.
Kamble, Shah, Marn, Parekh and Ramchandran propose the square root agreement rule (SRA). It uses only the users' answers, needs no knowledge of the distribution, and works when users perform many statistically similar tasks. A second difficulty of peer prediction is that uninformative coordinated behavior (everyone answers "yes") is often also an equilibrium, sometimes a better-paying one. The paper's main result says that, with many tasks, SRA makes truthful reporting a strict equilibrium whose payoff is within any prescribed of the best symmetric equilibrium.
Timeline. Output agreement and the peer-prediction method (Miller, Resnick, Zeckhauser 2005) require a known prior. The Bayesian truth serum (Prelec 2004) and its robust variants ask for prediction reports. Multi-task mechanisms (Dasgupta and Ghosh 2013; Shnayder, Agarwal, Frongillo and Parkes 2016) estimate the statistics from other tasks and obtain informed truthfulness under correlation assumptions. SRA (arXiv 2015, Management Science 2023) obtains strict truthfulness for every separated model and approximate payoff dominance over symmetric equilibria.
There are evaluation tasks and agents. Agent performs the tasks ; task is performed by the agents , with . Each task concerns an entity whose type lies in a finite set ; types are i.i.d. with law . An agent observes an answer in a finite set , drawn independently from . The pair is the generating model.
A reporting strategy gives, for each observation , a distribution over reported answers. The truthful strategy reports what it observes; a fully informative strategy reports for a fixed permutation of . A profile is symmetric if all agents use the same strategy.
SRA (Mechanism 1). For every task pick two distinct agents , and let
with . On each of her tasks , agent is paid if she and her peer both report , and otherwise. Rare agreements pay more.
A profile is a Bayes–Nash equilibrium if no agent can raise her expected payment by changing her own strategies, and a strict one if every change on her tasks lowers it. With , the Cauchy–Schwarz gap is
and the model is -separated if . The square root agreement measure is , and the uninformativeness of is .
For every , and there is such that for every -separated model, every and every allocation with :
for every symmetric BNE , every permutation and every agent . No constant is hard-coded: is only asserted to exist, uniformly over all models with the same .
Theorem 1 gives a detail-free mechanism: the designer needs neither nor , and the agents need only know that the model is -separated. The guaranteed gap over observation-independent reporting lets a platform pay for effort by scaling . Theorem 2 addresses equilibrium multiplicity, the main criticism of agreement-based mechanisms: no symmetric equilibrium can pay noticeably more than truthful reporting. Proposition 5.1 is a quantitative data-processing inequality for the square root agreement measure, of independent interest.
All statements are proved in the paper (arXiv:1507.07045v5, Appendix A). None has a machine-checked proof. The mission asks for formal proofs of the stated results with uniform in the model; explicit bounds on and alternative arguments for the second claim of Theorem 2 are welcome.
The payments are inverse square roots of empirical frequencies, so their expectations do not follow from the law of large numbers alone: a bound uniform over all -separated models is required, and it must be uniform in the answer . For a general symmetric profile the agreement probability of some answer can be arbitrarily close to , so no uniform concentration bound for holds across all symmetric profiles; the obvious argument "compare the limit payoffs " therefore does not transfer to finite directly. Finally, the expectations are over a product space of types, observations and reports of all agents on all tasks, and the independence structure (payments of never read her own reports) has to be made explicit.
Types, answers, tasks and agents are Fin m, Fin k, Fin N, Fin M; all quantities are real. A strategy is q : Fin k → Fin k → ℝ with q obs ans the probability of reporting ans after observing obs; models and strategies are required to be stochastic. A Setting holds the allocation together with the mechanism's choices (peers and the pairs ), and every theorem quantifies over all legal choices after . Every (task, agent) pair carries an observation and a report; entries of agents not assigned to a task are never read by a payment and marginalize out. The expected payment is the explicit finite sum, over all types, observations and reports, of the product probability times the payment; deviations change only the deviating agent's strategies on her own tasks, and strictness is over deviations that change some strategy on her tasks. "Commonly known" has no formal content beyond computing expectations under the true model. The printed "" is read as ; Theorem 1's second claim assumes . is when , so the separated theorems are vacuous there, as the page's is undefined.
Expected payments are not defined by (31) or by the limit formulas , and never depends on the model, the population or the mechanism's choices: either shortcut would make the targets trivial or strictly weaker.
A complete development needs binomial tail bounds (Hoeffding), moment bounds for inverse square roots of binomials, Cauchy–Schwarz on finite sums and the marginalization of product measures over finite types; the last two are reusable for other multi-task peer-prediction mechanisms. Proofs of any milestone are welcome.
In Illinois Brick Co. v. Illinois (431 U.S. 720, 1977) the U.S. Supreme Court held that only direct purchasers may recover antitrust damages; an indirect purchaser, who bought the overpriced goods through an intermediary, may not sue on the ground that the overcharge was passed on to it. In a three-tier supply chain of manufacturers, retailers and consumers, this IB ruling leaves the consumers without standing against colluding manufacturers. Only the retailers can sue, and a retailer sues only if collusion has cost it profit.
Jain, Hasija and Netessine (Management Science, 2021) ask which supply-chain contracts let competing manufacturers collude under this rule. They compare five common contract structures: wholesale price, revenue sharing, quantity discount, wholesale price plus fixed fee, and minimum order quantity. Their answer is that under the IB ruling only the contract with a fixed fee supports a cartel, and that the fee then takes the form of a slotting fee paid by the manufacturers to the retailers. Under competition all five contracts give the same outcome. The result tells public enforcers where to look: supply chains that use slotting fees.
Two manufacturers make a homogeneous product at common marginal cost . Two retailers buy quantities and sell them in a market with deterministic inverse demand
Retailer buys from manufacturer . A manufacturer's payment terms fix the payment a retailer makes for quantity when its sales revenue is (Table 1 of the paper):
| Contract | Terms | |
|---|---|---|
| Wholesale price (WP) | ||
| Revenue sharing (RS) | , | |
| Quantity discount (QD) | , | if ; otherwise |
| WP plus fixed fee (WPFF) | , | |
| Minimum order quantity (MOQ) | , | , purchases restricted to |
With revenue , retailer earns and manufacturer earns . A retailer equilibrium under is a pair of feasible quantities in which each maximizes given the rival's quantity.
The competitive terms of Proposition 1 set and all other terms to , except that under MOQ the minimum is . Terms with retailer equilibrium meet the cartel conditions against a retailer equilibrium under when
Condition (C1) is the manufacturers' motive to collude. Condition (C2) is what keeps the retailers, the only parties with standing, from suing.
For every contract a competitive retailer equilibrium exists, and
The goal fixes no collusive terms; it asserts only which contracts admit a cartel.
The result. Proposition 2 separates contracts that are equivalent under competition. Under the IB ruling the manufacturers prefer the fixed-fee contract because it is the one under which they can collude without being sued. Slotting fees are usually explained by demand signalling, risk sharing or retailer power; the paper adds a further explanation, as a way of paying off the only plaintiffs who could sue. For antitrust practice it identifies supply chains with heavy slotting fees as the place to look for cartels. The other four contracts need no such scrutiny under this ruling.
Formalizing it. The paper's proofs are in an online appendix and are not reproduced in the article. The mission produces a machine-checked version of the deterministic-demand model and of its two central propositions, stated over arbitrary admissible terms (including unequal terms for the two manufacturers) and over every retailer equilibrium rather than a selected one. No part of this model or result has a machine-checked proof yet.
Part (b) is an existence claim with a two-sided requirement: the witnessing terms must admit a retailer equilibrium, and every retailer equilibrium they admit must satisfy (C1) and (C2). A fixed fee makes a retailer's profit discontinuous at , so the best responses and the uniqueness of the equilibrium need care.
Part (a) is a negative statement over all admissible terms of four different contracts. Solving each contract's retailer game in closed form and then comparing the profits does not work: the quantity-discount schedule is piecewise, its profit need not be concave when is large, the minimum order quantity can bind at a corner, and the two manufacturers may offer different terms.
All objects are in the namespace IllinoisBrick.Cartel; equilibrium is the published generic pure Nash relation CarbonDoubleCount.Planner.IsPureNash. The conventions are:
Several readings would trivialize the goal, and the statement rules each of them out. The competitive profits are computed in the model at , not hard-coded. Part (a) covers all four contracts and unequal terms. Part (b) requires the cartel conditions at every retailer equilibrium of the witnessing terms, together with existence of one. Retailer equilibrium is a best-response predicate, never a closed-form formula.
Not formalized: the manufacturers' equilibrium part of Proposition 1 (that solves problem (3), which needs a sourcing rule for unequal offers the paper does not give), Propositions 3–11, consumer surplus and condition (C3), and stochastic demand. Proofs of any milestone are welcome. The equilibrium lemmas for linear Cournot games with transfer payments (milestones 2 and 3) are reusable for other supply-chain contract models.
Many learning problems are instances of the stochastic program
where the law of the data is unknown and only an i.i.d. sample is available. When is non-convex, gradient methods may stall at local minima or saddle points, and a guarantee on the population risk , with , requires controlling optimisation, discretisation and generalisation at once.
Langevin-type algorithms inject Gaussian noise into stochastic gradient steps so that the iterates approximately sample from a Gibbs law concentrated near global minimisers. X. Gao, M. Gürbüzbalaban and L. Zhu (arXiv:1809.04618, Operations Research 2022) prove explicit, non-asymptotic population-risk bounds for stochastic gradient Hamiltonian Monte Carlo (SGHMC), the momentum-based variant.
Timeline.
Fix a loss and a dataset , with empirical risk . Assumption 1 asks five things:
with friction , inverse temperature , and .
The algorithm SGHMC1, with step size , i.i.d. standard Gaussian and i.i.d. oracle draws , is
This is the Euler discretisation of underdamped Langevin dynamics, whose invariant law is the Gibbs law . Write for the law of . A drift constant satisfies . The constants of the paper's Table 1 (, , , , , , , , ) are explicit functions of these data. Here is the contraction rate of the continuous dynamics.
Let . Let the step size satisfy (3.3), , and let (3.4). Then, with the expectation over the sample and the algorithm's randomness,
The four terms bound, in order:
In attack order:
The result. Corollary 4 is a global-optimisation guarantee for a non-convex stochastic program with every constant explicit, so a target accuracy translates into a step size and an iteration count. Compared with the analogous SGLD bounds, the dependence on the contraction rate of the underdamped dynamics replaces the spectral gap of the overdamped one; §5 of the paper shows landscapes on which this improves the iteration complexity. The bound also separates the four sources of error (initialisation, discretisation, concentration, generalisation), so each can be sharpened independently.
Formalizing it. All results are proved on paper; none has a machine-checked proof. A formal development would supply:
The obvious route is to compare the discrete chain directly with its invariant law. That fails, because SGHMC1 does not leave invariant, and the bias must be controlled through the continuous-time diffusion. The proof of Theorem 2 needs three ingredients:
Mathlib has no stochastic integral or SDE solution theory, so none of these continuous-time statements is formalized as an item here. A solver proving Theorem 2 must either build that theory or find a discrete-time argument. Lemma 27 needs a logarithmic Sobolev inequality for derived from a Poincaré inequality and a Lyapunov condition.
is EuclideanSpace ℝ (Fin d). Laws on the phase space live on , and every Euclidean phase-space norm is written ; Lemma 26 is stated on WithLp 2 (ℝ^d × ℝ^d).
The oracle is with a dataset-independent law of the draws . The iterates are random variables on a probability space carrying , Gaussian and draws , all mutually independent. and are jointly measurable. The goal's expectation is a lower Lebesgue integral of over and the probability space. The Gibbs law is an explicit density against Lebesgue measure.
The following conventions are explicit hypotheses or definitions:
The goal is not a statement about a chosen , an existence claim or a junk value. Its left side cannot collapse to zero, and every hypothesis set is satisfiable, for instance by with an exact oracle and .
The underdamped Langevin SDE, Lemmas 16(i), 17, 18 and Theorem 19 are not items. Neither are the SGHMC2 results (Theorems 6, 9, Corollaries 7, 8), Corollary 3 and §5–6. Contributions toward Gibbs-measure moment bounds, couplings on and the Lyapunov recursion are reusable beyond this mission.
Many service providers are paid under a contract that makes them responsible for a customer's costly failures over a fixed window: a hospital penalized for heart-failure readmissions within 30 days, or a maintenance contractor responsible for engine replacements. A preventative appointment lowers the chance of such a failure, and the sooner it takes place the fewer customers fail while waiting. Capacity for appointments is limited. A clinic plans a fixed number of base slots per period at no incremental cost, and can add a limited number of surge slots (overtime, external staff) at a cost per slot. The scheduler therefore trades the cost of surge capacity against the discounted cost of failures caused by delay.
B. Grant, I. Gurvich, R. K. Mutharasan and J. A. Van Mieghem (SSRN 3092667; Manufacturing & Service Operations Management, 2021, doi:10.1287/msom.2020.0932) model this trade-off as an infinite-horizon discounted dynamic program, motivated by follow-up appointments for heart-failure patients at Northwestern Memorial Hospital. Their first optimality result, Proposition 1, identifies when the simplest policy, booking every request in the earliest period with a free slot, is optimal.
Time is divided into periods. The appointment book at the start of a period is , where is the number of appointments already booked periods ahead and is the booking horizon. Each period has slots: base slots and surge slots. A valid book has for every and .
At the start of each period new requests arrive, i.i.d. across periods with law supported on . The scheduler books them: an action is admissible (1) if (no same-period booking), for , and . If the requests do not fit, every free slot is filled and the remaining overflow requests are sent elsewhere at cost each.
Between periods each booked customer independently fails with probability , at cost , and leaves the book; the others move one period closer, so the next book is a product of binomial thinnings of with survival probability (4). A customer who reaches the appointment shows with probability and afterwards fails within the contract window with probability ; a no-show (probability ) fails with probability . Serving appointments costs (5). The expected one-period cost (7) is
and a policy is valued by its expected total discounted cost (9), with discount factor .
The First-Available (FA) policy books the requests into periods in order, filling every free slot of a period (base, then surge) before using the next.
If
then FA is optimal: for every admissible policy and every valid book .
Proposition 1 gives a closed-form, state-independent and arrival-independent sufficient condition under which the scheduler needs no optimization at all: book every request as early as possible, using surge capacity whenever base capacity is full. The paper's numerical study finds FA optimal in a large fraction of realistic scenarios, so the condition marks out a regime in which a hospital can use the simplest rule without loss. Together with Propositions 2 and 3 of the paper (base-first and base-first/last-surge policies) it maps out which simple policy to use as the surge cost varies.
The paper's argument for Proposition 1 compares the expected discounted cost of one customer booked at delay with surge against the same customer at delay without surge, and concludes optimality from the comparison. That step is an incremental-cost heuristic: the passage from the four inequalities (17)–(20) to optimality of FA in the dynamic program is asserted in one sentence, not proved. Milestones 4 and 5 formalize the algebra the paper does carry out; the bridge from (17)–(20) to optimality of the policy is the open part of this mission. As far as is known, no machine-checked proof of this result or of any optimality result for appointment scheduling with surge capacity exists.
The obvious argument is the paper's: each request is cheaper earlier, so book it earlier. In the dynamic program the requests interact. A customer booked early occupies a slot that a later arrival could have used; failures free slots again; surge cost is charged on the realized number of customers present at the appointment, after failures; and overflow depends on how full the book was left by earlier decisions. A single-customer comparison does not account for any of these, and the per-customer cost of FA (12) need not even be monotone in the delay for every parameter choice. Any argument has to account for the whole state of the book, not one customer at a time.
All objects live in the namespace SurgeAppt.FirstAvail. Costs and probabilities are real numbers and counts are natural numbers. A book is a function , indexed as on the page; the transition reads into and sets . The cost (7) is computed with the surge cost (5) and the expected failure term written as a finite sum over next books. A policy is a sequence of decision rules (Markov deterministic, possibly non-stationary); it is admissible if each decision at a valid book with satisfies (1), including the forced action when (1) is empty. The value (9) is the series over the law of the book at time ; it is never defined as a fixed point. Condition (13)'s minimum is read as "for every pair ", which is vacuous when .
Hypotheses added to the page and disclosed in every statement: , , , , and ; the page's , and with are kept. History-dependent and randomized policies are not modelled; the paper's remark after (11) that a stationary optimal policy exists licenses comparing FA against Markov policies.
The goal is not trivialized: the competitors are every admissible Markov policy, not only first-available-like ones; the admissibility of FA is part of the conclusion, so a rule that skipped bookings could not qualify; and the value is a convergent series of bounded nonnegative costs, not a junk value.
A complete development needs: finite discounted MDP facts (milestones 2 and 3, reusable for any finite-state model with constrained actions), properties of the product-binomial kernel, and a comparison argument for the goal. Proofs of any milestone, alternative arguments for the goal, and counterexample searches that probe the boundary of (13) are welcome.
On-demand service platforms (home cleaning, tutoring, handyman and care services) match customers with independent providers and keep a commission on every transaction. Once a customer and a provider have met through the platform, both can save the commission by transacting directly the next time. This platform leakage (also called disintermediation) is a central operational concern for such platforms: it erodes revenue and can make the platform unviable. Platforms counter it with lower commissions, perks such as insurance and payment protection, and enforcement.
He, Savin, Goh and Teo (SSRN 3550646; published in Manufacturing & Service Operations Management, doi:10.1287/msom.2022.1179) build a queueing-game model of this trade-off. The platform sets the share of each fee it pays out, providers choose whether to work on the platform, off it, or not at all, and customers choose where to queue. The paper's main result for perfect information, Proposition 3, gives the exact range of the customers' counterparty risk (the extra cost of transacting off-platform) in which leakage occurs at the platform's optimum. This mission formalizes that result and the chain of results its proof rests on.
There are two provider types , with providers of type . Customers value type- service at , every provider serves at rate , and customers pay per unit of waiting time. With the squared coefficient of variation of service times, put . Aggregate demand arrives at rate with (supply-constrained service, (1)).
Customers. An on-platform queue of providers at fee with demand rate has expected wait ; a single off-platform provider has . Off-platform customers bear an extra cost . Customers join each queue until their net utility equals that of the outside option, which determines the equilibrium demand rates and .
Providers. A provider of type has opportunity cost rate , with . Off the platform he sets a fee maximizing , earning utility . On the platform, when type- providers share a symmetric fee , each keeps the share of the fee and earns . A provider participation equilibrium (Definition 1) is a pair of head counts on and off the platform from which no provider wants to switch among on-platform, off-platform and outside options. When several equilibria exist, providers settle on the one with the most providers on the platform.
Platform. Anticipating these responses, the platform chooses payout ratios to maximize its profit rate
absorbing the counterparty risk on every on-platform transaction.
The paper's closed forms are and , and the non-platform opportunity cost is .
With
the platform's problem has an optimum, and at every optimal payout pair and in the selected participation equilibrium,
At the paper's own optimal payout ratio the equivalence (25) holds whenever .
The result separates the two forces behind leakage. Below , counterparty risk is cheap enough that the platform finds it profitable to pay providers enough to stay. Above , off-platform service is so unattractive to customers that providers prefer their outside option. Leakage is confined to the interval between, so a platform can read off whether perks that lower , or changes in pool size , push a provider type into or out of the leakage regime. The interval shrinks as grows, which is the paper's case that larger provider pools protect platforms.
The result is proved in the paper, by hand. No machine-checked version exists. The mission produces a formal model of a queue-based Stackelberg platform game: customer queue-joining equilibria, symmetric fee equilibria among providers, participation equilibria with a selection rule, and an optimizing leader. This structure recurs throughout the platform-operations literature (Taylor 2018 and its successors) and is reusable for related models.
Each step is elementary in isolation; the work is in the chain. The platform's objective depends on through the selected participation equilibrium, which is discontinuous in : it jumps from to providers at . Optimality must therefore be argued over a piecewise objective, not by first-order conditions. The natural first idea, evaluating everything at the closed-form , proves only the third clause of the goal. The goal also quantifies over every optimum, including ties at , where the platform is indifferent between keeping and losing a type. The final equivalences then require nontrivial manipulation of nested radicals in (A9)(ii).
Everything lives in the namespace PlatformLeakage.Perfect, in one definition file and eight theorem files. Parameters are a structure Params, with real values and natural-number head counts; the provider types are an inductive PType with constructors h, l. Every statement assumes Params.Std: , , , , , , and (1). Positive parts are max x 0, and square roots are Real.sqrt, with every radicand nonnegative under Std.
Committed conventions:
Classical.epsilon).A formalization that states the goal only at of (23), or that defines utilities by , would be trivial and is ruled out. Proofs of any milestone, and reusable lemmas on nested radicals or on piecewise-monotone optimization, are welcome.
A majority attack lets a miner create blocks on a private branch of a permissionless blockchain and later publish that branch as the accepted transaction history. The familiar motive is a private benefit from changing the record, such as a double-spend. Gans and Halaburda show that this motive need not be present: when transactions compete for limited block space, a slower private branch can collect more fees per block. The extra mining revenue can outweigh the attacker's cost even when the private benefit is zero. Their analysis therefore makes the fee market part of the security calculation, alongside the hash power needed to overtake the public branch. This mission formalizes the Proof of Work result in Proposition 1 of the pinned preprint, pp. 13–14.
The result matters for miners deciding whether to continue honestly on the incumbent chain and for designers assessing what a given distribution of mining power actually guarantees. An active miner need not already control half of the incumbent hash power to face a profitable attack opportunity. That is the specific vulnerability established here; the model does not claim that every miner attacks or that every attack succeeds under every network rule.
Let be miner 's hash power before an attack and the incumbent total. If the intended time between blocks is , the puzzle difficulty is . A miner deploying hash power earns an expected blocks per unit of clock time. With per-block reward and mining cost per unit time, its flow profit is
For an honest block, : is the value of newly issued tokens and the expected transaction fees. A miner is active when its incumbent flow profit is nonnegative, the participation condition (1) on p. 5. The attacking branch pays per block. The token reward is the same on both branches, as §4.3 states; their expected fees can differ.
If a miner held before attacking, the paper's minimum attack-power bound is (p. 6). Let be an attained maximizer of attack-chain flow profit over nonnegative hash powers. Equation (3), p. 8, evaluates the attack at and defines its net cost over expected duration :
A miner with private attack benefit prefers not to attack only if . A no-attack equilibrium, for this mission, means that every active miner satisfies this incentive condition. These definitions follow the paper's benchmark, attack description and incentive condition in §§2–4, pp. 4–8.
In the fee model, every available transaction has unit size and a nonnegative fee. A block takes the highest fees among its available transactions. Write for the expected block fee when independent fees have a common law . For congested honest blocks and a slower attack branch, the first central target is Lemma 2, pp. 12–13:
The paper expresses congestion as , with the mean transaction arrival rate, and obtains more arrivals between attack-chain blocks when attack hash power is below . The natural counts state that comparison directly. The same law on both branches represents users leaving their fee submissions unchanged.
The economic target is Lemma 1, p. 11. When the attack-chain reward per block is greater, there is a threshold strictly below half of above which the net attack cost is negative:
The goal, Proposition 1, pp. 13–14, combines these claims. For the finite miner population, there is such that any active miner with violates the no-attack incentive condition even at . The threshold is chosen before the incumbent allocation varies. Thus it applies to genuinely sub-majority values of , including an interval below .
Strictly higher fees on the private branch make its reward per block greater even though the issued-token reward remains . Lemma 1 then identifies incumbent miners whose forgone honest profit is less than their expected attack profit. Proposition 1 states the resulting failure of the no-attack equilibrium condition. This gives a precise economic implication of congestion in the model: hash-power shares alone do not determine whether an active miner has an incentive to preserve the public chain.
The paper proves these claims informally, while the proposed Lean theorems remain open proof targets. The development contributes reusable objects beyond the final proposition: a top- sum for finite fee samples, its expectation under a product probability law, and a separate mining-profit and attack-cost model. Formal proofs would make the assumptions behind strict fee improvement and a sub-majority threshold explicit. They would also resolve the paper's informal assertions about the attack cost curve without changing its stated target.
Adding candidate transactions can never reduce the top- fee sum, but that only gives a non-strict comparison. Strictness requires a positive probability that a new transaction displaces one selected by the honest block. The common fee law must therefore have more than one possible value, the block capacity must be positive, and the expectation must be finite. These conditions are easy to overlook when replacing the paper's order-statistics prose with a real-valued integral.
The threshold statement has a different difficulty. The paper describes a break-even hash-power level and treats its behavior as evident, but the needed existence and ordering are not established in the text. A faithful formal statement must retain the existential threshold below for an entire range of incumbent powers. It cannot choose a threshold after seeing one fixed allocation, since that would lose the proposition's sub-majority content.
Hash powers, rewards, costs, time and net cost are real numbers; hash powers used by miners are nonnegative. The miner population is finite, and the goal requires . The puzzle difficulty is always with , so no division by zero is used. Attack duration is positive. The attack fee and honest fee come from the same fee law with natural arrival counts ; the goal does not assume their ordering.
The paper says mining cost is nondecreasing and weakly quasi-convex on nonnegative power. Here cost is additionally convex there, which supports the single-peaked attack-profit model used in equation (3) and Figure 1. The attack-chain maximizer is required to be attained; some otherwise admissible costs yield no finite maximizer. The fee law is a nonnegative probability distribution with a finite first moment and is not a point mass. These additions are disclosed in the theorem descriptions and are needed for the paper's strict claims. Independent fees are represented by a product measure, and block fees by a maximum over sets of at most indices; with nonnegative fees and , this is the sum of the highest fees. This representation is continuous and integrable under the stated law, so the real integral does not receive Lean's default value for a non-integrable integrand.
The paper uses as a lower bound even though it says a successful attack must exceed it. The net-cost definition follows equation (3) literally at the maximum of that bound and the unconstrained optimizer. The target concerns the paper's incentive inequality in this stated model. Contributions to the fee-order-statistic infrastructure, continuity and integrability, attack-cost comparisons, and the two numbered lemmas are all useful to this mission.
Firms facing a new technology rarely decide in the dark: they run pilots, prototypes and market tests before committing. The management literature on disruptive technologies (Christensen, The Innovator's Dilemma, 1997) argues that incumbents fail because they evaluate new opportunities with tests tuned to their existing business, and that entrants succeed because they test differently. Gans's paper (NBER Working Paper 29091, published as Experimental Choice and Disruptive Technologies, Management Science 2023, doi:10.1287/mnsc.2022.4496) turns this into a decision-theoretic question: when a firm may choose which experiment to run, and experiments differ in how they trade false positives against false negatives, which one does it choose?
The first result of the paper, Proposition 1, is the building block for everything after it (incumbent versus entrant choices, competition, cooperation). It says that the optimal experiment is biased toward the firm's own predisposition, echoing the result of Che and Mierendorff (Optimal Dynamic Allocation of Attention, American Economic Review, 2019) that information seekers choose news sources that reflect their own bias.
A firm decides whether to exploit a new technology. The state of the world is (the technology works) or (it does not). Exploiting earns in state and in state ; not exploiting, the status quo, earns . The payoffs satisfy . The firm's prior probability of is , with .
Without information the firm exploits when , that is, when , where the no-information threshold is
An experiment yields a signal or , with and (Table 1 of the paper; is the sensitivity and the specificity). Experiments are costless; the firm runs exactly one, chosen from the experiment set
Put . The w-biased experiment is : a working technology always produces , so the signal is conclusive bad news. The n-biased experiment is : the signal is conclusive good news.
After observing the signal, the firm decides whether to exploit. A decision rule assigns an action to each signal; there are four. The value of an experiment is the expected payoff under the best of the four rules. An experiment is optimal if it lies in and no experiment in has a larger value.
The paper states Proposition 1 as "the firm optimally chooses the w-biased experiment" if and the n-biased one if , and adds that, "for all but a degenerate case, these are the only two experiments that will be optimally chosen". The goal records both: the biased experiment is optimal over , and it is the unique optimum. The degenerate case is excluded, as in the paper.
The result. Proposition 1 says that a firm predisposed to exploit designs its test so that only a conclusive "no" can change its mind, and a firm predisposed not to exploit designs it so that only a conclusive "yes" can. The rest of the paper applies it with firm-specific payoffs: an incumbent, whose status quo is valuable, has a higher threshold than an entrant (Proposition 2), and this difference drives the paper's account of why incumbents and entrants experiment differently with disruptive technologies (Propositions 3–5). Without Proposition 1 none of these comparisons is defined.
Formalizing it. The result is proved in the paper (§7.1, p. 31), but the proof covers only the comparison between the two biased experiments; the claim that no other experiment is optimal is argued graphically from Figure 1, and the proof leaves the case to "the same way". The mission produces a machine-checked proof of the full statement over , with uniqueness. To our knowledge no part of it has been formalized before.
The obvious argument compares along the frontier of with the slope of the indifference curves. That argument fixes the decision rule "exploit iff ", while the firm's value is the best of four rules: for priors far above the firm exploits after both signals of , and the comparison then changes form (the two cases of the proof on p. 31). A proof over must handle the maximum of four piecewise-linear functions of and show that it is uniquely maximised at one vertex. The printed slope expression on p. 13 also has its axes interchanged relative to Figure 1, so it cannot be transcribed as it stands.
All quantities are real numbers. States and signals are Bool; a decision rule is a function Bool → Bool; the value of an experiment is Finset.sup' of the expected payoff over the four rules, so the firm's post-signal choice is optimal by construction. Joint probabilities are prior times Table 1 entry; posteriors use real division and are stated only for signals of positive probability. Two hypotheses are added to the paper's and recorded in the definitions: (at the biased experiments tie) and (otherwise is empty and ). Optimality is maximisation over , and experiments are equal when both precisions are equal.
Defining the value as the payoff of the single rule "exploit iff " (the display ) would trivialize the goal into milestone 6 and is ruled out: the value is always the best rule. Comparing only and is milestone 5, not the goal.
The development needs only finite sums and elementary real inequalities; no probability library is required. Contributions of proofs of any milestone, and of alternative proofs of the goal, are welcome.
Impulse control models a decision maker who acts on a system by discrete interventions rather than continuously: a central bank adjusting a rate, a firm switching production capacity, a portfolio manager rebalancing with fixed transaction costs. Each intervention has a fixed cost, so the controller chooses both when to act and how much. In many applications an order is not executed the moment it is given: there is an execution delay between the decision and its effect, during which the controller cannot revise it.
Djehiche, Hamadène, Hdhiri and Zaatra (arXiv:1904.11924v2, published in Mathematics of Operations Research, 2022) study the infinite-horizon version of this problem with random coefficients: the state process and the reward are only assumed progressively measurable with respect to a Brownian filtration, not Markovian. Without a Markov structure the usual route through quasi-variational inequalities is unavailable, and the authors work instead with optimal stopping and (reflected) backward stochastic differential equations.
Execution delay in impulse control goes back to Robin (1976) for diffusions. It was treated for inventory problems with delivery lags by Bar-Ilan and Sulem (1995), for delayed reaction by Øksendal and Sulem (2008), and on a finite horizon by Bruder and Pham (2009), all in Markovian settings. Non-Markovian impulse control without delay was studied by Djehiche, Hamadène and Hdhiri (2010), and with execution delay by Hdhiri and Karouf (2018). The paper under formalization treats delay, random coefficients and an infinite horizon together; its stated main issue is the continuity of the value process.
Let carry a standard -dimensional Brownian motion , and let be its natural filtration augmented by the -null sets. The data are:
A strategy is a sequence of stopping times and -measurable -valued impulses. It is admissible, , if almost surely. The impulse decided at takes effect at :
The value is built by an iterated optimal stopping scheme. For an index , a stopping time and a finitely-valued -measurable , set , and for define the obstacle
and the Snell envelope
The sequence increases to a limit , with obstacle given by the same formula with in place of .
Define , , and let be an -measurable -valued maximiser in the obstacle. Then is optimal:
The formal goal asserts that the scheme and its obstacle exist, that a strategy satisfying the recursion exists, and that every such is admissible, attains , and dominates every admissible strategy.
In the order the proof uses them: Proposition 4.1 (the scheme is well-posed, , ); Remark 4.2 (gluing over the values of ); Proposition 4.2 i) (monotone convergence, càdlàg limit, the Snell identity for ) and ii) (independence of the starting time after ); the measurable maximiser of the proof of Proposition 5.3; the bound (6.27) on ; Proposition 6.4 (continuity of ); the full optimal-stopping identity at the first hitting time, Appendix (8.54), including the essential supremum after a random starting time; and the two halves of the proof of Theorem 6.1, and for every .
Theorem 6.1 reduces a control problem over sequences of stopping times and impulses, with delayed effect, to a countable family of single optimal stopping problems, and identifies an optimal strategy explicitly from the value process. It gives existence of an optimal strategy in a non-Markovian infinite-horizon setting where no verification theorem for a quasi-variational inequality is available.
The result is proved on paper. As far as is known it has no machine-checked proof. Formalizing it would add a continuous-time optimal stopping layer (Snell envelopes with values at , first hitting times after random times) that the current libraries lack, and a precise record of the conventions the paper leaves implicit: values at , versions of optional projections, and the index shift between Sections 3 and 6.
The obvious argument is a dynamic programming verification: show the value satisfies a fixed-point equation, then check the candidate strategy attains it. Here the candidate strategy stops at the first time meets its obstacle , and that time is optimal only if the Snell envelope is continuous. The limit of increasing continuous supermartingales is only càdlàg, and the obstacle involves at the shifted time , so a jump of propagates to a jump of and back. Ruling out these jumps (Proposition 6.4) is the main technical step of the paper; it uses that the Brownian filtration is quasi-left continuous, and fails for general filtrations. The remainder needs a continuous-time Snell envelope theory over stopping times that may be infinite, which Mathlib does not provide.
Fin l → ℝ; is a nonempty Finset. Time is ℝ≥0; stopping times take values in WithTop ℝ≥0. The filtration is the published ReflectedBSDE.Existence.augmentedFiltration of a standard Brownian motion (Peng1990.SMP.IsStdBrownian). It is never an arbitrary filtration. The essential supremum is the published ReflectedBSDE.Existence.IsEssSupOver.The bibliographic data are those of the paper's reference list (arXiv:1904.11924v2, pp. 28–29).
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.
Network interdiction asks how an inspector should randomize over sets of links when a router can choose a path through a network. Link inspection probabilities and path interception probabilities describe different features of the same random choice. Specifying both sets of numbers separately does not guarantee that one distribution over inspection sets realizes them. The poset model of Dahan, Amin and Jaillet isolates this compatibility question: links become elements of a partially ordered set, and relevant paths become maximal chains. Their feasibility theorem supplies the distributions required in the equilibrium analysis of their interdiction game. This mission formalizes that theorem and its stated structural results, from the pinned preprint arXiv:1811.08516v3.
The question also stands on its own as a finite probability problem. A vector of element marginals fixes the chance of selecting each element, while a lower bound for every maximal chain fixes the chance of selecting at least one element from that chain. The two requirements interact because chains can overlap and share several splice points. Conditions that look sufficient one chain at a time can fail to support a single distribution across all chains. The paper's Example 2 on p. 9 demonstrates infeasibility when its conservation condition is absent. Dahan, Amin and Jaillet prove that the two stated conditions together are sufficient for every finite nonempty poset.
A finite poset is a finite set with a reflexive, antisymmetric and transitive order. A chain is a subset whose points are pairwise comparable; a chain is maximal when it cannot be enlarged while remaining a chain. Write for the family of maximal chains. For each , prescribe an element marginal . For each , prescribe a chain hitting target . A distribution gives a nonnegative weight to every subset , including the empty set, with total weight one. Its marginal at is the total weight of subsets containing ; its hitting probability for is the total weight of subsets meeting .
Two parameter conditions are central. Condition (2) says for every maximal chain. To state condition (3), take maximal chains and a common point . Splice them at : follows through and then above it; takes the opposite halves. The conservation law is for every such pair and every common point. The paper's §2.2 specifies these conditions and the distribution problem (D) on pp. 7–8.
The auxiliary program (Q) keeps the element marginal equalities but omits total weight one. It minimizes total assigned weight while limiting how much weight may be assigned to subsets that meet a maximal chain more than once. Its slack is , and its optimum is . The factor in its chain constraint is the real number when .
The goal is the paper's Theorem 1, p. 8: under conditions (2) and (3), some distribution satisfies all marginals and chain hitting bounds simultaneously:
Theorem 2, p. 11, is the strongest quantitative milestone. With the same standing setting, it identifies the least feasible total weight in (Q):
The intervening milestones are the paper's Lemmas 1–3 and Propositions 1–4. Lemma 2 establishes the poset generated by a splice-closed family of chains. Proposition 1 relates (D) to the bound . Propositions 2–4 state the properties, termination, feasibility and total weight of the paper's Algorithm 1.
Theorem 1 is an existence guarantee for a joint distribution, not merely separate bounds that can be met one chain at a time. It lets a model specify desired inspection marginals and path interception lower bounds while retaining a genuine probability distribution over inspection sets. In the paper, this supplies the interdiction strategies used in the network game's equilibrium characterization in §5. Theorem 2 gives the exact amount of unnormalized weight needed to meet the same constraints, which also identifies when normalization to a probability distribution is possible.
The results are already proved in the cited paper. The work here is to state their hypotheses, objects, algorithm and conclusions in Lean and then construct machine-checked proofs. The reusable output is a finite-poset interface for maximal-chain splicing, chain-generated subposets, distributions on subsets, and the auxiliary optimization problem. The game equilibrium theorem of §5 is outside this mission; a formal development of it could import the distribution theorem after it is proved.
Matching each element marginal separately does not control the probability of hitting every chain at once. If a selected subset meets a chain at two or more elements, the sum of its element marginals counts that subset more than once, while the chain hitting event counts it once. Hence condition (2), although necessary, does not alone capture all compatibility constraints. The conservation law couples overlapping maximal chains at every common splice point, and the auxiliary program records the excess count . In Algorithm 1, a chain can be removed from the active family while its constraint must remain satisfied; the paper's Lemma 3 addresses precisely that issue. Sections 2–3 of the preprint give the detailed statements.
The ground set is a nonempty finite Lean type with a partial order. Subsets and maximal chains are Finsets, and a distribution is a real-valued function on all finite subsets. The values of are stored as a function on finite subsets for convenient splicing, but all bounds and conservation equations use only maximal chains. The splice uses the first chain at and below the common point and the second at and above it. The conservation equation quantifies over every common point. This rules out a vacuous or weaker encoding that checks only one splice, drops the empty subset, or replaces probability normalization by an inequality.
The optimal value is the real infimum of feasible (Q) objective values. Under the standing assumptions it is a proper finite optimum; the statements using it retain those assumptions. The maximum in Theorem 2 ranges over all elements and maximal chains of the nonempty poset. Cardinalities in (Q) are converted to reals before subtracting one. The algorithm's Lean state zero is paper iteration one, and its output accumulates weights assigned to a subset if that subset appears in more than one iteration. This additive interpretation of step A7 is disclosed because the printed assignment does not say what happens on repetition.
The development needs Mathlib's finite posets, chains, finite sets and real-number sums, together with the paper-specific chain relation and algorithm state. Contributions proving the numbered milestones, establishing the algorithm's invariants, or providing reusable facts about chain splicing and finite distributions all advance the goal. The affine special case of §4 and the game theory of §5 are separate work.
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.
Training a neural network means minimizing a non-convex loss over its weights. Local search methods can only certify local optimality, so a recurring question in the theory of neural network optimization is whether every local minimum of the training loss is a global minimum. A local minimum that is not global is called a sub-optimal (or bad) local minimum.
A line of positive results suggested that sufficiently wide networks have no bad local minima. Yu and Chen (IEEE Trans. Neural Networks 6(5), 1995, Theorem 3) stated that for one-hidden-layer sigmoid networks with at least as many hidden neurons as training samples, every local minimum is global; the survey of Bianchini and Gori (Neurocomputing, 1996) lists this as a main result of the area. Later work proved weaker landscape properties for deep over-parameterized networks, such as the absence of sub-optimal valleys or basins (Nguyen, Mukkamala and Hein, arXiv:1809.10749; Nguyen, arXiv:1901.07417), and Nguyen, Mukkamala and Hein conjectured that "no bad local minima" holds under mild conditions.
Timeline of related results, as attributed in the source paper:
A fully connected network with hidden layers has widths , input width and output width . Its parameters are
Given an activation and a data matrix whose columns are the samples, the post-activations are and
and the network output is , with no output bias. For targets , the empirical loss is
Two assumptions are made.
For every satisfying Assumption 1 with , every satisfying Assumption 2, any depth and any widths with , there is an output matrix such that
The data and the activation are given; only is chosen. The widths other than are unrestricted, so the statement covers arbitrarily wide and deep networks.
The theorem is a counter-example: for generic data and almost every smooth activation, increasing width or depth does not by itself remove bad local minima of the squared loss. It refutes Theorem 3 of Yu and Chen (1995) (Corollary 2 of the paper) and the conjecture of Nguyen, Mukkamala and Hein for this setting. Positive landscape results therefore need further assumptions on the data, the targets or the architecture, and the construction indicates which assumptions cannot be dropped.
The result is proved in the paper; no machine-checked proof of it is known. A formalization would verify a full counter-example for arbitrary depth, which involves a layer-by-layer second-order expansion whose bookkeeping across layers is where informal arguments of this type are most error-prone. It also provides a reusable Lean model of a deep fully connected network with biases and an arbitrary activation, which other landscape results can build on.
The output of the constructed configuration does not depend on the input, so a perturbation of changes in ways that need not be first-order: the obvious approach of checking a vanishing gradient and a positive semidefinite Hessian is inconclusive, because the loss is flat along several directions at the constructed point (for instance, changes of that keep its row sums), and the decisive effect of perturbing appears only at second order in the hidden layers. Local minimality must be shown for all nearby configurations at once, by controlling the second-order term of every layer uniformly in a neighbourhood and propagating the sign through the layers. The correlation condition must hold for every row of and every neuron simultaneously.
Fin a → Fin b → ℝ; indices of neurons and samples are 0-based. The parameter space is the full product of all weights and all hidden biases , with its usual sup-norm metric; local minimality is Mathlib's IsLocalMin. The forward pass is defined by recursion over the layers, feeding the post-activation of layer to layer (the printed eq. (2b) writes the pre-activation, a slip).Contributions welcome: proofs of the milestones, in particular a Lean development of the layer-wise Taylor expansion behind Lemma 2.
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.
A seller choosing between a first-price auction (FPA) and a second-price auction (SPA) needs to know whether the payment rule changes expected revenue. In the classical independent private-value benchmark, the two formats can be revenue equivalent. Balzer and Rosato examine a different setting: a bidder’s value depends on other bidders’ private signals, and the bidder dislikes outcomes that fall below a reference lottery formed from the bid she chooses. Their result gives a precise revenue ranking under these preferences. The paper was published online in Management Science in 2020 in its Articles in Advance pagination Balzer and Rosato.
The question matters because a payment rule changes both what a winner pays and which monetary outcomes she anticipates. In an FPA the winner pays her own bid. In an SPA she pays the highest opposing bid, so her payment varies with competitors’ signals even when she wins. Balzer and Rosato distinguish the risk of winning versus losing, which they call extensive risk, from variation in value or payment among winning outcomes, which they call intensive risk. Their analysis asks how these risks affect bidding and the seller’s expected receipts Balzer and Rosato, §§3–4.
There are bidders. Each observes a signal drawn independently from a continuously differentiable distribution on , where and the density is strictly positive. Bidder values the item at . The value is nonnegative, increasing in every signal, strictly increasing in the bidder’s own signal, twice continuously differentiable, and symmetric in opponents’ signals. The distribution of the highest of the opposing signals has cumulative distribution and density Balzer and Rosato, §2.1 and §3.1.
A realized outcome is a value-payment pair . Its comparison point is another such pair . Gain–loss utility is for and for , with denoting the item and money dimensions. Here , , and . Total utility is
For outcome lottery and reference lottery , expected utility averages this expression over an independent draw from each lottery. Under a choice-acclimating personal equilibrium (CPE), a type assesses each possible nonnegative bid against the lottery that the same bid induces. A symmetric increasing strategy is a CPE when bidding maximizes this self-referenced expected utility for every type. The paper maintains Assumption 1, , through its CPE results Balzer and Rosato, Definition 1 and Assumption 1.
The main target is Corollary 1. For any symmetric CPE strategies and in the FPA and SPA, respectively, let and be the expectation of the sum of all bidders’ payments. Then
The milestone list follows the paper’s CPE results: the direct-utility representations (10) and (12), existence and bid formulas for every symmetric equilibrium in Propositions 7 and 9, the common equilibrium-utility identity in the proof of Proposition 11, and Proposition 11’s comparison of utilities and payments. These targets retain the distinction between a lottery-based preference definition and the formulas derived from it Balzer and Rosato, pp. 10–11 and Appendix.
The corollary tells the seller which format yields more expected revenue within this model. When bidders have no loss aversion over money, the two formats yield the same revenue even though values are interdependent. With positive monetary loss aversion, the FPA yields strictly more. Proposition 11 gives the bidder-level comparison behind this statement: equilibrium utility is the same in both formats, while each type above the lowest pays more in expectation in the FPA when Balzer and Rosato, Proposition 11 and Corollary 1.
The result is proved in the paper but is not yet machine-checked in this mission. A completed formalization would connect the primitive gain–loss utility, lottery construction, CPE incentive condition, interim payment comparison, and ex ante revenue ranking. The auction data module can also support other results about independent signals and interdependent values; the loss-aversion module records the additional preference and equilibrium structure.
The expected utility of a bid changes when the bid changes because the reference lottery changes with it. Treating the comparison point as fixed would describe a different equilibrium concept. An SPA also exposes winners to variation in the payment itself, which is absent from the FPA. Thus the two formats cannot be compared merely by inserting the same bid into different payment formulas. The paper’s two direct-utility displays and its payment comparison are separate substantive targets Balzer and Rosato, §4 and proof of Proposition 11.
Lean uses real-valued signals, values, bids, and payments, and exactly bidders, so an opponent always exists. The signal law is a density-weighted measure on ; opponent and all-bidder signals use product laws. Strategies are measurable, nonnegative, and strictly increasing on the signal support. The model requires measurable values so mapped lotteries are genuine measures. A bid wins only when it strictly exceeds every opposing bid; ties have probability zero under the stated atomless signal law and strict monotonicity. Values of strategies outside the support do not affect the lotteries.
Revenue is defined directly as the expectation of the sum of payments, rather than by the payment formulas that the results seek to establish. Likewise, CPE is the incentive inequality over every nonnegative bid, and expected utility is built from the primitive outcome and reference lotteries. The direct-utility formulas are theorem targets, not definitions. The conditional value is used only when , where ; the bid formulas (11) and (13) are stated on because their displayed denominators vanish at the lower endpoint for some bidder counts.
The paper writes the intensive-risk term with a conditional density of value, although that density need not exist for private values. Lean instead uses a double expectation over the winning-signal region. The paper’s printed prefactor in (10) is inconsistent with a reference lottery induced by the deviation; the formalization uses . This correction is recorded on both representation milestones. Contributions toward the measure identities, equilibrium existence, envelope identity, and bidder-level payment comparison are all within scope.
A cryptocurrency user can attach a fee to a transaction, and a miner can choose which waiting transactions enter the next block. When the most valuable waiting transactions compete for a limited number of places, the fee rule affects both the user's bid and the amount the user expects to pay. Basu, Easley, O'Hara and Sirer study a protocol that charges every included transaction the minimum included fee. This makes the fee visible from the block itself, but it also lets a bidder affect the price when that bidder supplies the lowest winning bid. Their Result 3 asks how much this incentive matters when many users are active. Basu et al., §4 and Result 3, pp. 13–16.
The result is a useful distinction for the design of a multi-unit fee auction. Truthful bidding can fail as an exact dominant strategy even while the maximum expected benefit from deviating becomes small in a large active market. The paper treats this as one part of a proposed fee mechanism; the claims about miner payments, fill penalties and longer-run blockchain behavior are separate from Result 3. Basu et al., §4, pp. 13–16.
A block has places for transactions. There are other active users besides the bidder being studied, with . Each user's value for inclusion in the current block and each allowed bid lie in . The others' truthful bids form a vector . Write for its th highest entry, counting repeated values. The rule places the highest bids in the block. A winning bidder pays the lowest of those bids. Basu et al., §3, pp. 10–11; §4, pp. 13–16.
For a bidder with value who bids , let be the current-block payoff: value less the charged fee when included, and zero otherwise. A bid strictly above wins; the bidder then pays . A bid equal to loses under the tie convention used here. The strategic gain is the best admissible payoff minus the payoff from bidding one's value,
The model draws active users' values independently from a common continuous density on , with throughout that interval. Thus the joint law of is the product law of draws. A bidder knows their own value and the number of active users, but does not observe the other users' values or bids before choosing their own bid. The expected strategic gain therefore fixes the bid before averaging over the others' values :
The goal is Result 3. Its first clause says that truthful bidding fails to be a dominant strategy: for every admissible number of other active users, there is a valid profile and an admissible deviation with higher current-block payoff. Its second clause concerns the expected strategic gain when the others bid truthfully:
The quantifier over makes the convergence uniform across the bidder's possible values. It follows the paper's claim for “any bidder” and the value-independent upper bound stated immediately before Result 3. Basu et al., Result 3, p. 16; proof, pp. 21–22.
The milestone list records the statements in the paper's proof: an explicit profitable deviation when ; no profitable bid below the lower threshold; the two possible prices for a winning slot; the pointwise bound ; the bound ; and the assertion that this expected spacing tends to zero as grows. These are intermediate targets, not replacements for the goal about strategic gain. Basu et al., proof of Result 3, pp. 21–22.
The theorem identifies what the mechanism does and does not guarantee for a user. It rules out an exact dominant-strategy interpretation of truthful bidding for the minimum included fee protocol, while bounding the incentive to depart from truthfulness in a sufficiently large active market. Without the first clause, a claim of truthfulness would be misleading; without the second, the protocol would lack the paper's quantitative reason to expect truthful behavior to be nearly optimal when participation is high. Basu et al., §4, p. 16.
The paper gives the mathematical result and an appendix argument. This mission asks for a machine-checked account of that result, including the auction payoff, the order statistics, and the probability statement; these claims are open Lean targets in the proposed mission, not already machine-checked results. The definitions of the finite order statistic and of gain from an admissible deviation can be reused in later multi-unit auction formalizations. The density and product-law interface may also support other bounded-support order-statistic results.
A pointwise payoff comparison is not by itself an asymptotic statement. The gain depends on the entire vector of other bids through two adjacent order statistics and on a supremum over all allowed bids. Turning its bound into a statement about expectations requires those random quantities to be measurable and integrable. The spacing between the st and th highest of draws then has to vanish in expectation for the stated class of densities. Merely showing that this spacing is nonnegative or at most gives no decay with . Basu et al., proof of Result 3, p. 22.
There is also a boundary issue in the auction itself: a bid tied at the last included position requires a specified outcome. The protocol states the payment for included users but does not prescribe a complete deterministic tie rule for this one-bidder analysis. The chosen strict inclusion threshold makes every payoff a total function, and the continuous value law makes ties irrelevant to the expected-gain limit.
Lean represents the other active users as Fin m → ℝ, their th highest value as a real supremum defining kthHighest, and their i.i.d. values as Measure.pi of a density law supported on . The density assumption includes , continuity on that interval, , and total integral one. The slots satisfy : has no and the fee rule becomes a first-price case. The index is the number of other active users; the convergence is conditional on that count, matching the model's statement that bidders know how many users are active. Basu et al., §3, p. 11; Result 3, p. 16.
Bids range over . The gain is computed from the protocol payoff by a supremum over that interval; it is not defined as the adjacent order-statistic spacing or as a closed expression for the optimum. The expected gain takes the supremum over bids of expected payoffs, not the expectation of the pointwise supremum, since a bidder cannot condition a bid on the others' bids. The theorem explicitly requires integrability of the payoff of every admissible bid, so the real-valued integral cannot acquire meaning from Lean's default value for a non-integrable function. The first clause uses a concrete admissible bid profile; the second uses the product law of truthful others. The participation probability , the total potential user count , miner rewards, and the multi-block averaging parameter do not enter this conditional one-block claim. Basu et al., §3–§4, pp. 10–16.
The development needs finite order statistics, a measurable payoff and gain, probability laws from continuous densities, and integrability and convergence of adjacent order-statistic spacings. Contributions that establish those interfaces or prove the quoted intermediate claims serve the stated goal directly.
A Nash equilibrium of a two-player game is a pair of choices from which neither player can improve by changing their own choice alone. Computing one equilibrium is a central task in algorithmic game theory. For unrestricted bimatrix games, their payoff tables may encode difficult equilibrium computations. The structure of a rank-one bimatrix game gives a more specific question: can one equilibrium be found in time polynomial in the binary description of the game, even when equilibria are not isolated? Adsul, Garg, Mehta, Sohoni and von Stengel answer this with their BINSEARCH algorithm in Fast Algorithms for Rank-1 Bimatrix Games, Theorem 19. Their analysis explicitly includes degenerate games, which can have continua of equilibria (p. 5).
The paper develops a geometric account of rank reduction, parameterized linear programs, the connected set of equilibria of the auxiliary games, and the binary search procedure. The present mission targets the algorithmic result. The separately stated results on enumeration, exponentially many equilibria, and a structure theorem are outside this mission (Adsul et al., §§6–9).
An bimatrix game has payoff matrices . Player 1 chooses a row and player 2 chooses a column. A mixed strategy assigns nonnegative weights summing to one to a player's pure strategies. Write and for the two simplices. Against mixed strategies and , the payoffs are and . The pair is a Nash equilibrium when each strategy maximizes its owner's payoff against the other. These are the paper's definitions on pp. 4–5.
The games studied here have the form
The sum of the two payoff matrices is , so its rank is at most one. Zero vectors are allowed; the zero-sum case is included. A real parameter defines an auxiliary game . The set consists of triples for which is an equilibrium of that auxiliary game. The desired equilibria are the triples in that also satisfy (equations (10)–(12)).
For each , a primal linear program minimizes subject to , , and . Its dual maximizes subject to and . Their optimal solutions describe the auxiliary equilibria. The sets and identify the inequalities that can be slack or the coordinates that can be positive on the dual optimal face. They define a face of the parameterized primal polyhedron (equations (17)–(29)).
The goal is Theorem 19: for rational of combined binary length , and polynomial-time LP solvers returning extreme optimal solutions, Figure 2's BINSEARCH finds a Nash equilibrium of in polynomial time in . In the formal statement, a polynomial is chosen before the dimensions, game data, and admissible LP-selection oracle. It bounds the number of main-loop iterations, the bit length of every midpoint parameter passed to , and the bit length of every returned , including the parameter passed to the final :
for every optimal returned by the final dual LP, with the stated bound on each intermediate parameter. The ordered milestones cover best responses (Lemma 1), rank reduction (Lemma 6 and Theorem 7), primal-dual optimality (Lemma 9), preservation of the bracket (Lemma 17), the segment test (Lemma 18), and separation of distinct breakpoints (proof of Theorem 19).
The theorem gives an algorithm whose performance guarantee depends on the input's bit length, not on the number of equilibria. This matters for degenerate games: a continuum of equilibria does not by itself supply an algorithm to find one. The auxiliary LPs also connect game-theoretic best responses to ordinary finite-dimensional optimization. These claims and their precise scope are in §§4–5 of the paper.
The paper proves the theorem on paper. This mission asks for a machine-checked version of its formal statements and, ultimately, the proof. The definitions of best responses, primal and dual feasible sets, optimal faces, breakpoints, and a rational-input LP oracle are reusable in other formalizations of parametric games. The draft theorem declarations contain proof placeholders; they are targets rather than completed machine-checked proofs.
Ordinary bisection finds an interval containing an equilibrium parameter, but it can continue indefinitely when the equilibrium lies at a breakpoint: the two bounds can remain in neighboring segments. Repeated midpoints also create parameters whose bit descriptions grow with the number of iterations. Figure 2 therefore uses additional LPs that search the current optimal face and, in a strict branch, replace the answer by a breakpoint. A correctness proof must cover every permitted extreme optimal answer from these LPs, including degenerate faces, and must bound the separation of rational breakpoints (pp. 17–22).
Lean represents pure strategies by zero-based Fin m and Fin n, mixed strategies by real standard simplices, and payoffs by real matrices and vectors. The goal's input entries are rational and cast to reals for the LPs. It assumes : the paper leaves this implicit, while its minimum over the entries of and both mixed-strategy simplices require nonempty index sets. The game may be degenerate and may have rank zero.
LP optima are members of feasible sets whose objective is least or greatest on the full feasible objective image. An extreme LP solution also lies in the feasible set's extreme-point set. A selection oracle is constrained whenever an optimal extreme solution exists, and the goal asserts that every LP actually called during the run has such an answer. This excludes arbitrary values from an oracle at an infeasible or unbounded call. The initial bracket is the minimum and maximum entry of ; every branch and BR replacement follows Figure 2. The breakpoint endpoint symbols and are represented by absent optional finite endpoints in Lemma 18.
The running-time clause is an iteration bound together with a bound on the binary size of the midpoint and returned LP parameters; it does not formalize a machine model or the assumed polynomial-time LP solver. The goal is about the specified BINSEARCH run for every admissible selection oracle. Existence of some Nash equilibrium or termination for one hand-picked oracle would not express Theorem 19. Lemma 6 uses , the condition used in its printed proof; with a freely fixed , its printed implication (a) to (b) is false. A full development needs finite-dimensional LP duality, extreme-point and rational-vertex bounds, convex optimal-face geometry, and control of the run invariant. Contributions proving these components are welcome.
A bilevel program is an optimization problem in which one of the constraints is itself an optimization problem. An upper-level decision maker (a leader) chooses ; a lower-level decision maker (a follower) responds with an optimal solution of a problem parameterized by ; the leader's cost depends on both. Stackelberg games, toll setting on transportation networks, hyperparameter selection in machine learning, and many pricing and network design problems in operations research have this form. See Dempe, Foundations of Bilevel Programming (Kluwer, 2002), and Dempe and Zemkoho (eds.), Bilevel Optimization (Springer, 2020).
Necessary optimality conditions for bilevel programs are hard to obtain because the follower's optimality is not a standard constraint. The value function approach of Outrata (1990) replaces " is optimal for the lower level" by the single inequality , where is the optimal value of the lower level. This gives an equivalent single-level problem, but a well-known obstacle follows: Ye and Zhu (1995) showed that the standard nonsmooth constraint qualifications (nonsmooth MFCQ, equivalently NNAMCQ) fail at every feasible point of this reformulation. KKT-type conditions have therefore relied on calmness (Clarke 1983) or on partial calmness (Ye and Zhu 1995), both of which are strong.
Gfrerer (2013) introduced directional versions of regularity conditions, required only along one critical direction. Bai and Ye (arXiv:2004.01783, Mathematics of Operations Research 2022) carry this idea to the value function approach. They define calmness in a direction, prove a directional KKT condition for a general inequality-constrained problem under it, and apply this to the value-function reformulation of a bilevel program. This mission formalizes that chain, up to the paper's Theorem 5.1.
Let , and be continuously differentiable. For each , is the solution set of the lower level program : subject to . The bilevel program is
The value function is , and the value-function reformulation is
All norms are Euclidean, and is the open unit ball. For a direction and , the directional neighbourhood is
It is a cone of half-angle governed by around the ray through , cut at radius ; for it is the whole ball .
(VP) is calm at in direction if there are such that for every perturbation of the right-hand sides and every that satisfies the perturbed constraints. The same definition (Definition 3.1) applies to a general problem (P): s.t. .
A map is directionally Lipschitz at in direction if it is Lipschitz on for some . Its directional derivative is .
The directional limiting subdifferential collects the limits of Fréchet subgradients with , and .
The critical cone of (VP) consists of the with
Let be a local minimizer of (BP). Suppose is directionally Lipschitz and directionally differentiable at in direction , that , and that (VP) is calm at in direction . Then there exist , and with
Theorem 5.1 gives a KKT condition for bilevel programs under a regularity assumption checked in one critical direction only. Directional calmness is weaker than classical calmness, because the neighbourhood is smaller than a ball. The conclusion is also sharper than the nondirectional KKT condition: the subdifferential of is the directional one, and the multipliers satisfy the extra orthogonality conditions with and . Example 3.1 of the paper is a bilevel program in which partial calmness and calmness fail but calmness in a nonzero critical direction holds. Theorem 5.1 applies there, and the classical results do not. Section 5 of the paper derives verifiable sufficient conditions (directional quasi-normality, Theorems 5.2–5.3) from it.
The result is proved in the paper; nothing here is open mathematically. To our knowledge none of it has been machine-checked. A formal proof would check a chain that passes through Ekeland's variational principle, a Fermat rule and a chain rule for limiting subdifferentials, and a limiting argument with directional sequences. The general Theorem 3.1 is reusable for any inequality-constrained program with directionally Lipschitz constraints.
The obvious route is "calmness gives exact penalization, then Fermat's rule". For directional calmness this only says that minimizes the penalized function on the directional neighbourhood, which is not a neighbourhood of . Fermat's rule cannot be applied at itself, so the stationarity must be produced at points inside the cone that approach along the direction, and then passed to the limit. That passage needs the multipliers to be bounded and the limiting subgradients to be directional ones.
The bilevel step adds two obstacles. The constraint is nonsmooth and extended-valued, so its subdifferential has to be split exactly into and the -part of . And when the conclusion still requires an element of , which exists only because is directionally Lipschitz.
EuclideanSpace ℝ (Fin q) (E q). The pair lives in WithLp 2 (E n × E m), the Euclidean product; the bare product type would carry the sup norm. Theorem 3.1 and its milestones are stated on any finite-dimensional real inner product space, which is linearly isometric to ; this lets the goal apply Theorem 3.1 on the product.EReal-valued infimum: when the lower level is infeasible, when it is unbounded. The constraint of (VP) is evaluated in EReal. " directionally Lipschitz" includes finiteness of on , which Definition 2.4 leaves implicit because it is written for real-valued maps. Directional differentiability is that of as a real function on that set, and its value is passed explicitly and enters the critical cone.NonconvexSplitting.Shared.IsRegularSubgrad, and the directional normal cone is the published SetConstrSOC.Directional.dirLimNormal. Each is an inner product, and is . "" is stated as the existence of one that makes the sum zero, including when .A complete development needs Ekeland's variational principle (on the platform as EkelandVP.General.ekeland_variational_principle) and the Fréchet and limiting subdifferential calculus: the Fermat rule, the sum rule with a smooth function, and the chain rule for a Lipschitz composition. It also needs the fact that Lipschitz functions have bounded subgradients. These are reusable well beyond this mission. Proofs of any milestone are welcome, as are proofs of the subdifferential calculus lemmas as separate theorems.
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.