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?
Under fee-for-service payment, a hospital and its physicians receive separate payments for treating a patient. Under a bundled payment, a payer makes one payment for an episode of care, leaving the hospital to pay the physicians and cover the treatment costs. A bundled contract can reward the use of a less costly clinical pathway, but the hospital and physicians need not value the resulting change in care in the same way. The question in Vlachy, Ayer, Ayvaci and Raghunathan's study is when the payer, hospital and physicians can all gain from moving to a bundle. Their base model makes physician integration—the extent to which physicians' decisions are aligned with the hospital—a parameter of that question.
The mission concerns the paper's first main result, Theorem 1. It asks for a machine-checked account of the model's simultaneous effort choices under fee-for-service, its two-stage game under bundling, and the payment interval that would improve all three parties' positions. The paper's printed sufficient conditions need two disclosed corrections to give the strict benefits it states; the mission makes those conditions explicit.
A patient's treatment follows one of two pathways. Pathway 1 is more intensive and more costly to the hospital than pathway 2. Care intensity is the share receiving pathway 1. The hospital and physicians choose efforts ; the physician integration coefficient is . Their choices determine intensity by equation (1):
The hospital pays costs for the pathways, and physicians receive . Write and . Both are positive. The quality-maximizing intensity lies in . Physicians incur the quadratic loss , where ; a hospital may incur the corresponding loss weighted by . This mission treats the base model, in which .
With fee-for-service, the hospital receives and pays the pathway costs. Physicians receive their pathway-dependent fees. The two efforts form a simultaneous pure-strategy game. Under bundling, the payer instead pays to the hospital. The hospital pays the physicians their pathway fees and a gainsharing amount , where . It chooses first; then the hospital and physicians simultaneously choose efforts. A bundled outcome is a subgame-perfect equilibrium if its continuation is a Nash equilibrium for every feasible , and the selected maximizes the hospital's resulting payoff.
Let be fee-for-service equilibrium intensity and let be the payer's fee-for-service total. The payer benefits when ; the other two parties benefit when their bundled payoffs strictly exceed their fee-for-service payoffs at the same . These are the three comparisons used in the paper's proof of Theorem 1, p. 35.
The primary target is a corrected sufficient condition for a bundled payment at which all three parties strictly benefit. Define
Theorem 1 is stated under
For every fee-for-service Nash equilibrium, it asserts the existence of one payment and at least one bundled subgame-perfect equilibrium, with strict hospital and physician gains at every bundled subgame-perfect equilibrium for that payment. The mission's milestones characterize fee-for-service effort and intensity, bundled continuation equilibria, the relevant gainsharing equilibrium, payer savings and the physicians' strict gain. The savings formula is the two-case expression in Proposition 2, equation (12), on either side of .
The result identifies a parameter region where the payer can spend less while the hospital and physicians each receive a strict improvement. Its conditions connect the hospital's cost difference, the physicians' payment difference, their quality concern and the existing level of physician integration. The payer's savings expression also shows how the available margin changes as integration moves past . These are precise statements about this model; they do not claim that any observed hospital will adopt a bundle.
The cited SSRN preprint contains proofs on paper, including Appendix B for the base model. This mission asks solvers to formalize those results, the equilibrium definitions and the corrected boundary conditions in Lean. The goal and milestones are open formal statements here; the existence of a paper proof does not mean they already have machine-checked proofs. The generic two-player and two-stage equilibrium definitions are reusable for other payment or contracting games.
The first-stage hospital payoff depends on the second-stage equilibrium. As varies, the physicians' effort can sit at either boundary of or in its interior. In particular, when , the hospital's payoff as a function of is not globally concave. An interior first-order condition alone therefore does not identify its global choice. The comparison with and with continuation games at larger matters to a subgame-perfect statement. The exact cutoff also matters: at a payer-savings boundary, a weak inequality yields zero savings rather than the strict benefit in Theorem 1.
All primitive payments, costs, intensities and efforts are real numbers. Efforts lie in , ranges over , and . The model retains both and in its payoffs, with stated in each base-model theorem. A continuation selection specifies a pure Nash equilibrium after every feasible , including off-path choices; the hospital's first-stage condition compares all those choices. The goal never substitutes an explicit candidate effort or gainsharing formula for equilibrium, and it asserts equilibrium existence so its universal clause cannot hold vacuously.
The printed Theorem 1 uses . The mission uses because equality can leave no strict payer savings. It also states , the interior condition from Lemma 5 (34); without it, the printed sufficient conditions admit a case where the hospital chooses . The added condition confines the goal to the paper's interior regime (Lemma 5 Case A part 1); the corner regime with , which Lemma 2 also mentions, is not covered, because there the printed conditions are not sufficient and the paper gives no replacement. These are corrections to the preprint's claimed sufficient condition, not standing assumptions silently attributed to its theorem. The bundled payment in the goal is chosen within a beneficial interval, rather than fixed at the hospital's break-even payment, which would make the hospital's gain zero. The separate savings definition uses that break-even payment solely to measure the interval available to the payer.
The development needs real algebra and order, compact effort intervals, best responses, a two-stage equilibrium predicate and the piecewise payment formulas. The game predicates and boundary analysis can support other formal models. Contributions establishing the milestone statements, refining the comparison at boundary cases, or formalizing other results of the paper are welcome. The general model with and mandatory bundling results are outside this mission.
Research and development partners may begin a project with different capabilities, then learn to perform some of each other's work. A contract written before that learning must govern who develops the product after the parties discover what they can do. A fixed buyout price can leave development with a party that implemented the new capability poorly. Taneri and Crama study contracts that let the recipient of an offer reverse the transaction and buy out the offeror at the offered price. Their reciprocal option is intended to address this allocation problem while preserving a price chosen after capabilities are acquired (Taneri and Crama, §4.4).
This mission isolates the offer decision after both parties have acquired the other's capability. At that point the uncertainty is how well each has implemented it. The paper's Proposition 5 specifies a strike price and the parties' offer behavior in the two parameter regimes. That offer game is also an input to the paper's subsequent analysis of acquisition effort and contract comparison (Taneri and Crama, pp. 22–23).
Each party has a private implementation type , where . Type has fully implemented the other party's capability; type has implemented it only partially. Each type occurs with probability , independently for the two parties. A single developing party produces value . If the parties instead develop jointly, each receives , with . The value-creation model also gives (Taneri and Crama, pp. 8–10).
The parties decide simultaneously whether to make a buyout offer. If neither offers, they develop jointly. If one offers at price , it becomes the offeror and the other party becomes the offeree. If both offer, a fair random choice determines who moves first. The offeree may accept, leaving the offeror with the product, or reciprocate, buying out the offeror at the same price. Acceptance pays the offeror and the offeree ; reciprocation pays the offeror and the offeree . The recipient accepts when the two choices tie (Taneri and Crama, pp. 13, 21–22).
A mixed offer strategy assigns each type its probability of offering, between zero and one. The equilibrium condition is a symmetric Bayesian Nash condition: for each privately known type, its assigned probability must maximize interim expected payoff against the other party's strategy. Interim expectation uses the two equally likely types and the fair first-mover choice when both parties offer.
The main target is Proposition 5's price and offer strategies. Let . The price claim says that maximizes the offeror's expected payoff against the prior distribution of the offeree's type, for either offeror type and every candidate :
At that price, the claimed symmetric equilibrium profiles are
In the second regime , so the full implementer genuinely mixes. The equality boundary belongs to the first regime. The milestones isolate the offeree's response, the strike-price claim, and each of the two strategy cases. These are the clauses of Proposition 5 and a response stated in the surrounding discussion (Taneri and Crama, pp. 22, 25–26).
The result identifies when each implementation type initiates a buyout under a contract that lets the recipient reverse the offer. In the first regime, only a full implementer initiates a transaction. In the second, a partially implementing party always offers while a full implementer sometimes waits for the chance to reciprocate. The mixed behavior shows that both fully capable parties can decline to offer and continue joint development, even though a completed buyout would pay each more than joint development in that regime (Taneri and Crama, p. 22).
The paper gives the statement of Proposition 5, but its proofs are in an eCompanion that is absent from the held SSRN working paper (Taneri and Crama, p. 11). The mission therefore starts with open Lean theorem statements. A completed proof will check the price comparison and the strategic best-response claims against an explicit offer game. The generic binary-action Bayesian game interface and the reciprocal-option payoff definitions can support subsequent formalization of effort incentives and related buyout mechanisms.
The offeree's choice changes at price thresholds because reciprocating yields while accepting yields . Consequently, the offeror's price payoff changes form at those thresholds. The strategic decision to offer also depends on the other party's private type and on whether simultaneous offers place a party first or second. A direct comparison of an offeror's revenue with the joint-development payoff does not settle the equilibrium: being the offeree can be preferable to offering. The second regime requires a type- player to be willing to use a probability strictly between zero and one while type offers with certainty.
Lean uses real-valued prices, payoffs and probabilities. The implementation type has exactly two constructors, partial and full. Its prior assigns probability to each. The offeree's acceptance at indifference, the random first mover after simultaneous offers, and the payoff after no offers are encoded in the game. Candidate strike prices range over all nonnegative real numbers; strategy deviations range over every real probability in . The denominator is positive under the standing assumption.
The strike-price clause evaluates the offeror's payoff against the prior on the offeree's type. The paper says the price is set with reference to the anticipated offeree response, independently of the offeror's own implementation level, and treats price and offer decisions separately (Taneri and Crama, p. 22). Conditioning instead on which party becomes the offeror in the equilibrium changes the type distribution; that alternative is outside this target. The stated profiles are equilibria, without a uniqueness claim. The additional explicit inequality comes from the paper's underlying value-creation model, where with (Taneri and Crama, p. 10).
The equilibrium predicate checks payoffs for all unilateral offer probabilities; it does not encode the displayed value of as a best-response condition. Likewise, the offeree's response is computed from its payoff comparison, and is a candidate derived from the parameters rather than a restriction built into the game. Reusable contributions include payoff identities, finite-type expectation calculations, and general lemmas about binary-action mixed equilibria. Effort choice, the price-floor contract and comparisons among contract forms are outside this mission.
Many risk-averse decision problems are not expectations of a loss but nonlinear functions of several nested expectations. The optimized certainty equivalent of a deviation, the buffered probability of exceedance and mean–deviation criteria all take the form "a convex isotone function of an expectation of a convex function of a random map and of another expectation". Liu, Cui and Pang call such problems compound stochastic programs and study them without assuming that the inner random maps are convex or smooth (arXiv:2004.14342; Mathematics of Operations Research, 2022). Two features make them harder than ordinary stochastic programs: the inner expectation sits inside a nonlinear map, so a sample average of the objective is a biased estimate of it, and the inner maps may be nonconvex and nonsmooth, so gradient-based stochastic approximation does not apply directly.
The paper's first contribution is an algorithm that combines majorization–minimization (replace each nonconvex map by a convex majorant that touches it at the current point) with incremental sampling (enlarge the sample at every iteration), and a proof that its accumulation points are, almost surely, fixed points of the surrogate scheme. This mission formalizes that convergence theorem.
Let be a random variable with law on a measurable space . The data are a nonempty convex compact set , Carathéodory maps and , and outer maps and . The compound stochastic program (1) is
A map is isotone if it is nondecreasing componentwise. Assumption (A2) asks and to be isotone, Lipschitz (constants , ) and convex (each component of ). Assumption (A4) bounds the variances of and by , uniformly on .
A surrogate family (A3) assigns to every base point and sample a nonempty set of maps that touch at , majorize on and are componentwise convex on ; in addition the family is uniformly outer semicontinuous in , with an integrable modulus . (A3) is the same for . Selecting surrogates for every gives the convex majorant
a member of the family ; it is well defined when the expectations exist.
The SMM algorithm keeps two growing independent i.i.d. samples and of . At iteration it uses the first of each, chooses surrogates at the current iterate , forms the sample surrogate by replacing both expectations with sample averages, and sets
Let , let the sample sizes satisfy the growth conditions of Lemma 3, and assume (A1)–(A4). Then, with probability 1, for every accumulation point of at which condition (E) holds (for almost every the family is a compact convex subset of with an integrable envelope, and likewise ), there is a well-defined with
The theorem says that the SMM iterates cannot accumulate anywhere except at points that are optimal for a convex majorant touching there; §4 of the paper converts this fixed-point property into directional stationarity for smooth, difference-of-convex and max-smooth inner maps. It is the convergence guarantee behind a practical method for minimizing risk measures of nonconvex random losses, and it is the first such guarantee for incremental-sampling majorization–minimization on nested expectations.
The result is proved in the paper, but the published argument leaves steps open: it uses the uniform almost-sure convergence of Proposition 2(a)–(b), which needs an integrable envelope that (A1)–(A2) do not provide, and it applies the fixed- bound of Proposition 2(c) at the sample-dependent iterate . A complete machine-checked proof would settle whether the theorem holds under the printed hypotheses or needs a further assumption. No part of the paper has been formalized before. The milestones are true statements in their own right; the goal is posed as printed.
The obvious route is "the SAA objective decreases up to summable errors, so the Robbins–Siegmund lemma applies". The errors, however, are bounded in expectation only for a fixed point, while the iterates depend on the very samples entering the errors; a uniform-in- rate is not part of the hypotheses. Passing to the limit along a subsequence then needs a selection of limiting surrogates that is uniform across the samples, and identifying the limit of the averaged surrogates with an expectation requires a strong law of large numbers for i.i.d. random compact convex sets in the Banach space (Puri–Ralescu, Ann. Probab. 1983), which is not in Mathlib. Finally, every expectation inside and must be controlled through a nonlinear isotone map.
is EuclideanSpace ℝ (Fin k) with the Euclidean norm, which is the norm the paper's constants use; is curried in , its Lipschitz bound uses the Euclidean norm of the pair, and isotonicity is joint in both arguments. The law lives on a measurable type ; the samples live on a separate probability space and are jointly independent. The open set containing is dropped, since only values on matter. Sample indices are 0-based, (the page leaves undefined), and a run chooses each surrogate as a measurable function of the iteration, the current iterate and the sample value. Iterates are assumed measurable. Lemma 3's constants are required to be positive; without this the sample sizes qualify and the lemma is false. The printed coefficient of has the wrong sign and is corrected. (E) is imposed on both surrogate families, and its expectation of a supremum is an integrable envelope.
Trivializing formalizations are ruled out: the limiting surrogate must be a selection from the families , ; "well defined" means the integrability of every expectation in for every (otherwise a junk integral of makes any point a minimizer); accumulation points are those of each sample path, inside the almost-sure event; and the surrogate families are nonempty. Propositions 2(a) and 2(b) are deliberately absent: they are false under (A1)–(A2), even with (A4).
A complete development needs a strong law of large numbers for i.i.d. random compact convex sets in a separable Banach space, conditional-expectation bookkeeping along the growing sample, and the Robbins–Siegmund lemma (posed on the platform as an open statement and referenced here). The random-set law of large numbers and the compound SAA bound of Proposition 2(c) are reusable beyond this mission. Proofs of any milestone, and of the open Robbins–Siegmund statement, are welcome.
Charity watchdogs rate nonprofits by their program expense ratio, the share of spending that goes to programs rather than to administration and fundraising, and donors reward a high ratio. Practitioners have long argued that this pressure produces a nonprofit starvation cycle: organizations underinvest in administration, the infrastructure that sustains their capacity to deliver services, and their capacity erodes (Goggins Gregory & Howard, Stanford Social Innovation Review, 2009). Whether a nonprofit that maximizes the needs it meets should in fact starve administration is an optimization question, and Kotsi, Aflaki, Aydin and Pedraza-Martinez pose it as a two-period budget-allocation problem (SSRN 3460795; later published in Manufacturing & Service Operations Management, DOI 10.1287/msom.2020.0660). Their main structural result, Proposition 1, says that the answer depends on the nonprofit's current capacity through two thresholds.
A nonprofit lives for two periods. In period it has budget , needs and capacity . Each program dollar meets dollars of needs, with . Keeping capacity costs the required administration , convex and nondecreasing. Spending on discretionary administration raises next period's capacity to , where , is strictly concave and strictly increasing, and . Spending on program, on discretionary administration and on fundraising raises the donations
where is concave and nondecreasing on , with and for . Donations depend on the program expense ratio .
The second-period needs are a random variable with a density. The net budgets are and , and the program ceiling is . Throughout, . Lemma 1 reduces the two-period dynamic program to problem (2):
subject to , , and . The last constraint says the second-period budget never exceeds what the second-period capacity can use. The allocation exhausts capacity when that constraint binds, and leaves capacity unused when it is slack.
Fix all data except . Problem (2) has an optimal allocation for every admissible , and there are thresholds such that every optimal allocation satisfies the following.
The thresholds are asserted to exist; no formula for them is part of the goal.
The milestones follow the appendix proof:
Proposition 1 gives the structure of the optimal policy. Spending on administration is optimal at low capacity. At moderate capacity, the nonprofit spends on administration only when the program ceiling binds. Starving administration while leaving capacity unused is optimal only at high capacity. This turns the starvation-cycle debate into a statement about where a given nonprofit sits relative to and . The paper's case study and numerical sections build on this classification.
The paper proves the result by hand, with implicit-function calculus over several threshold functions of . No machine-checked version exists. A formal proof would confirm the case analysis, including the boundary cases that the printed statement gets wrong (see Formalization scope). It would also produce reusable facts about the concave function and about one-parameter families of concave programs.
Problem (2) is not concave in , because the donation term divides by the total spending. So the Karush–Kuhn–Tucker conditions are neither necessary nor sufficient, and no general convexity argument applies. The proof splits on whether the capacity constraint binds. Each branch has its own maximizer and its own thresholds in (, , ), and these move with . The goal then requires comparing the two branches uniformly in . A threshold in exists only if certain differences of these maximizers are monotone in , and that monotonicity comes from second-order implicit differentiation of the root of equation (4). A pointwise analysis at a fixed does not give the thresholds.
All quantities are real. The data form a structure Params, and is the law of . The capacity is a separate argument, quantified over the paper's range , . The expectation is an integral against . An optimal allocation is a feasible point whose objective is at least that of every feasible point. The goal asserts existence separately and then quantifies over all optimal allocations.
Added hypotheses. The formalization adds the following to the page's assumptions:
Strictness and full support are needed for the uniqueness claims. Without them, can be flat at its maximum, and optimal allocations can fall in two cases at once. Full support is how "Ψ can take any value in " is read.
Repairs to the printed statements. Each is disclosed in the item concerned.
The comparison "" is stated as a condition on , not as a defined number. The thresholds , the root and the maximizers enter as variables characterized by hypotheses.
Ruled out. The thresholds are chosen once for all admissible , and the goal includes existence of an optimum. So the goal cannot hold vacuously, and it cannot be met by thresholds that depend on .
Infrastructure. A complete development needs the following:
The first and last are reusable beyond this mission. Contributions toward any milestone, or toward these general lemmas, are welcome.
A hog producer selling to both a meatpacker and an open market faces a weekly allocation choice. The meatpacker contracts for a fixed quantity, pays different rates for underweight and regular-weight hogs, and charges for any shortfall. The open market has separate prices for the two weight classes. Holding an underweight hog costs money now but makes it regular-weight next week. These features make a single “sell or hold” rule inadequate: fulfilling the contract changes the value of the next hog allocated to either market. Kouvelis, Liu, Qiu and Turcic model this setting and state a price-dependent, multiple-threshold sales policy in Proposition 1 of their March 6, 2023 preprint.
The stated policy is of direct interest for inventory decisions with quality upgrading and contractual penalties. It also provides a precise test case for dynamic programming with continuous stock decisions, stochastic prices, and a capacity-constrained contract. The mission concerns the mathematical policy statement, rather than the paper’s empirical estimates or numerical comparisons.
At the start of period , the producer observes underweight and regular-weight hogs and the price vector . The contract requires hogs. A regular-weight hog sent to the contract earns ; an underweight one earns . Open-market prices are . Holding costs per hog, and a contract shortfall costs per missing hog. The discount factor is .
The decision is sent to the contract and held. Open-market sales are . Every decision is nonnegative; and . The immediate reward is
Newly available hogs next period are . Both classes of held hogs enter the regular-weight pool, so . The value function is the maximum expected discounted reward from periods through , with , as in equations (4) and (7a)–(7c) of the preprint.
For total holding , write . Its increments are the holding margin. The fulfillment margins are and ; the spot margins are and . A break-even level for margin is the least nonnegative at which every forward increment of is no greater than times the increment. The mission uses this level truncated at .
The first targets are concavity of the value and action-value functions (Lemma 1), preservation of concavity in total holdings (Proposition 1, proof Step 1), and the holding-margin bound corresponding to Lemma 2(1). The one-period attainment result from Proposition 1, proof Step 2, connects those properties to the explicit actions. These are the four milestones.
The goal is the corrected part of Proposition 1, Cases 1(a), 1(b), 2(a), and 2(b). In each case, the indicated action must satisfy the feasibility constraints and attain the dynamic-programming value:
The cases split first on or , then on the underweight fulfillment and spot margins. The explicit quantities are in the goal theorem. Its thresholds are computed from and the observed stock and prices, so the target is a policy for the original dynamic program. Proposition 1 also prints Case 2(c), but its multi-period formula is false under the paper’s stated assumptions and the additional no-arbitrage bound below; this mission does not assert it.
The result identifies feasible, optimal contract, spot-market, and holding quantities in four observable price regimes. It gives a policy rather than an existence statement: a producer can determine the action from the current stock, prices, and three break-even levels. The holding thresholds are linked to the actual continuation value, which matters when future penalties or regular-weight prices change.
The preprint supplies a proof on paper; these particular Lean statements do not yet have verified proofs. Formalizing them would yield a checked dynamic program and reusable facts about a concave continuation value, a shared holding pool, and a linear contract capacity. The corrected statement also separates the regimes that the available numerical checks support from the printed Case 2(c), which has a concrete counterexample. The four milestones expose the mathematical obligations needed to complete the verified result.
The continuation value depends on the sum , while the two pools have different fulfillment and spot prices and share one contract capacity. A comparison of each pool’s holding and selling margins in isolation therefore does not settle the allocation: holding one pool changes the marginal value of holding the other. The dynamic value is also defined by a supremum over a continuous feasible polytope and an expectation over future data. The central difficulty is obtaining a well-defined, concave value function and then showing that each explicit threshold action attains it. The paper’s no-arbitrage assumption controls expected contract and spot price changes, but does not control a jump in the next period’s contract penalty; Lemma 2(1) fails without an additional bound.
Lean uses real-valued stocks and decisions, a positive finite horizon, and a time-indexed Markov kernel on an exogenous information state . Taking to include the observed history represents the paper’s general adapted price and supply process; the formalization imposes no independence between supply and prices. Prices and supplies are measurable, nonnegative, and uniformly bounded. These are disclosed well-posedness additions that keep the expectations integrable and the real supremum finite. It also assumes , , , and .
Assumption 1 from page 14 is retained. The added condition A* bounds the discounted expected next-period maximum of the regular-weight fulfillment and spot margins by the present maximum plus holding cost. Without it, a two-period instance with next-week penalty makes the printed Lemma 2(1) policy worth while holding is worth . The corrected Case 1(b) holding quantity is the unsold underweight stock capped by its spot break-even level. Case 2 uses a regular-weight holding threshold net of already held underweight hogs. The printed Case 2(c) can yield when a feasible action yields , so it is excluded. These departures are recorded item by item in the moderation notes.
The definition layer contains the reward, feasible actions, Bellman recursion, continuation value, and break-even levels. A complete proof also needs measurability and integrability of the recursively defined value, compact feasible sets, concavity under integration and partial maximization, and real infimum properties. Contributions to those reusable results, the four milestones, and the corrected goal are within scope. A formulation with free thresholds or a free value function would make the policy claim empty; both are computed from the model data here.
When a financial institution fails, its counterparties on over-the-counter derivatives are exempt from the automatic stay of bankruptcy: they may terminate their contracts at once, accelerate what is owed to them, and seize posted collateral. Whether this exemption stabilizes or destabilizes the system has been debated since the 1990s, and the failure of Lehman Brothers in 2008 sharpened the question. Termination turns contingent contract values into immediate payment obligations, which can push further institutions into default. But it also brings cash into the system and frees collateral, which can let other obligations be met.
Ghamami, Glasserman and Young (Management Science, 2022) build a clearing model in which payments, collateral seizure, returned collateral and contract termination interact over successive rounds. They compare two policies. Under full termination the default of a node accelerates every derivative contract it is party to, in both directions. Under selective termination (creditor "cherry-picking") only the obligations of the defaulted node become due. Their headline comparison is that, under a bound on aggregate derivatives leverage, full termination leaves no larger system-wide payment shortfall than selective termination.
A finite set of nodes. For nodes : is the payment due from to , with total ; is the cash of ; is the collateral posted by for its obligations to ; is the value to of its derivatives with , owed by on termination, with . Diagonals vanish and obligations are netted (). Collateral has constant value .
Round 1. Given payments , node has assets and defaults if ; is the default set. A creditor of a defaulted first seizes , and the rest of 's assets is shared pro rata over the residual claims . Clearing payments are the nonnegative solutions of these fixed-point equations. Excess collateral is returned after Round 1: a defaulted node gets back what was not seized, a surviving node gets back what it had posted to defaulted nodes.
Proposition 2.1 also treats a Round 2 without derivative termination: remaining obligations are , paid from returned collateral and incoming payments. Its total-payment identity (15) is included.
Rounds under full termination. A default in round creates the obligation between the defaulted node and each counterparty that has survived; unpaid obligations carry over; two survivors owe each other nothing. A node's assets in round are its cash , its returned collateral and the payments it receives; it defaults in round if they fall short of its round- obligations, and payments again solve a pro rata fixed-point equation. is the full-termination default set.
Selective termination shares Round 1, and in Round 2 only defaulted nodes owe: for , else . No node defaults after Round 1, and payments solve the Round-2 equation.
The payment shortfalls are
with the total paid by over all rounds and its total over the two selective rounds. The net worth at the end of Round 1 is .
With constant collateral price, common first-round payments, and both models taken at their largest, or both at their smallest, second-round clearing payments ((37) or (38)), the aggregate derivatives leverage condition
implies
The result. Proposition 5.2 is the paper's formal answer to the policy question raised by the safe-harbor debate: it identifies a balance-sheet condition, derivatives liabilities bounded by equity in aggregate, under which the stay exemption does not worsen the total amount of unpaid obligations, even though full termination always produces at least as many defaults (Proposition 5.1). The paper's Example 5.1 shows that without such a condition the comparison can go either way and by arbitrary amounts.
Formalizing it. The paper gives proofs; none is machine-checked. A formalization fixes the accounting of a multi-round collateralized clearing model precisely. This matters here: read literally, the cash recursion of §4 drops unsold returned collateral, and with it Proposition 5.2 (i) fails on a four-node network. The mission states the repaired accounting under which the paper's argument goes through. It also produces reusable statements about extremal fixed points of Eisenberg–Noe-type clearing maps with collateral and their monotone comparison.
The two models are compared at fixed points of different maps, and fixed points need not be unique; a pointwise comparison of arbitrary solutions is false in general. The comparison has to be made at extremal fixed points, through monotone comparative statics in the parameters (obligations and pro rata proportions), and both the largest and the smallest cases are needed. Second, full termination runs up to rounds with new defaults in each; the shortfall bound requires tracking each node's cash, returned collateral and payments across rounds, and showing that a node defaulting after Round 1 has paid out at least its Round-1 net worth. The tempting shortcut, assuming that full termination creates no new defaults (), turns the goal into Corollary 5.1, a different and weaker statement.
All values are real numbers; nodes form a Fintype with decidable equality. One definitions file CollatNet.Termination.Model holds the network, its standing assumptions, Round 1, the §2.3 freed-collateral Round 2, a round state (cash, returned collateral, obligations, survivors), the full-termination round map, the selective Round 2, default sets, shortfalls and net worth. Conventions:
IsGreatest/IsLeast in the componentwise order on each model's round-2 clearing set; later full-termination rounds may be any clearing payments.Case (ii) of Proposition 5.2 (illiquid collateral, no excess collateral) is not posed: it is false as printed, because returned collateral is sold below its Round-1 value.
The goal must keep (40) as its hypothesis. Replacing (40) by , or dropping the later full-termination rounds (which forces by construction), would state Corollary 5.1 instead.
Needed infrastructure: Knaster–Tarski on boxes in (Mathlib's OrderHom.lfp/gfp), a monotone comparison of extremal fixed points, and finite-sum bookkeeping over rounds. The extremal-fixed-point comparison and the node-total property of pro rata clearing are reusable for other clearing models. Proofs of any milestone are welcome; the shortfall identity and the dominance of round-2 parameters are the most self-contained.
Firms that collaborate on research and development must share proprietary knowledge to make the collaboration work, yet the knowledge they share can later be used against them: a partner that has learned from the alliance can walk away and use what it learned on a rival project. Management research calls this the appropriability hazard of alliances. Arora, Belenzon and Patacconi (Management Science, 2021) model knowledge sharing as a property-rights problem in the tradition of Grossman–Hart and Hart and Moore (1990): knowledge sharing is an ex ante investment that shifts the partners' ex post outside options, and payoffs are fixed by bargaining after the investment is sunk.
The paper's main structural question is whether a firm can mitigate the hazard by organising its collaborations as a portfolio of alliances rather than as a single alliance. The answer it gives, Proposition 6, is that it can: there is a range of parameters in which a single alliance cannot sustain knowledge sharing while a portfolio of two alliances can.
Single alliance (§2). A focal firm and a partner each pay a private cost , with , to share knowledge. After sharing, implementing the project together creates value ; if the alliance is terminated prematurely, and obtain their ex post outside options and . It is assumed that . Bargaining follows the Nash solution with equal weights, so firm obtains
Firm 's knowledge-sharing constraint is . Knowledge sharing is efficient if .
Alliance portfolio (§4.1). The focal firm now has two partners and , on the player set . The partners' outside options are normalised to . After knowledge sharing in both alliances, the value created by a coalition that implements together while its alliances with outsiders are terminated is (Table 1)
with . The parameter is the synergy between and in implementation, measures substitutability in implementation and measures substitutability in rival benefits. Gross payoffs are the Shapley value
and since bears in each of its two alliances, the net payoffs are , and . Knowledge sharing in a configuration is feasible when every firm's knowledge-sharing constraint holds.
Under the standing assumptions, suppose . If
then knowledge sharing in the portfolio is feasible (), while knowledge sharing in the single – alliance (with ) is not.
The result. Proposition 1 shows that in a single alliance, efficiency () does not imply investment: shifts in bargaining positions, measured by , create underinvestment. Proposition 6 identifies a structural remedy. A second partner changes the bargaining game: the synergy is created only when all three firms cooperate, and substitutability in rival benefits weakens the focal firm's threat point, both of which raise the weak partners' Shapley payoffs. The paper uses this to argue that alliance portfolios with the right characteristics can sustain knowledge sharing that a dyadic alliance cannot, and that substitutability among partners is not uniformly harmful.
Formalizing it. The proofs are relegated to an online appendix that is not part of the source manuscript, so the mission produces the first complete, checked derivation of the portfolio result from the model's primitives: the Table 1 game, the Shapley value and the cost allocation. A search of the platform found none of these statements already formalized; the Shapley value itself is reused from an existing platform definition.
The computations are finite and elementary, so the difficulty lies in carrying out the Shapley sum over all coalitions of a three-player game honestly, rather than by quoting the closed forms (9)–(10), and in tracking the asymmetric cost allocation: the focal firm pays , the partners each. A second point is that the paper assumes the focal firm's constraint "to facilitate the comparison"; the formal goal concludes it from and the standing ranges, so it must be derived, not assumed.
Players are Fin 3 with , , ; all parameters are real numbers. The game game V b πF sImp sRB assigns to every coalition without and, to a coalition containing , the Table 1 value determined by its size, with . The gross payoffs are the platform's published Supermodularity.Cooperative.ShapleyValue applied to this game. Single-alliance payoffs follow eq. (1), and both notions of feasibility are defined from the payoffs: SingleFeasible is , PortfolioFeasible is for every player. The standing assumptions , , and are bundled in Standing. "Feasible" refers only to the knowledge-sharing constraints; the coordination problem of the investment game (footnote 10) is ignored, as in the paper.
A trivializing formalization would define by the closed forms (9)–(10) or feasibility by the inequalities (5) or (11), which would make the milestones true by definition and the goal a linear inequality between its own hypotheses; the definitions here are the Shapley sum and the payoff constraints, so those closed forms must be proved.
No probability, measure theory or analysis is needed; a development needs finite sums over the powerset of Fin 3 and linear arithmetic over ℝ. A reusable by-product is a computation of the Shapley value for three-player games with a distinguished player, which recurs in property-rights models. Proofs of the milestones and of the goal, in any order, are welcome.
A client who needs to buy a security may hire a dealer to execute the purchase. The client can observe market prices and trading volume but cannot observe the dealer's trades or the market conditions known to the dealer before trading. A contract based on the closing price or another benchmark can therefore change the dealer's incentives. Baldauf, Frei, and Mollner study when a familiar benchmark, the volume weighted average price (VWAP), implements the outcome the client would choose if the client could control the trades directly (Baldauf, Frei, and Mollner, 2022, §§3–5 of the August 8, 2020 working paper). The question matters wherever a benchmark price determines the payment for an order that an intermediary also influences through its execution.
A client asks a dealer to acquire one share over a finite number of periods. A trading schedule is a vector with and . Before trading, the dealer sees a vector of positive market conditions ; the client does not. Neither party observes the price shocks in advance. In the specialized model, the dealer chooses a static policy , so the whole schedule depends only on and cannot react to prices realized during trading. These information and policy restrictions are stated in §§3.1 and 4.1 of the working paper.
Period has price and total market volume . The paper assumes that is strictly increasing, is strictly convex, is positive on the relevant domain, and for , where is strictly decreasing. Every shock has the same conditional mean: almost surely. The paper imposes no independence or identical distribution requirement on the components of or . The dealer's utility is strictly increasing and concave.
A contract specifies the client's payment using only the observed price and volume vectors. The dealer's monetary payoff is , and the dealer's expected utility must be at least , the utility from rejecting the contract. Incentive compatibility means that the recommended policy maximizes the dealer's expected utility among static policies. The client chooses a contract and a recommended policy to minimize subject to those two constraints. This is the paper's second best problem; an optimal contract is part of a solution. The VWAP contract pays the realized volume weighted average price, (working paper, pp. 10–12, 21–22).
The paper identifies the first best policy, the schedule the client would choose with direct control of trading:
Its expected trading cost is , and its share of each period's total market volume is . The mission includes Lemmas 10 and 11 on conditional means (their static case 1), both parts of Lemma 12's weighted inequality, the Jensen step of the proof of Lemma 3, the three sentences of Lemma 3 (the first best policy and its uniqueness, its expected cost, and its volume shares) as separate statements, and the sufficiency part of Lemma 4. It also records the full insurance and strict incentive claims stated in the proof of Proposition 5. These are the results the paper uses to reach its main assertion (working paper, pp. 21–23, 44–47, 50–53).
Proposition 5 says that the VWAP contract itself solves the client's second best problem:
The comparison covers every measurable contract on prices and volumes and every admissible static policy. The goal does not select an impact function, a volume law, or a utility curve beyond the paper's assumptions (working paper, Proposition 5, p. 22).
Proposition 5 gives a condition under which a common benchmark contract reaches the same expected payment as direct control of the dealer's trading. The result links the first best schedule, the realized VWAP, and the dealer's incentives without specifying a distribution for market conditions or independent price shocks. Under the contract, the first best schedule leaves the dealer with zero realized monetary surplus, while other static schedules yield strictly lower expected utility in the paper's model (working paper, pp. 22–23 and proof on p. 53).
The published paper proves these statements. They do not yet have machine checked Lean proofs. A complete development would supply reusable definitions for static execution policies, price and volume outcomes, contracting constraints, and conditional cost comparisons, together with proofs of the paper's auxiliary inequalities.
A direct comparison of expected VWAP payments across schedules does not establish incentive compatibility: the dealer cares about expected utility of payment minus trading cost, and both terms change when the dealer changes the schedule. The relevant volume weights depend on the same schedule that changes price impact. The key difficulty is the strict equality case in Lemma 12's weighted inequality, including periods in which the dealer trades zero shares. Conditional means must also be carried through schedule dependent but measurable weights, while the final client comparison ranges over all feasible measurable contracts. Dropping that broad comparison would state a substantially weaker result (working paper, Lemmas 10–12 and proof of Proposition 5).
Time is indexed by Fin T, with paper period represented by Lean index . The probability space is arbitrary, its measure is a probability measure, and . Market conditions are positive at every outcome. Shocks are integrable and have conditional mean given the sigma algebra generated by . The model assumes measurability of , , , and ; it also assumes integrability of so the stated first best cost is finite. These measurability and integrability clauses make explicit conditions used by the paper's expectations but not separately listed there.
Policies are measurable maps from to schedules on the positive market condition domain; Lemmas 10 and 11 (case 1) are stated, as in the paper's appendix, in a general framework with only their own hypotheses: Lemma 10 for measurable functions of summing to one almost surely (with integrable), Lemma 11 for measurable nonnegative functions of that need not sum to one and any positive measurable volume function . Contracts are measurable functions of the price and volume vectors; their values off positive volume vectors are irrelevant. Feasible contract policy pairs require finite expected payment, cost, and dealer utility. Incentive compatibility compares against static deviations with integrable utility; under VWAP the omitted deviations cannot improve the dealer's expected utility, while this convention makes the competing contract class at least as demanding for optimality. First best is expressed by almost sure comparison of conditional expected costs. The properties of and are imposed on the nonnegative and positive arguments actually used by schedules. Positivity of volumes makes the VWAP denominator nonzero on realized outcomes. These conventions exclude empty schedules, division by zero at realized conditions, and Lean's default zero integral for nonintegrable payoffs.
The mission needs Mathlib's measurable functions, conditional expectations, Bochner integrals, finite sums, convexity, and almost everywhere relations. Its model definitions and the deterministic statements (Lemma 12, the Jensen step and the volume-share identity of Lemma 3, stated for arbitrary , , and every number of periods) are meant to be reusable. Contributions may prove the conditional mean lemmas, the deterministic inequality and equality case, the first best characterization, the sufficiency criterion, or the proposition. The goal must retain all measurable contracts and feasible static policies; restricting competitors to benchmark contracts or asserting only incentive compatibility would trivialize the intended optimality claim.
Shoppers judge products differently inside a store than outside it. Lighting, the color of price tags, the position of a product on the shelf, the presence of a decoy: each of these can change how much weight a consumer puts on quality or on price at the moment of purchase. A large literature in behavioral economics documents such effects and models them. Examples are the salience model of Bordalo, Gennaioli and Shleifer, the focusing model of Kőszegi and Szeidl, and relative thinking in the sense of Bushong, Rabin and Schwartzstein. Retail practice exploits the same effects: loss leaders draw customers in, and the sale is then steered towards a different product (up-selling to a pricier, higher-quality item, or down-selling to a cheaper, lower-quality one).
A. Apffelstaedt and L. Mechtenberg (Competition for Context-Sensitive Consumers, MPRA Paper No. 99509, 2016; published in Management Science, 2021) ask what happens to such tactics under perfect competition. Consumers choose a store on the basis of the product they expect to buy. Inside the store, the context may change their mind. Consumers may misjudge how strongly it does so. The paper shows that when consumers underestimate their sensitivity to context, competition does not remove the distortion. Instead it pins down a specific fooling strategy in every equilibrium: a loss-leading attraction product and a target sold at cost. The store context is used to up-sell or down-sell from one to the other.
A product has a quality , a price and a store context : no distortion, quality-inflating or price-inflating. Outside a store a consumer values it at the undistorted surplus ; the outside option of not buying is worth . Inside a store, a consumer with context sensitivity values it at
The true sensitivity is . Each consumer has a type , her belief about , drawn from a distribution with a density and supported in . Types with are optimists. A product is acceptable if and , for a minimum quality and a maximum price .
There are firms. Each firm commits to a finite menu of products with their contexts. Consumers then move in two stages:
Selling a product of quality costs the firm . The cost satisfies , , . The cost-efficient qualities solve . The paper assumes and .
Fooling (Definition 3) is a pair: an attraction product , which a type expects to buy, and a target , which she buys. It requires (IC) and (PCC), with one of the two strict.
A competitive equilibrium is a profile of menus with three properties:
The two context technologies are store-wide (one context for all products of a store) and product-specific (one context per product). Write
Assume all types are optimists. With store-wide contexts, a competitive equilibrium exists. In every one, at least two firms have positive demand and all others offer nothing. Each active firm offers exactly two products, a target and an attraction product :
When , each active firm offers one of the two menus.
With product-specific contexts, a competitive equilibrium exists. In every one, each active firm uses with
In all cases : the attraction product is a loss leader.
The proposition shows how a behavioral bias survives perfect competition. Zero profits do not mean undistorted choices. Competition passes the gains from fooling on to consumers through the attraction product, and the store context does the selling. Which context arises (quality inflation with up-selling, or price inflation with down-selling) is decided by comparing two explicit switching surpluses. A planner can read welfare comparisons and policy predictions directly off the explicit equilibrium menus. Later results of the paper build on this one: Proposition 3 implements the contexts with one decoy under salience, focusing or relative thinking, and Proposition 4 treats mixed populations.
The result is proved in the paper; no machine-checked proof of it, or of any part of the model, is known to exist. The mission produces three things:
The formalization also records three slips in the printed proof:
The pair-level bounds are elementary inequalities. The difficulty is the market argument. The paper first derives best responses for a single type with a fixed outside option, then argues that in equilibrium every type faces the same outside surplus. Turning this into a proof requires several steps:
The naive approach treats each firm as facing a single type. That step does not carry over: demand is a positive-measure condition on a continuum of types, and uniqueness must hold for all of them.
All quantities are real numbers.
(q, p, θ) and a menu is a Finset of products; the context is carried by each product. Firms are indexed by Fin K.Proposition 2 must be stated about equilibrium profiles of firms with arbitrary finite menus. It must not be stated about the candidate menus or about two-product menus. Without footnote 4's conditions it is false (padding menus), and with a literal lexicographic cost it is vacuous (no equilibrium exists).
Contributions are welcome at every level: the pair-level inequalities (Lemmas 2–3, the best-response bounds), the market argument (at least two active firms, uniqueness of the outside option), and the existence proofs. The model file, two-stage choice under a continuum of types with a firm-favourable tie rule, is reusable for other behavioral industrial-organization results.
Influenza vaccine is made in fertilized chicken eggs, and how many doses an egg yields is not known until production is under way. By the time the season begins, the realized supply can fall short of, or exceed, what a planner would want. Two inefficiencies then compound. On the supply side, a manufacturer paid a wholesale price per dose sold carries all the yield risk and plans too little. On the demand side, vaccination protects others as well as the vaccinated person, so self-interested individuals vaccinate too little when supply is ample. When supply is scarce, high-risk individuals compete with low-risk ones under random rationing, and from society's point of view too many low-cost individuals seek the vaccine. Earlier work coordinated one side at a time: Chick, Mamani and Simchi-Levi (Operations Research 56(6), 2008) designed cost-sharing contracts between a government and a manufacturer, and Mamani, Adida and Dey (IIE Transactions on Healthcare Systems Engineering 2, 2012) studied subsidies that coordinate the vaccine market.
Arifoğlu and Tang (2022) design one program for both sides at once: a vaccination incentive for individuals and a transfer payment for the manufacturer, both contingent on the realized supply . A lump-sum tax completes it. The mission formalizes the paper's headline: this modified program attains the social optimum, balances the planner's budget in expectation, and lets the planner divide the optimal welfare between individuals and manufacturer at will.
The manufacturer plans an input quantity . The realized supply is , where the yield is random with law and finite mean, the wholesale price is , the cost per planned unit is , and .
A unit mass of individuals have infection costs uniform on , so and . A healthy individual enjoys , and vaccination costs . If a fraction is vaccinated, an unvaccinated individual is infected with probability and a vaccinated one with probability . The zero-risk fraction is the least at which the population risk vanishes (or ), and Assumption 1 of the paper imposes monotonicity, convexity and concavity conditions on and below .
When only individuals with cost above a threshold seek vaccination, the vaccinated fraction is , the fill rate under random rationing is , and the ex-post welfare is minus vaccination costs minus the expected infection losses. The planner's threshold maximizes ; its demand is
where is determined by the sign of the marginal social benefit . The planner's ex-ante problem is , with maximizer .
Without a program, individuals use the equilibrium threshold : the least cost at which the marginal individual strictly gains from seeking vaccination, , given the fraction that threshold induces. With an incentive , the right side becomes , giving . The program is
with a free constant . The planner's net payment is , and the constant is evaluated at .
With :
In addition, the manufacturer's profit-maximizing quantities are socially optimal, makes the manufacturer better off than without a program, and makes the individuals better off. Here and are computed at any equilibrium production of the chain without a program.
Proposition 7 says a planner can implement the first-best vaccination outcome under random yield with no expected subsidy. Any division of the first-best welfare is also achievable, which is what makes the program implementable: it can be tuned so that both the manufacturer and the population prefer it to the status quo. Propositions 5 and 6 isolate the two halves. The incentive aligns individual thresholds with the social optimum supply by supply, and the transfer makes the manufacturer's profit equal to social welfare up to a constant.
The results are proved in the paper and its Online Supplement; none is formalized anywhere. The mission adds three things. First, a machine-checked model of a supply chain with a consumer externality and an equilibrium threshold, which no existing formal library has. Second, corrected statements where the printed ones fail: Lemma A.1(ii) needs strict convexity, and Proposition 1's uniqueness fails at and at . Third, an explicit equilibrium concept, the least-strict-gain threshold used in the proofs, under which the coordination claim holds.
The algebra of Proposition 7 is short once coordination is known: pointwise, , and the individuals' utility collapses to . The difficulty is in coordination itself, Proposition 5(i). The marginal individual's gain must vanish exactly at and be positive above it. Above that rests on Assumption 1(iv) holding strictly. Below , where the induced fraction is capped by supply rather than by demand, a separate argument is needed. Under the fixed-point reading of equilibrium, every individual is indifferent at and coordination fails, so the threshold rule must be used exactly. Proposition 1 needs a piecewise analysis of across the point where demand meets supply, with derivatives taken one-sided at and through the kink at . Proposition 2 needs differentiation under the integral with a moving upper limit.
The model is a structure of data (, , , , , , and the law of , a measure on ) plus a predicate Standing bundling every standing condition:
The formalization commits to these conventions:
derivWithin on , and Assumption 1(ii) is imposed on ;Two corrections carry added hypotheses: strict convexity in Assumption 1(iii) for Lemma A.1(ii) and the uniqueness part of Proposition 1, and a density of for the first-order condition (10).
Trivializing formalizations are ruled out. The thresholds , and are computed from the primitives, never passed in as parameters. The manufacturer's choice under the program is concluded, not assumed. The infimum defining is over a nonempty set, and is inserted into the threshold set, so no junk value of or of a division by zero enters a statement.
A complete development needs one-sided derivatives of convex functions, piecewise monotonicity arguments, and dominated differentiation under the integral sign. The threshold-equilibrium layer is reusable for other vaccination and rationing models. Proofs of any milestone are welcome, as are formalizations of the decentralized results the mission omits: Proposition 3 (decentralized demand) and Proposition 4 ().
The moving sofa problem, posed by Leo Moser in 1966, asks for the planar shape of largest area that can be moved around a right-angled corner in a hallway of unit width — one of the most famous unsolved problems of everyday geometry. Joseph Gerver exhibited in 1992 a sofa of area 2.2195... built from five boundary curves solving a system of balancing ordinary differential equations, and conjectured it to be the largest possible; Dan Romik later derived the curves' exact formulas, and Kallus and Romik proved the best upper bound before the source. The source resolves the problem: Baek proves that Gerver's sofa is optimal, so the sofa constant is Gerver's area 2.2195..., and the sixty-year-old problem is closed.
The mission formalizes the proof of Theorem 1.1.1 of the source — Gerver's sofa attains the maximum area among all moving sofas — following the paper's own attack path: reduce to monotone sofas and their supporting rotation paths, express the sofa area through the cap and niche of the path, control the rotation angle of large sofas, take Hausdorff limits of maximum polygon sofas to obtain balanced maxima, establish the injectivity of the supporting path of a maximizer, and dominate every injectivity-constrained path by a Gerver sofa through the concavity of the area upper bound Q.
The arena is the L-shaped hallway L, the union of the horizontal side (-∞, 1] × [0, 1] and the vertical side [0, 1] × (-∞, 1]. A shape is a nonempty compact subset of the plane — the source's standing convention, adopted here — and a moving sofa is a nonempty, compact, connected shape that admits a movement around the corner. A movement is encoded by two continuous paths: a rotation angle path Θ and a translation path W, producing the rigid motion Φ_t(p) = rot(Θ t) p + W t of the unit interval, with Θ 0 = 0, the initial image inside the horizontal side, every intermediate image inside the hallway, the final image inside the vertical side, and total clockwise rotation -Θ 1 = ω, the movement's rotation angle. The area of a planar set is its two-dimensional Lebesgue measure as a real number; the maximum sofa area α_max is the supremum of the areas of all moving sofas.
The monotone arena replaces sofas by their supporting rotation paths. A rotation path x with angle ω ∈ (0, π/2] determines strips, quarter-planes Q_t⁺ \ Q_t⁻ at the outer and inner corners of the translated hallways, the parallelogram P_ω, the fan F_ω, the cap (Equation 1.3), the niche (Equation 1.4), and the monotone sofa of the path — the common part of the strips and the hallways (Equation 1.2). A supporting path pins down the canonical inner-corner path through contact: both outer walls of every supporting hallway touch the sofa. Balanced maximum sofas are stated at the level of sofas: a moving sofa that is the Hausdorff limit of maximum polygon sofas whose uniform angle sets run over a strictly increasing sequence of powers of two, with Hausdorff convergence phrased through Euclidean ε-neighborhoods rather than Mathlib's metric thickening API. The Gerver sofa is characterized by the paper's own structural properties: a moving sofa equal to the monotone sofa of its rotation path, whose supporting-hallway structure is carried by the five curves of Definition 8.4.3 with contact on the outer and inner walls and satisfying the balancing ODEs of Theorem 8.4.2 on the five intervals cut by angles 0 < φ < θ < π/4, derivatives taken one-sided within each interval. The source defers the curves' explicit formulas to Gerver's and Romik's papers; the existential form — some sofa satisfying this structure — is used for the goal and the dominating bound, since that is what the proof of Theorem 1.1.1 actually produces.
Six conventions deserve disclosure. First, the platform publishes definitions as modules Definitions.Def_<definition_name>, so the three definition bundles — the hallway arena, the monotone arena, and the Gerver sofa structure with Mamikon's swept region — are published as platform definitions (Gerver_arena, Gerver_monotone, Gerver_sofa) and attached to the proposal as reference items; the theorem drafts import them. Second, the injectivity condition abridges the source's Definition 6.1.2 by dropping its auxiliary clause on the boundary curve σ_K, keeping the continuous differentiability and the two strict derivative inequalities that the endgame consumes. Third, balancedness is stated at the sofa level rather than through the paper's rotation-path data, the sofa-level form being what the compactness argument yields. Fourth, the generalized Mamikon theorem is stated for continuously differentiable tangent segment families with continuous lengths and pairwise non-overlap on the open parameter rectangle, over turning intervals of length below π — exactly the smooth, non-self-overlapping families to which the endgame applies it. Fifth, the movement's initial term is a pure translation (Θ 0 = 0), matching the source's Definition 1.1.2 with its footnote. Sixth, all statements are developed against the platform's Mathlib build (0df444a), with inner products, rotations, scalings, and neighborhoods given by small self-contained definitions so that every draft compiles without instance-hunting.
The goal is Theorem 1.1.1: some Gerver sofa has area at least that of every moving sofa. The supporting chain, in the paper's order, each step a milestone except the last:
The goal follows by assembling the chain: every moving sofa sits under a monotone one, maximizers are balanced maxima admitting the full right angle, their supporting paths are injectivity-constrained, and the dominating bound caps them by a Gerver sofa.
The moving sofa problem is a benchmark of planar geometry that has resisted exact solution since 1966; the source closes it. The proof is not a computational verification but a structural argument — compactness produces extremal objects, contact geometry pins their supporting paths, injectivity rules out self-overlap, and a concavity argument of a kind familiar from calculus of variations delivers the dominating bound. Each layer is a theorem of lasting value independently of the goal: the cap-niche decomposition, the existence of balanced maxima, the injectivity of maximizer paths, and the generalized Mamikon theorem all predate or outlive the final step. A Lean formalization makes each layer independently checkable, and the mission's chain structure lets solvers claim credit for any layer while the community assembles the whole.
The formalization spans real analysis, topology, convex geometry, and measure theory, at a level well beyond elementary competition material but below the frontier of ongoing formalization projects. The monotone reduction and the cap-niche identity require careful handling of intersections of translated half-planes and the additivity of Lebesgue measure; the balanced-maximum existence requires sequential compactness in the Hausdorff topology; injectivity requires differentiability arguments on paths defined by contact conditions; the endgame requires the concavity of the functional Q on triples of convex bodies. The definitions are engineered to be self-contained — plain real arithmetic for inner products, rotations, and neighborhoods — so that the labor concentrates on the geometry rather than on API friction. Individual milestones are of moderate difficulty; the goal requires assembling all of them, which is the source's own achievement.
Every item quantifies only over the objects it needs — hallways, shapes, rotation paths, angle sets, segment families; no item carries a vacuous hypothesis: moving sofas, monotone sofas, polygon intersections, and Gerver sofas all exist, and the inequalities are in the intended directions. The fragment excludes the explicit trigonometric formulas of Gerver's curves (the goal needs only their structural characterization), the source's sections on the ambidextrous sofa and non-convex generalizations, the computer-search evidence for the sofa constant's decimals, and any statement about shapes that are not moving sofas. Nothing in the mission asserts the uniqueness of the Gerver sofa or the value of the sofa constant as a decimal; it formalizes what the source proves — optimality.
How many ways can a closed orientable surface of genus be "coloured" by a finite group ? Precisely: how many group homomorphisms are there? The answer is the partition function of two-dimensional Dijkgraaf–Witten theory with gauge group . That theory is the simplest topological quantum field theory (TQFT) in the sense of Atiyah and Segal, and the standard test case for gauge theory with a finite gauge group (Dijkgraaf–Witten 1990, Freed–Quinn 1993). The count has a closed form in terms of the dimensions of the irreducible representations of alone. It is known as Mednykh's formula.
Timeline. Frobenius (1896) counted pairs with a prescribed commutator, , in terms of characters, which is the genus-one case. Frobenius and Schur (1906) treated the non-orientable analogue. Mednykh (1978) proved the formula for every genus using character theory and the standard presentation of . It was rediscovered in physics as the partition function of 2D and 3D finite-gauge-group TQFTs (Freed–Quinn 1993), and reproved with matrix integrals (Mulase–Yu 2005) and with lattice TQFTs (Snyder 2007). The last paper fixes the form of the statement used here.
Let be a finite group. A surface tuple of genus in is a family . Its commutator product is
multiplied left to right. For let (commCount G g z). The surface group (SurfaceGroup g) is the presented group
the standard presentation of the fundamental group of the closed orientable surface of genus , whose Euler characteristic is .
A complete irreducible family (IrrepFamily G ι) is a finite family of finite-dimensional complex representations of that are irreducible, pairwise non-isomorphic, and such that every irreducible finite-dimensional complex representation is isomorphic to some . Write and for the character.
For every finite group , every complete irreducible family and every ,
which is Mulase–Yu, Thm. 1.1 and Snyder, eq. (1) with . Equivalently, . Exponents are integers: at the formula reads .
The milestones follow the algebraic proof of the counting formula recorded in Mulase–Yu 2002, §4, which goes back to Frobenius and Mednykh. Write for the convolution of functions on .
The result. The formula says that the number of -coloured genus- surfaces is a function of the multiset of irreducible dimensions alone. Two groups with the same character degrees (for example and , both with degrees ) have equally many homomorphisms from every surface group, even though the groups are not isomorphic. In TQFT language the left side is the evaluation of the Frobenius algebra , where is its handle element. The right side is the gauge-theoretic state sum. The identity is the two-dimensional instance of the agreement between the Atiyah–Segal gluing description and the path-integral description of a TQFT. It also gives the volume of the moduli space of flat -bundles on , and it underlies counts of covering spaces of surfaces.
Formalizing it. The theorem is classical and fully proved; to our knowledge it has no machine-checked proof. Mathlib has characters of finite-dimensional representations, their orthonormality (FDRep.char_orthonormal) and Maschke's theorem. It lacks the completeness of irreducible characters, the column orthogonality relation (M2), and any statement linking class sums to characters (M3). These are reusable well beyond this mission. The mission also produces the first formal link between a surface-group presentation and representation theory.
The available orthogonality is the row relation between two irreducible characters. Every step here needs the column relation M2, . That relation is equivalent to the decomposition of the regular representation , and in particular to the finiteness and completeness of the irreducible family. Mathlib has no such decomposition. The convolution identity M4 must also be established in its non-isomorphic case, which the row relation alone does not give in convolution form. The passage from to tuples (M1) depends on the universal property of PresentedGroup and on using one ordering of the commutator product throughout. A proof that bypasses characters by brute counting is not available for general .
All representations are over : FDRep ℂ G with G : Type a Group with [Fintype G]. Characters are FDRep.character and is Module.finrank ℂ (V i). Counts are Nat.card. Powers with exponents depending on are integer powers (zpow) in , so is included and no natural-number truncation occurs. is PresentedGroup on generators Fin g × Bool, with , and the single relator (List.ofFn fun j => ⁅a_j, b_j⁆).prod. This is the standard presentation and stands in for , since Mathlib has no fundamental groups of closed surfaces. The goal quantifies over every complete irreducible family. M0 shows that such families exist, so the goal is not vacuous. Because the family must be complete and pairwise non-isomorphic, it cannot be chosen to make the sums trivial.
Out of scope: the non-orientable formula of Frobenius–Schur (it needs Frobenius–Schur indicators), positive characteristic, and the bordism-category formulation of TQFTs. Reusable contributions are especially welcome: the decomposition of the regular representation, column orthogonality, and the class-sum Schur lemma.
A seller deciding whether to offer two products separately or as one bundle also changes what customers need to learn before buying. A customer can know what a familiar product is worth to her while remaining uncertain about a new one. She may pay to inspect the new product, buy it without inspection, or leave. The seller's price can move customers between those choices. Wu, Jin and Chen study this interaction in a tractable two-product market and identify the exact search-cost threshold at which the preferred selling scheme changes (Wu, Jin and Chen, 2022, §§3–5). The question matters for pricing a new product alongside an established one when customers can buy from a description but can also spend effort learning whether the new product suits them.
A monopolist faces a unit mass of risk-neutral customers and has zero marginal production cost. Each customer values products 1 and 2 at independent uniform valuations . Product 1 is mature: its valuation is already known to that customer. Product 2 is new: before search, the customer knows only that its valuation is uniform on , with mean . Searching product 2 reveals and costs . Search is non-obligatory: a customer can buy a new product without inspecting it. The model and the information available at each decision are specified in §3 of the working paper.
Under separate selling, the seller posts nonnegative prices and , and each product is purchased independently. The mature product sells when ; its revenue is . For the new product, buying without search gives expected payoff , searching gives , and leaving gives zero. If a customer searches, she buys only when the observed . Write for the resulting purchase probability, , and for total separate-selling revenue (§4).
Under pure bundling, the seller posts one nonnegative price for both products. A customer who knows compares leaving, buying immediately with expected payoff , and searching product 2 with expected payoff . After search she buys the bundle only when . Let be the probability of purchase after these choices, integrating over both independent uniform valuations, and let (eqs. (1)–(2), pp. 11–13).
The customer follows the paper's footnote-10 tie rule: when an immediate purchase and search have equal best payoff, she buys without search; otherwise she searches if its expected payoff is nonnegative and a valuation in the support can meet the price. If search and leaving tie at zero payoff beyond the support, she leaves. The rule matters at exact optimal prices. It also ensures a customer is counted once when the two demand segments printed in §5.2 overlap at .
The mission first identifies the optimal new-product and bundle revenues, including prices at which they are attained. The new-product maximum has three search-cost regimes: , , and . The bundle maximum likewise has three regimes, with boundaries and . These are the cases of Propositions 1 and 2, pp. 9–13, and form the central milestones. The mature product's optimal revenue is , attained at price .
The goal is the paper's Theorem 1, p. 15. Write for the maximum of over , and for the maximum of over . The theorem asserts that these maxima exist and
At , both revenues equal . The formal goal therefore also records the strict form, exactly when , under the standing assumption . It asserts no unique optimal price: the new product can have two optimal prices at .
The threshold gives an exact decision rule in this model: below it, bundling earns more; at it, the schemes tie; above it, separate selling earns more. It is a comparison of optimized revenues, after the seller chooses the best admissible price for each scheme, rather than a comparison at fixed prices. It also makes precise how the familiar product's known value changes the demand generated by searching for the new one (Theorem 1 and its discussion, pp. 15–16).
The paper gives the analytical results, but this mission targets machine-checked proofs of their formal statements. The development contributes a reusable payoff-based rule for non-obligatory search and a concrete uniform-valuation revenue model. It leaves the interval-integral demand definition in place so that deriving the piecewise optimal revenues remains genuine mathematical work. No proof of these results is included in the SSRN copy held for this mission; the supporting milestones are the results stated in its main text.
Search and purchase choices change discontinuously when a price crosses a payoff threshold. For a single new product the same choice is made by every customer, but under bundling the mature valuation sorts customers into buyers without search, searchers who may buy after observing , and nonbuyers. The bundle demand must integrate across these groups. Its maximizing price changes regime as moves through and (§5.2 and Figure 1, pp. 12–13). A fixed-price comparison cannot establish Theorem 1, because the best price itself depends on search cost and on the selling scheme.
Lean uses real prices and costs, with and every price restricted to be nonnegative. Uniform expectations are interval integrals over , and uniform tail probabilities are volumes intersected with that interval. Demand and revenue are built from the customer choice rule; optimal values are expressed as greatest elements of the image of the admissible price set. In particular, the goal does not substitute the closed formulas from Propositions 1 and 2 for those maxima. Such a substitution would reduce the intended economic comparison to arithmetic and leave the search model untested.
The formal choice rule implements footnote 10's immediate-purchase tie preference and selects leaving when zero-cost search could never result in a purchase. Bundle demand counts each customer once, including at , where the two weak-inequality demand segments in the printed text overlap. The mature and new valuations remain independent uniform variables; search reveals the new value only, and every search incurs cost . The real-valued interval integrals represent finite, bounded payoffs or bounded purchase probabilities, so their values are genuine expectations and probabilities rather than defaults for nonintegrable functions. No separate assumption of a unique maximizer is used. Contributions that establish the integral identities, measurable choice regions, piecewise demand formulas, and global optimality statements are within scope.
Spare parts for capital goods (aircraft, defence systems, industrial machinery) are slow-moving and expensive to stock, and an unplanned stock-out idles the equipment they serve. Industrial additive manufacturing (3D printing) lets a part be produced close to where it is used, with short lead times and small batches. An original equipment manufacturer (OEM) that owns the design can therefore sell an IP license to its buyers instead of the parts themselves, letting each buyer print locally through a third-party printing service provider. The US Army's directive on advanced manufacturing (Department of Defense 2019) and commercial digital-inventory platforms are examples of this practice.
Zhang, Westerweel, Basten and Song (MSOM 2022) model the OEM's choice of license terms when buyers decide rationally between the two channels. The license has two classical components from the licensing literature (Kamien and Tauman 1986): a fixed annual fee and a per-unit royalty. The paper's main finding is about a single standard license offered to buyers of different sizes. A positive royalty can then be optimal under symmetric information, and all three supply chain configurations arise: centralized, decentralized and hybrid.
There are buyers . Buyer has Poisson demand with annual rate . All buyers share a holding-cost rate and a safety factor .
Traditional channel. The buyer orders from the OEM at wholesale price , with fixed ordering cost and lead time . Its expected annual cost is
The OEM produces at unit cost and earns from this buyer.
Licensing channel. Under a license with fixed fee and royalty , the buyer prints at price , with fixed ordering cost and lead time . Its expected annual cost is
and the OEM earns from it.
Surplus and choice. The surplus of buyer is , and its maximum surplus is . The licensees are ; the others stay in the traditional channel. The OEM's profit is
For two buyers with and , two kinds of royalty matter. The maximum royalty fees solve . The equalizing royalty solves .
Let be the least upper bound of . In each of the three cases of Table 1, is the largest profit in that case's column:
Each listed license realizes its profit and channel selection. Row iv of Case I is reached only as a limit . Any license that leaves both buyers with negative surplus earns . The optimal value is nondecreasing in .
In the paper's order, the milestones are:
The result gives a closed characterization of the optimal standard license for two nonidentical buyers. Three features follow from it. A royalty-only or mixed license can beat a fixed fee, unlike the identical-buyer case. The larger buyer can be deliberately kept in the traditional channel. The OEM's optimal profit rises with the wholesale price. These are the paper's managerial conclusions about distributed 3D printing, and the numerical study in §5 builds on them.
The result is proved in the paper (appendix, pp. 2699–2701), with several steps described as straightforward and Cases II and III left to the reader. As far as is known, none of it has been formalized. A machine-checked proof would supply the omitted cases and pin down the boundary behaviour. On the boundary, two entries of Table 1's channel-selection column need strict inequalities that the table does not print. The formalization adds the platform's first IP-licensing model, built on closed-form inventory costs.
The surplus is an explicit function, but the optimization is over a two-dimensional license space. The licensee set changes discontinuously across the curves and . One might reduce the problem to comparing a handful of candidate licenses evaluated at their formulas. That reduction is exactly what has to be proved: every license must be shown to be dominated by one of the candidates, region by region. In one region the supremum is approached and never attained, so no maximizer exists. The single-crossing property behind depends on a sign of a mixed derivative that fails without . The final claim, monotonicity of in , must hold across changes of case as moves, while itself moves with .
Fin n. For two buyers, the paper's Buyer 1 is index 0 and Buyer 2 is index 1. All parameters are real.IsLUB), never through sSup, whose value on an unbounded set is a junk . The royalties , and are bound by their defining equations, not left free. "" means any license under which every buyer has negative surplus.An advertiser observes customer paths through a sequence of states and advertising actions, then wants to assign credit for a purchase to the actions that occurred. Giving the last action all the credit misses earlier interactions; dividing credit by the number of visits can overreward a repeated action. Credit should also reflect what would have happened under the baseline no-ad action. Singal, Besbes, Desir, Goyal, and Iyengar formulate these requirements in a Markov model and a cooperative game, then connect their counterfactual adjusted Shapley value to a path-based quantity (Singal et al., SSRN version, §§3–5).
The paper is a known research result, published in Management Science in 2022. This mission uses the authors' August 21, 2021 SSRN version, whose displayed equations and page numbers are the formalization's citation basis. Its objective is to formalize the paper's characterization theorem, together with the intermediate claims that identify what a coalition is worth and how the ordinary Shapley value treats a converting customer path.
The transient states are ; a customer eventually reaches either the absorbing conversion state or the absorbing quit state . The actions are , with action designated as the baseline no-ad action. A customer begins at state with probability . At state , the advertiser takes action with probability . The probabilities , , and govern the next transient state, conversion, and quitting. The initial and action distributions sum to one, each transition row sums to one, and all probabilities are nonnegative. The paper's absorption assumption says that every customer eventually converts or quits, starting from any transient state (§2.1, pp. 6–8).
A player is one state-action pair , and the player set is . To value a coalition , only its players keep their actions. Action probability assigned to a pair outside instead takes an artificial zero-value action that sends the customer to . If is the resulting transient-state transition matrix and its one-step conversion vector, the coalition value is the conversion probability . Conversion has value one, so there is no additional revenue parameter (§2.3, p. 9; §4.2, pp. 14–15).
The Shapley value averages the marginal value over coalitions that omit , weighted by . For the counterfactual adjusted Shapley value, or CASV, the baseline value is instead : the frequency assigned to is spent on the no-ad transition row, in addition to any existing no-ad frequency. Thus CASV compares an advertising action with its specified no-ad alternative (§4.2–4.3, pp. 15–16).
A path lists the state-action pairs encountered before quitting or conversion. Write for the number of distinct pairs, regardless of repetitions. The unique-uniform weight is when the path converts and contains , and zero otherwise. It rewards each distinct participating pair once (§3.3, p. 12; Proposition 1, p. 20).
The first target is Proposition 1, which identifies the ordinary Shapley value of the coalition game with the expected unique-uniform weight:
The mission goal is Theorem 2. Let be the counterfactual chain for . It characterizes CASV as a difference of two path expectations:
The milestone list also records display (6), the matrix and path forms of coalition value in Step 1 of the proof of Proposition 1, and the Step 3 carrier-game identity. These are the paper's intermediate statements, with the carrier-game fact linked to an already proved general Shapley theorem (pp. 16, 20–22).
Theorem 2 gives a path-based meaning to a value defined by averaging over coalitions. It separates the credit earned in the observed Markov chain from the credit that the same player identity would earn under a baseline no-ad transition. This distinction matters in the paper's Example 5: an ad and a no-ad action both guarantee conversion, so the ad receives zero counterfactual credit despite having ordinary Shapley value one (pp. 15–16, 20, 22).
The paper also develops estimation methods after the characterization, but those algorithms and their numerical performance are outside this mission. Formalizing the known theorem would supply a reusable connection among absorbing finite chains, coalition conversion games, and Shapley values. The linked general Shapley definition and carrier-game result are already available as platform content; the paper-specific model and theorem statements here remain draft formalization targets.
A coalition changes which state-action pairs can contribute to a path. The Shapley definition averages marginal coalition values, whereas a path expectation assigns a weight to a realized sequence, including sequences that revisit the same pair. Identifying these two descriptions requires accounting for the distinct set of players on every converting path. Counterfactual adjustment adds another chain whose player identities and action frequencies must align with the original model; simply removing or merging the player changes the quantity in Theorem 2 (proof of Proposition 1, p. 21; Appendix B, p. 46).
States and actions are Fin m and Fin n, so the paper's index is Lean index . The model designates a noAd action rather than assuming it is Lean index zero. Players are pairs in Fin m × Fin n; the ordinary Shapley value transports them to Fin (m*n) to reuse the published Shapley definition. The separate general action-chain definition contains the initial, action, and transition probabilities; the attribution model adds the no-ad action and the coalition game.
The Valid predicate states every distribution and row-sum condition. Absorbing states convergence of powers of the original averaged transient matrix to zero. Theorem 2 additionally assumes absorption of the counterfactual chain, because absorption of the original alone does not imply it. This makes the inverse in each coalition value represent the conversion probability under the paper's Assumption 1; a singular matrix's totalized Lean inverse must not supply a default answer.
The counterfactual chain keeps at frequency and as a player, while replacing its transition row by the no-ad row. This reading matches the counterfactual marginal displayed in Appendix B. Pairs outside a coalition take the artificial quit action; that action is never a player. Path expectation is a real tsum over finite converting paths, each weighted by its initial probability, action frequencies, transitions, and final conversion probability. Nonconverting paths contribute zero. The Shapley weight and the conversion value one are exactly the paper's constants. CASV is defined by display (5), and path expectation is defined independently, so Theorem 2 does not follow by unfolding a prearranged identity. Work on path summability, matrix-series convergence, coalition path expansions, and the connection to the general Shapley theorem is welcome.
A cryptocurrency launched through an initial coin offering is often sold before the platform it serves has users. Its value to a buyer then depends on who else buys: a token that gives access to a trading network is worth more when many households with large endowments join. Sockin and Xiong (preliminary draft, March 2018, later published in Management Science) build a tractable rational-expectations model of this complementarity, in which the price of the currency is pinned down jointly by households who buy memberships and by miners who supply them. The perfect-information benchmark of the paper, in which the platform fundamental and the mining-cost shock are publicly observed, already shows the central phenomenon: the market can have two self-confirming equilibria, one with a high price and broad adoption and one with a low price and narrow adoption, and they respond to fundamentals in opposite directions.
The model belongs to the literature on multiple equilibria from strategic complementarities (Morris and Shin 1998) and on search models of money (Kiyotaki and Wright 1993), applied to a market in which the supply side is a population of miners with heterogeneous costs.
There are two dates. A continuum of households has endowment exponents with , where is the platform fundamental. At a household is randomly matched with another; if both own the currency, they trade, and with Cobb–Douglas utility
the competitive allocation of the matched pair gives household the realized utility . A household that does not trade gets zero utility.
At each household decides whether to buy one unit of the currency at price . It buys exactly when its expected utility , the expectation over its partner's of on the event that the partner also buys, is at least . Miners have productivity with , receive a share of the proceeds, and mine exactly when . The developer keeps the share , so its revenue is times the mass of buyers. The ex ante utility is .
An equilibrium at is a measurable purchase set of endowment exponents and a price such that the households in are exactly those whose expected utility, computed with partners drawn from , is at least , and the -mass of equals the mass of miners who mine at . In the Lean development these are IsEquilibrium P A xi B price and equilibria P A xi, in the namespace CryptoMembership.PerfectInfo.
There is a threshold such that there are exactly two equilibria when , one when , and none when . Moreover:
The milestones follow the proof in Appendix A: the matched-pair allocation and utility of Proposition 1; the closed forms of and ; optimality of cutoff strategies; market clearing as equation (13); the reduction of equilibria to the roots of equation (15); the log-concave bell shape of the left side of (15); the two–one–none root count; and the opposite movement of the two roots as the right side falls.
Proposition 2 is the paper's characterization of adoption equilibria with observable fundamentals. It explains why a token market can sustain both a high-price, broad-adoption outcome and a low-price, narrow-adoption one, why the latter reacts perversely to good news about the platform, and why a platform below a fundamental threshold attracts no buyers at all. The later sections of the paper build the unobservable-fundamentals analysis on the same equation.
Formalizing it produces a complete, checked equilibrium analysis of a nonlinear rational-expectations model: the equilibrium is defined from optimization and market clearing over arbitrary measurable purchase sets, and the count of equilibria is stated as an exact trichotomy rather than "generically". As far as is known, no part of this paper has been formalized. The development also requires facts about the Gaussian distribution that are reusable elsewhere, notably strict log-concavity of the standard normal cdf and truncated Gaussian moment generating functions.
The reduction to a scalar equation is mechanical once one knows that equilibria are cutoff sets; that step must be proved for an arbitrary measurable purchase set rather than assumed, as the paper does when it announces the cutoff form as a conjecture on p. 15. The equilibrium count rests on strict log-concavity of , which is not in Mathlib, and on the tail behaviour of against an exponential. The comparative statics of are not a direct consequence of the root statics: depends on both the price and the cutoff, and its monotonicity in the low-price equilibrium has to be established without the sign error in the paper's own derivative computation.
All quantities are real. Normal laws are Mathlib's gaussianReal with variances and , and is the cdf of gaussianReal 0 1. The standing assumptions , , , are bundled in Params.Standing. Ties are broken as on the page: a household buys when expected utility equals the price, and a miner mines when its revenue equals its cost. The mining cost is as in (4); display (5) prints , which yields the same mass of miners. Prices are positive. Equilibria are counted with Set.encard over pairs (purchase set, price). The high- and low-price equilibria are the cutoff equilibria with the smallest and largest cutoff. "No household buys" is stated as "no equilibrium exists", since with a positive price the miner mass is positive and the empty purchase set cannot clear. Part 3 is stated as printed in the proposition, not as the proof's final display, which has the wrong sign for the low-price equilibrium.
The equilibrium is not defined as a root of equation (6): defining it that way would make part 1 empty. Purchase sets range over all measurable sets.
A complete development needs Gaussian integrals of exponentials over half-lines, strict log-concavity and tail limits of , and a two-root lemma for strictly log-concave functions vanishing at both ends. These are reusable beyond this mission. Contributions to any milestone, or to these Gaussian facts as separate lemmas, are welcome. The unobservable-fundamentals setting (Proposition 3) is not part of this mission.
Health insurers pay providers in one of a few ways, and the choice shapes what providers charge. Under variable payment (co-insurance) the patient pays a fixed fraction of the provider's price. Under reference pricing the insurer announces a cap for a procedure: the patient pays a fixed co-payment at any provider charging at most , and in addition the whole excess above at a provider charging more. The authors motivate their model with the California Public Employees' Retirement System's reference-pricing program for knee and hip replacement (Nassiri, Adida and Mamani, 2022).
S. Nassiri, E. Adida and H. Mamani (Reference pricing for healthcare services, M&SOM 24(2), 2022; author manuscript SSRN 3176280) model the two payment systems as price games between competing providers whose patients choose by a multinomial logit rule, and compare the resulting equilibria. Their first comparison, Proposition 5, is about provider prices. Variable payment leads to higher prices than reference pricing exactly when the patient cost share is below a provider-specific threshold. This mission formalizes that result and the equilibrium characterizations it rests on.
Two providers, , offer a procedure to patients. Provider has a non-price attribute , with . Both providers have nonnegative treatment cost , and every patient has price sensitivity . The alternative to treatment has utility . If the patient's out-of-pocket cost at provider is , provider 's market share is
where is the price vector. Provider 's profit is .
Under each system the two providers choose prices simultaneously, and an equilibrium is a pure Nash equilibrium of that game: no provider can raise its own profit by changing only its own price. Each system also carries a standing assumption on best responses. Assumption 1 says that, as the rival's price tends to infinity, the limit of provider 's share at its VP best response is at most . Assumption 2 is the same condition under RP.
Assume, in addition, that the co-payment is below the reference price, . Let be an RP equilibrium. For each provider there is such that, for every and every VP equilibrium ,
The threshold is only claimed to exist; it is not given by a formula, and the statement fixes no constant.
The result. Proposition 5 sorts the two payment systems by cost share. When patients bear a small share of the price, co-insurance leaves providers free to charge more than they would under a reference-price cap. Above the threshold, co-insurance disciplines prices more than the cap does. The paper's later comparisons build on this price comparison: patient out-of-pocket and utility (Proposition 6), provider profit (Proposition 7) and insurer cost (Proposition 8). The equilibrium characterizations, Theorems 1 and 2, are also what the paper's numerical study computes with. Proposition 2 is the formal statement of shadow pricing: value-based providers charge exactly the cap.
The formalization. The result has a published proof but no machine-checked one. The paper cites external equilibrium results, leaves several inequalities to "some algebra", and does not separately state continuity of the VP equilibrium price in (Nassiri, Adida and Mamani, Appendix D). A formal development pins down which hypotheses each step uses; the co-payment condition is one that the theorem's sentence omits. It also yields reusable facts about two-firm logit price competition.
The central difficulty is the comparison of equilibrium prices across two different games. Under RP, a provider's out-of-pocket charge changes formula at , and its equilibrium status depends on the rival's price. Both providers may be value-based, both may be non-value-based, or only provider 2 may be non-value-based. In the second case, each best-response price depends on the other provider's price, so separate comparisons of the two providers' first-order conditions are insufficient. The VP equilibrium price must also vary continuously with for the strict inequality to define a threshold; strict monotonicity alone does not establish that.
All quantities are real numbers. Providers are Fin 2, and index 0 is the paper's provider 1. Prices range over instead of the paper's . This does not change the equilibria: an equilibrium price earns positive profit, and any price at or below earns non-positive profit. Equilibrium is the published generic pure-Nash relation CarbonDoubleCount.Planner.IsPureNash, with every price set equal to . "Value-based" is read as , following Proposition 2. The standing assumptions are , , and (implicit in the paper), and . The nonnegative cost bound is needed: negative treatment cost can make VP equilibrium prices rise with , contradicting Lemma 2(a). Assumptions 1 and 2 are encoded as follows: best responses exist, and along every best-response selection the share converges, as the rival's price tends to infinity, to a limit of at most . The goal assumes Assumption 1 at every , and it adds , which the proof uses and without which the statement fails numerically. "As approaches 1" in the proof is read as the value at .
The goal is stated about the Nash equilibria of both games and quantifies over every VP equilibrium at every . A version about solutions of the first-order systems would bypass Theorems 1 and 2 and is not the target. Neither is "VP is higher for small and lower at ", which is only milestones 3 and 10.
A complete development needs: derivative and quasi-concavity facts for logit shares in one's own price; existence of an equilibrium in a two-player game with continuous, quasi-concave payoffs on compact price intervals; uniqueness for the logit first-order system; implicit-function continuity of the equilibrium in ; and the RP case analysis. The logit and quasi-concavity lemmas are reusable for any logit price competition model. Proofs of individual milestones, and alternative arguments, are welcome.
An advance market commitment (AMC) is a promise to pay for a product if it is developed and supplied. For vaccines intended for low-income countries, a donor may use an AMC to encourage a manufacturer to invest before demand is certain. The investment decision happens before the firm and donor negotiate actual purchases. This timing creates a hold-up problem: once capacity is sunk, the firm receives only its negotiated share of the benefit from using it. Kremer, Levin, and Snyder analyze which commitments change that incentive in Designing Advance Market Commitments for New Vaccines. This mission concerns their framework AMC, in which a donor puts money in an interest-bearing escrow fund that pays a subsidy per vaccine until exhausted.
The result is specific to a temporary subsidy and a monopoly firm. It explains why depositing money in an escrow can transfer value to the firm without raising its chosen capacity. The paper also studies perpetual subsidies, supply commitments, forcing contracts, competing firms, and products farther from development. Those are different designs or regimes; their results are outside this mission.
A country receives a flow health benefit when citizens per period receive a vaccine. The benefit starts at , increases, and is strictly concave; its marginal benefit tends to zero as output grows. A donor values this benefit at fraction and pays for the vaccine. Its inverse demand is , with choke price and demand curve at positive price . Production costs per vaccine per period. The firm pays before trade to install capacity , and can produce at most in any period. Everyone discounts future flows at rate ; write for the flow equivalent of unit capacity cost. The paper maintains , so the integrated benchmark invests positive capacity. These assumptions and the interpretation of the donor and firm are from the BFI working-paper version, §§2–3.
After investment, the firm and donor bargain over vaccine purchases. Either can block trade, so both threat payoffs are zero. Efficient Nash bargaining chooses the output plan that maximizes their discounted joint surplus, and the firm receives fraction of that surplus. The firm anticipates this bargain when it chooses capacity. Without an AMC, denote its equilibrium capacity by ; with integrated control, denote the optimum by . The paper's first two propositions identify these benchmarks:
Under the framework AMC, the donor fixes a subsidy and deposits in escrow before the firm chooses . The escrow earns interest at the same rate as the participants' discounting. A subsidy is paid for each vaccine during the AMC period. If output is and , the fund is exhausted at a finite time ; afterwards there is no subsidy. The bargain chooses both AMC-period output and tail output , each bounded by capacity. If , the subsidy is perpetual at that output and there is no tail period. This branch matters when evaluating capacities the firm could have chosen instead.
The core comparison is the paper's Proposition 3. For any framework AMC whose equilibrium subsidy is temporary,
The goal covers every qualifying equilibrium. It also asserts that the displayed candidate is an equilibrium whenever , so the claim cannot hold merely because no temporary-subsidy equilibrium exists. It fixes the policy terms but does not assume the firm's capacity or bargained outputs in advance.
The milestones establish the inverse-demand property (Lemma 1), the integrated and no-AMC benchmarks (Propositions 1–2), the fund accounting identity (6), the discounted joint-surplus identity (7), full capacity utilization in the temporary regime, and the firm's ex ante profit identity (8). The last identity identifies the fund's contribution as on that regime. Their statements and numbering follow the December 2020 BFI working paper, with printed pages 6 and 10–13 and Appendix A, pages 37–38.
Proposition 2 measures the capacity lost to hold-up when a firm cannot keep all returns to investment. Proposition 3 then shows that this particular escrow design does not repair that loss when its subsidy is temporary: the fund changes the firm's payoff level while leaving the capacity choice at the no-AMC benchmark. That conclusion helps distinguish an AMC's payment amount from its effect on investment incentives. The paper's other contract designs address separate policy questions and should not be inferred from this result.
The formalization produces a reusable discounted-flow definition and a concrete capacity-and-bargaining game with an interest-bearing escrow. The source result has a paper proof; the Lean theorems here are proposed proof obligations, with no machine-checked proofs claimed. A complete development would verify the inverse-demand construction, existence and uniqueness of the relevant maxima, the escrow integral, and equilibrium optimality on both finite and perpetual subsidy branches.
The firm's value cannot be calculated by assigning full output at the outset. Bargaining chooses output after capacity is installed, and using fewer vaccines during the AMC period lengthens the subsidy period. Thus the escrow duration changes with the bargained output. The simple capacity comparison from the no-AMC benchmark only becomes applicable after the output and fund identities have been established. Moreover, the firm's alternative capacities can cross from a finite subsidy period to a perpetual one, so a statement proved only for the candidate equilibrium branch does not settle its investment choice.
All amounts, times, and discounted values are real. Discounted flows are Lebesgue set integrals over positive time; an open interval represents the AMC period, with endpoint choices irrelevant to its integral. Demand is the real infimum of nonnegative quantities at which . Its value at nonpositive prices is a Lean default and is never used in a result. The firm's value is times the real supremum of feasible joint-surplus values minus ; feasible output intervals are nonempty for admissible capacities, and the intended values are bounded and attained. Capacity is chosen over .
The Lean benefit function is twice continuously differentiable on all of , extending the paper's half-line convention so derivatives at zero are unambiguous; its sign assumptions are only for . Output is constant within the AMC and tail periods, following the paper's equation (A8) reduction. “Temporary” means at equilibrium. The model separately represents a perpetual subsidy for deviations. The framework profit is defined from bargained joint surplus and its discounted flows; equation (8) is a theorem target, and output is a bargain choice rather than a fixed capacity value. These choices keep the formal goal about the paper's investment game.
The development needs real derivatives, inverse functions, concavity, filters for the bargaining-weight limits, Lebesgue integrals of exponential flows, real suprema on compact feasible boxes, and optimization over nonnegative capacities. The discounted-flow and capacity-game infrastructure can be reused in other procurement models. Contributions that establish these interfaces or close any listed milestone support the goal.
A manufacturer that sells through an independent retailer charges a wholesale price above cost, and the retailer then adds its own margin: the double marginalization problem of vertical contracting. Anand, Anupindi and Bassok (Management Science 2008) showed that in a two-period monopoly chain the retailer can blunt this by buying more than it sells in the first period and carrying the excess into the second. This strategic inventory makes the retailer less dependent on the manufacturer's next wholesale price, which forces that price down, and in their model both firms gain.
Li, Li and Chen (SSRN 3003887; Manufacturing & Service Operations Management, 2021) ask whether the conclusion survives when two such chains compete. Their answer is that strategic inventory still arises, but under fierce enough competition it hurts every firm. The mission formalizes that result.
There are two supply chains ; denotes the rival chain. Each consists of a manufacturer with zero production cost and an exclusive retailer. There are two periods . In period the demand for product is
where is retailer 's price and measures the intensity of chain-to-chain competition.
The game has four stages. In stage 1 each manufacturer sets a wholesale price . In stage 2 each retailer sets and orders enough to cover demand plus a carryover , held into period 2 at unit holding cost . In stage 3 each manufacturer sets . In stage 4 each retailer sets and orders whatever demand its carryover does not cover; unsold units are worthless.
Contracts are unobservable: firms of chain see neither , nor the orders of chain , nor . The equilibrium is a perfect Bayesian equilibrium with passive beliefs. At every history of its own chain, a firm keeps believing that the rival charges its equilibrium-path prices , and acts optimally given that belief and the continuation play of its own chain.
Two games are compared. In the SI game each chain may carry any . In the NI benchmark, "a manufacturer only delivers whatever its downstream retailer can sell", so . Manufacturer 's profit is . Retailer 's profit is its revenue minus its wholesale bills minus .
Let . There is with such that for every , every SI equilibrium and every NI equilibrium satisfy
and equilibria of both games exist. Conversely, if or , no strategic inventory is carried in any SI equilibrium. The goal leaves unspecified, as the paper does: it asserts the shape of the comparison, not a numerical threshold.
The result. Proposition 2 overturns the monopoly-chain conclusion. Carryover still lowers the second-period wholesale price, but under competition that lower price feeds a fiercer price war between the chains, and the gain from softened double marginalization is lost. Because contracts are unobservable, no chain can commit to holding no inventory, so the firms end up in a situation every one of them would prefer to avoid. Proposition 3 sharpens the point: near the threshold a higher holding cost raises every firm's profit. A carrying cost, normally a pure loss, here acts as a commitment device.
Formalizing it. The paper's proofs are in an online appendix, which is not part of the source; the equilibrium notion is named on p. 8 but not written out. A machine-checked proof would supply both. It would pin down the equilibrium concept: what a passive-beliefs perfect Bayesian equilibrium of a two-chain, four-stage game is. It would establish that Table 1 is the unique equilibrium outcome, including against asymmetric profiles. It would derive the retailer's SI profit, which the page does not print. None of these results has a machine-checked proof.
Each stage payoff is piecewise quadratic, with kinks where demand reaches zero and where carryover covers period-2 demand. Table 1 must be shown optimal against all deviations, not only local ones, at every off-path history of a chain: a retailer that deviates in its carryover changes its own manufacturer's second-period price, and that response has to be the equilibrium one there too. The tempting shortcut is to solve the first-order conditions of a symmetric profile and stop. It establishes neither global optimality nor that asymmetric equilibria share Table 1's outcome. The goal quantifies over every equilibrium of both games, so both are needed.
The model is a single definitions file, ChainCompSI.Backfire.Model. It has the following parts:
demand, and sales ;Hist and pure profiles Profile with one strategy per stage;IsEq θ h si E, where si : Fin 2 → Bool selects SI or NI per chain;w1, p1, inv, w2', p2', D1, D2;mfrProfit () and retProfit ().Chains are Fin 2, with rival 1 - i. All quantities are real.
The formalization commits to the following conventions, each disclosed in the items:
Every statement of the form "in equilibrium, …" also asserts that an equilibrium exists, so none holds vacuously. The goal is stated about equilibria of the games, not with Table 1's closed forms substituted. A version comparing the two columns' rational functions would be a lemma of the proof, not Proposition 2.
Not formalized:
si flag leaves room to pose it later;Contributions welcome:
Many service providers can infer how long a customer's request will take when the customer shares personal information. A customer who withholds that information may instead enter a queue as an unidentified request. Hu, Momot, and Wang study the resulting conflict between an individual's choice to disclose and the waiting times experienced by the whole customer population in a single-server system. Their comparison asks whether giving customers control over disclosure improves total customer surplus relative to a rule requiring full disclosure. The answer depends on which jobs the provider gives priority, even though the provider keeps the same priority order among identified and unidentified requests. Hu, Momot, and Wang, §3–4
The manuscript distinguishes shortest-processing-time priority (SPT), where the identified high-priority type has a shorter mean service time, from longest-processing-time priority (LPT), where it has a longer one. This distinction makes privacy control a queueing question as well as an information-choice question: withholding changes a request's priority class, so it changes waiting times for other customers. Theorem 1 gives the direction of the population-level comparison in both regimes. Hu, Momot, and Wang, Theorem 1, p. 15
Requests reach one server according to a Poisson process of rate . A request has type with probability and exponential mean service time , or type with probability and mean . The rate parameter is positive and differs from one. The average service rate of the combined population is , and stability requires . The manuscript also assumes a service reward at least , where is the cost per unit of time spent in the system. These are the parameters of the two-type service model. Hu, Momot, and Wang, §3.2, p. 8
Each customer chooses whether to disclose before observing the request type. If the fraction that discloses is , disclosed type- requests arrive at rate , disclosed type- requests at rate , and undisclosed requests at rate . The latter form a type- class with a mixture of the two service-time distributions. The server uses preemptive priority in the fixed order . For each class, , , and denote its mean time in the system, including service. The values are determined by the three-class formulas in Online Appendix A.1. Hu, Momot, and Wang, §3.3–3.4 and Online Appendix A.1
An infinitesimal customer compares the utility of disclosure, , with that of withholding, . The total customer surplus at population strategy is
An equilibrium disclosure probability is an endpoint supported by the appropriate strict utility comparison, or an interior point where the two utilities agree and their difference decreases nearby. The manuscript chooses the Pareto-dominant equilibrium when several exist. Hu, Momot, and Wang, Eq. (1), p. 10; equilibrium definition, p. 12; Eq. (9), Online Appendix p. 3
Let and . The target is
When and , the corresponding inequality is strict. The first regime is SPT and the second is LPT: under the fixed ranking , type has the shorter mean service time exactly when . The comparison holds for any equilibrium satisfying the paper's equilibrium conditions, including its Pareto-dominant selection. Hu, Momot, and Wang, Theorem 1, p. 15
The mission includes Lemma 1's closed forms for and , the closed form of and the auxiliary function in the proof of Lemma 4, its derivative and denominator-sign statements, and Lemma 4's monotonicity of on . Those statements connect the queueing model to the social comparison without replacing the final claim by a special case. Hu, Momot, and Wang, Lemma 1, p. 12; Lemma 4, Online Appendix p. 3; proof of Lemma 4, Online Supplement p. 2
Theorem 1 identifies a precise direction for the welfare effect of control over request-type information in this model. Under SPT priority, giving customers control cannot raise total customer surplus above full disclosure; under LPT it cannot lower surplus below full disclosure. The result therefore ties the social effect of the same disclosure option to a service discipline and to the mix of request types. Its strict clauses identify when withholding produces a genuine difference rather than equality. Hu, Momot, and Wang, Theorem 1 and discussion, p. 15
The paper establishes the theorem and the supporting identities mathematically. Here the remaining task is to prove the Lean statements from the definitions of the queue's class parameters and mean times. The formal development can leave reusable algebraic interfaces for finite-class preemptive-priority queues and for checking stability and denominator conditions in rational queueing formulas. These definitions and statements currently compile as a local draft; they are not yet machine-checked proofs of the paper's results.
An individual disclosure choice moves a request between the middle priority class and one of the two extreme classes. The direct utility comparison does not by itself determine the direction of total surplus: each choice also changes the class workloads and the waiting times faced by other customers. Thus the endpoint comparison cannot be read off from the sign of at a single . The analysis must account for the full dependence of , , and , including the hyperexponential residual time of undisclosed requests. The algebra has several denominators whose sign matters, and a formula in the source proof has a boundary exception at . Hu, Momot, and Wang, Online Appendix A.1 and Online Supplement A.2
Lean represents rates, costs, rewards, waits, disclosure probabilities, utilities, and surplus as real numbers. A generic three-class preemptive-priority interface stores mean service times, mean residual times, and workloads. The paper-specific model supplies the H, N, and L table from Online Appendix A.1, including the undisclosed class's hyperexponential residual time. It treats the resulting mean waiting times as formulas; it does not construct a stochastic queueing process. Lemma 1 then asserts genuine algebraic identities from those formulas, rather than following immediately from the definitions. Hu, Momot, and Wang, Online Appendix A.1
The standing assumptions retain , , , , and from §3.2. They state , , and explicitly because these are rates and a marginal cost, and because zero values would erase the strict comparisons. The theorem items restrict to whenever using the waiting-time formulas. The auxiliary closed-form, derivative, and bracket items exclude , where the source's displayed second fraction is undefined as a real quotient. Lemma 4 and the goal include that parameter value. The derivative of is strictly negative on and equals zero at ; its strict decrease across the whole interval is stated separately. Hu, Momot, and Wang, §3.2 and Online Supplement A.2
Strict monotonicity of surplus requires , since a population with only one service type has no type-mix effect. The goal's strict clause requires ; at , a withholding equilibrium can have exactly the same surplus as full disclosure. The goal still quantifies over an equilibrium, rather than an arbitrary point of . Contributions toward the queueing identities, rational-function sign conditions, monotonicity, and final comparison all serve this scope.
Retailers that sell through both a website and physical stores must choose how many stores to operate and which products to stock in them. Product returns change that decision: a customer who is uncertain about a product may inspect it in a store instead of purchasing it online and later returning it. Gao, Agrawal, and Cui study this tradeoff in a model where stores are uniformly spaced and every store carries the same assortment. Their Proposition 1 gives a counterintuitive comparison: when the product return rate rises, the optimal number of stores falls, while the range of products in each store grows. The present source is the authors' manuscript generated on 2020-12-25, with the relevant result on its p. 12 and proofs in its Online Appendix pp. 1–2; the journal pages are not used here.
Let be a finite set of products. The retailer offers every product online and chooses a store count and a store assortment . Stores are evenly located on a circle of circumference one, and each carries . Product has a customer class of deterministic size . A fraction of this class is uninformed about its valuation. An uninformed customer dislikes the product with probability , the common return rate; a customer who dislikes an online purchase returns it. Informed customers know their valuations already.
The online hassle cost is , the return hassle cost is , and travel to a store costs per unit of distance. The retailer earns per-unit margin and pays for each return. Each carried product uses display area and inventory area proportional to store sales, with coefficient . A store also requires common area ; facility area costs per unit. These assumptions and the symmetric circular-city setting come from §§3.1–3.2 of the paper.
Let denote uninformed online demand. The paper's full-market-coverage assumption yields the four online and store demand functions in equations (5)–(6). One store has size from equation (8). The total expected profit is equation (9):
An optimal decision maximizes this profit over all and . The paper relaxes the integrality of on p. 11. The retailer prefers stores at rate if a decision with has strictly greater profit than the online-only decision. This reading distinguishes strict preference from a tie at the store-opening threshold.
For , suppose stores are strictly preferred at both rates. For any optimal decisions and , the goal is
and, when ,
The goal includes the proposition's parenthetical equivalence and its necessary conditions and . The size condition is evaluated at the larger rate, so it holds across the interval being compared.
Lemma 1 identifies a threshold for opening stores. Above it, the positive-store count is , and the profitable assortment is specified by the inequality printed in the lemma. The milestones also record the authors' profit decrease beyond this count and the zero-or-turning-point bound. Further draft items state the incremental profit of each carried product, the increasing positive-store profit gap, the monotonicity of the closed forms, and the optimal-store-size expression in the Online Appendix. These are statements from the source rather than new targets selected by analogy.
The result links return behavior to two costly retail decisions at once. Stores can reduce online returns by letting uncertain customers inspect products, yet a higher return rate need not call for more locations. Within the model, fewer locations can be paired with a broader assortment, and the stores can become larger when the return and online hassle costs satisfy the stated condition. Without Proposition 1, the model's demand and profit equations alone do not establish the direction of these comparative statics. The paper also studies other hassle-cost changes and omni-channel services, but they use additional results and models.
The theorem is proved in the authors' manuscript. The remaining task here is a machine-checked development of its exact model, threshold, and comparative statics. The compiled mission items are statements with open proofs; a successful compile does not prove them. The demand and profit definitions, together with the lemmas about maximizing a piecewise expression over a continuous store count, can be reused when formalizing the paper's other sections.
The objective changes formula when all uninformed customers near a carried product switch to stores, and again when informed customers do. Therefore differentiating one expression for profit across all does not justify a global optimum. At the store-opening threshold, the profit from stores can tie online-only profit; an interior count can then also be optimal. Product-selection ties can likewise produce more than one optimal assortment. A statement only about one selected closed form would not control every optimal decision and would miss the tie cases in Proposition 1.
Products form a finite type, possibly empty, and assortments are finite subsets. The empty catalogue has no positive-store preference; a one-product parameter instance witnesses that strict store preference is possible. All monetary quantities and the relaxed store count are real numbers. The return rate is quantified separately in so the same parameters can be compared at two rates. The bounds and spell out “fraction” and “handling cost” on pp. 6 and 9. No sign condition is imposed on the exogenous margins , which cancel from the decision comparison.
The source assumes sufficiently high customer valuations to guarantee full market coverage on p. 8. The Lean model begins with the resulting demand equations (5)–(6); it does not introduce valuations or prices from utility equations (1)–(4). The formulas retain and the area expression divided by ; at , Lean's zero-division convention gives zero store demand, while the total facility cost is multiplied by zero. The target always quantifies over actual profit maximizers. Proving only that decreases would leave the retailer's optimization claim untouched. Contributions to the source-backed milestones and the algebra connecting the two printed assortment criteria are in scope.
Many firms that run their own delivery or service workforce have started to operate a hybrid workforce: salaried employees serve part of the demand, while a crowd of independent freelancers on a platform owned by the same firm serves the rest. A firm in this position faces a recurring allocation question. Every order sent to the platform pays freelancers and so attracts more of them, which increases the platform's market thickness (the size of its freelancer pool) and with it the platform's own future demand. The same order, served in house, earns the firm's margin today. He and Goh study this trade-off between profit now and platform growth later, with data from the Vietnamese delivery company AhaMove (He & Goh, SSRN 3537700; published in Management Science, 2021, doi:10.1287/mnsc.2021.4177).
The question the mission formalizes is whether a thicker platform is worth having at all. The paper's answer, its Theorem 1, is that it depends on two numbers: the mean and, centrally, the variance of the cross-network effect , the random number of platform orders generated per freelancer.
Time runs over periods . At the start of a period the platform has freelancers and the firm faces orders. The firm chooses a transfer quantity with and sends those orders to the platform. Customers pay per order; an order served in house earns the firm , with . The platform also receives its own demand , where is random with . To serve the total load it pays freelancers the payout ratio , where measures the inefficiency of freelancers relative to employees. The period profit is .
The state then moves to
with parameters and shocks that are square integrable and independent, with . Future profits are discounted by . The value functions are and
Write , , and (which is when ). Inside the paper defines three disjoint regions: (high variance), ; (low variance), ; and (moderate variance), strictly between the two bounds. Market thickness benefits the system in period if is increasing in for every fixed , and is costly if it is decreasing; both in the weak sense.
and when . "Costly as " means that for every , is decreasing on some tail .
The appendix proves the theorem through a structural result and three lemmas, which are the milestones, in attack order:
The theorem replaces the intuition that a larger freelancer pool is always an asset with a criterion that a firm can estimate. When is very volatile, matching supply to a random platform demand is expensive, because the wage bill is quadratic in the load, and a thicker market only amplifies that cost; when is stable, thickness pays in every period. In the moderate regime the value of thickness changes sign once over the horizon, which is what drives the paper's later results on the structure of the optimal transfer policy (Proposition 3) and on the gap between the dynamic and the myopic policy (Theorem 2).
The result is proved in the paper. It has no machine-checked proof. Formalizing it adds a checked model of a finite-horizon stochastic dynamic program with a continuous two-dimensional state, concavity of value functions under partial maximization, envelope formulas with right derivatives, and an explicit backward recursion for the bound . The formalization also records two printed slips that it corrects (see Formalization scope).
The obvious argument is a backward induction on the sign of , read off the envelope formula (13). That step does not close by itself: the formula contains the optimal transfer , its multiplier and expectations of the next period's partial derivatives at random states, so the induction needs a priori bounds on the derivatives, monotone limits as and , and exchanges of limits with expectations. The value functions are only concave, so all derivatives are one-sided, and the optimal decision can sit on the constraint . Part (c) needs, in addition, an explicit lower bound on the asymptotic slope and a proof that switches sign at most once.
All statements share one definition, HybridOrderAlloc.Thickness.Model. The data are a structure Sys Ω (a measure on , shocks , real parameters and ) and a predicate Sys.Standing with the page's assumptions. Conventions committed to:
variance.MonotoneOn, AntitoneOn). is indexed by integers.Hypotheses added to the page, each disclosed in the statements: (Theorem 1 is false for , because then puts points where thickness pays into ); , , almost surely (so the next state stays in the domain of for every feasible , which the page takes for granted); ; and in Lemma 3(c) alone (the printed lemma fails for ).
is never a free parameter constrained by a Bellman hypothesis, and never a closed formula. Square integrability of is assumed, so no integral takes a junk value. The regions carry the guard wherever appears, so a divergent series cannot be read as .
A complete development needs: concavity of a partial maximum over a convex graph, one-sided envelope theorems, dominated convergence for the derivative limits, and finite geometric sums. The concavity and envelope steps are reusable for other dynamic programs with continuous states. Proofs of any milestone are welcome, as are sharper variants that remove the added well-posedness hypotheses.
A blockchain miner pays for electricity and equipment while block rewards arrive at irregular times. A strategy that raises the average reward can still expose a miner with limited capital to ruin before those rewards arrive. Albrecher and Goffard study this tension for a simplified selfish mining strategy in which the miner temporarily withholds a discovered block. Their model connects the block discovery process to a dual risk process: capital falls continuously as costs accrue and jumps upward when the miner collects block rewards. The quantity of interest is the miner's expected remaining capital at a random evaluation time, counting paths that have already reached ruin as zero. The paper derives a closed expression for this quantity when the miner begins with no withheld block. Albrecher and Goffard, arXiv:2010.12577v1, §§2–3.
Network blocks are discovered at Poisson rate . The miner has a share of computing power, pays operating costs at rate , and receives per block for which the strategy earns a reward. On each discovery, records whether the miner found the block. If the miner has produced a fork and another participant finds the next block, records whether that participant extends the miner's branch; its probability is .
The state just before discovery records an empty buffer, one withheld block, or a public fork. From state , the miner withholds a newly found block and earns nothing. From state , a further miner discovery pays for two blocks and returns to ; a competing discovery creates a fork. From , the next discovery resolves the fork and returns to . It pays two rewards if the miner finds the block, one reward if another miner extends the miner's branch, and no reward otherwise. These cases define the reward count and the surplus
where is initial capital and is the number of network discoveries by time . The ruin time is . For initial state , the fixed-horizon value is . The paper replaces a fixed horizon by an independent exponential time of mean and defines . Thus the exponential law has rate . Source, equations (15), (16), and (19).
The goal is Theorem 3.1 for the initially empty buffer. Let be the parameter expressions in the paper's equation (22). Let and be precisely the roots with negative real part of
For satisfying the corrected boundary system (23), the target is, for all ,
The paper prints the third right-hand side of (23) as . Its boundary condition (33), together with its own coefficients (24), requires . The mission states this correction explicitly. Source, Theorem 3.1 and equations (23), (24), (33).
The three curated targets are the corrected advanced differential system (29) for the three starting states; Lemma A.1, which counts three characteristic roots in the left half-plane when ; and the explicit function in (39)–(40), including its corrected boundary equations. These are statements made in Appendix A and used in the discussion of Theorem 3.1. The root-count lemma has the narrower hypothesis that the authors print; the main result permits and while specifying the root set. Source, Appendix A.
The formula gives expected remaining capital for a specific block-withholding policy while accounting for the event of ruin before the evaluation horizon. It allows the model's cost rate, reward size, hash share, connectivity, and initial reserve to be compared through the same value function. The result addresses the limited-capital question that an average revenue rate alone does not answer. Its use is within this simplified strategy and the paper's Poisson and independent-mark assumptions. Source, §§3–4.
The result is presented in the paper, but a machine-checked proof of this corrected statement is still to be supplied. A complete development would establish the expectation's measurability and integrability, the differential properties of the three state-dependent value functions, the complex root count, and the identification of the explicit function with the expectation. The stochastic model and its value function can also support separate formalizations of the paper's ruin-probability and honest-miner results.
The reward at a discovery depends on withheld-block state, so the surplus alone does not describe the next reward. The value functions for all three states are coupled, and the resulting differential equations evaluate the empty-buffer function at larger reserves and . Those advanced terms prevent a direct application of ordinary differential-equation uniqueness results. The root count is a statement about a transcendental complex equation, and its left-half-plane roots must be isolated exactly.
Appendix A says that it constructs a solution of the advanced equation and assumes uniqueness, observing that simulations can check the result. That assumption leaves an identification step between the displayed candidate and the stochastic expectation that the paper does not prove. It remains part of the goal, without an invented source milestone. Source, p. 25.
Lean represents the network process through independent exponential interarrival times of rate and independent Bernoulli marks. Marks begin at index zero in code, corresponding to the paper's first block at index one. The state transition and reward map encode the cases of (16). The ruin time is extended nonnegative, so an empty set of ruin times has infimum . On the null event of infinitely many arrivals in finite time, the cardinality-based block count has Lean's default value zero; the model law excludes that event almost surely.
The horizon average uses the first expression in (19), integrating against the exponential measure of rate . The expected surplus must be obtained from this stochastic construction; defining it by the closed formula or by a differential equation would erase the target. The roots and coefficients are constrained by the characteristic equation and corrected boundary system, and integral defaults on nonintegrable inputs cannot establish the result. No net-profit condition is imposed on Theorem 3.1.
The paper-specific definitions, the three curated milestones, and the main theorem are open to contributions. General infrastructure for marked Poisson processes, extended ruin times, integration of stopped surplus, and complex root counting would be reusable beyond this case. The four printed discrepancies affecting (23), (29), (31), and (40) are recorded in the local moderation notes; this mission's Lean statements use the mathematically corrected forms.
We investigate the possibility of dividing quantum channels into concatenations of other channels, thereby studying the semigroup structure of the set of completely-positive trace-preserving maps. We show the existence of 'indivisible' channels which can not be written as non-trivial products of other channels and study the set of 'infinitesimal divisible' channels which are elements of continuous completely positive evolutions. For qubit channels we obtain a complete characterization of the sets of indivisible and infinitesimal divisible channels. Moreover, we identify those channels which are solutions of time-dependent master equations for both positive and completely positive evolutions. For arbitrary finite dimension we prove a representation theorem for elements of continuous completely positive evolutions based on new results on determinants of quantum channels and Markovian approximations.
This mission is the statement-level formalization of Dividing Quantum Channels (arXiv:math-ph/0611057v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
23 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 16 (Structure of infinitesimal divisible channels) (Theorem 16 (Structure of infinitesimal divisible channels), PDF p. 14). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
This paper establishes several converse bounds on the private transmission capabilities of a quantum channel. The main conceptual development builds firmly on the notion of a private state, which is a powerful, uniquely quantum method for simplifying the tripartite picture of privacy involving local operations and public classical communication to a bipartite picture of quantum privacy involving local operations and classical communication. This approach has previously led to some of the strongest upper bounds on secret key rates, including the squashed entanglement and the relative entropy of entanglement. Here we use this approach along with a "privacy test" to establish a general meta-converse bound for private communication, which has a number of applications. The meta-converse allows for proving that any quantum channel's relative entropy of entanglement is a strong converse rate for private communication. For covariant channels, the meta-converse also leads to second-order expansions of relative entropy of entanglement bounds for private communication rates. For such channels, the bounds also apply to the private communication setting in which the sender and receiver are assisted by unlimited public classical communication, and as such, they are relevant for establishing various converse bounds for quantum key distribution protocols conducted over these channels. We find precise characterizations for several channels of interest and apply the methods to establish several converse bounds on the private transmission capabilities of all phase-insensitive bosonic channels.
This mission is the statement-level formalization of Converse bounds for private communication over quantum channels (arXiv:1602.08898v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Covariant channels admit a fixed Choi-state teleportation simulation (Proposition 2, PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
25 results of the paper are not stated yet, because the library lacks an interface they need: