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?
Improve the separation exponent between block sensitivity and sensitivity of total Boolean functions. This mission targets ; higher is better.
For every and every integer , the goal asks for a function with and . The shared definition SensitivityCampaign.AchievesExponent expresses exactly this requirement.
Using a finite certificate. Choose a total Boolean function , an input , and integers . Prove , , and , then apply SensitivityCampaign.finite_certificate. Here means block sensitivity at the chosen input. The shared theorem handles normalization and passage to arbitrarily large sensitivity. Its proof is a foundation milestone; a proof depending on an open milestone remains conditional until that milestone is proved.
Direct proofs of the asymptotic goal are equally welcome. Keep the shared definitions, replace the target value, and give your theorem a unique name. Use exact certified bounds; numerical estimates alone do not establish a record.
Background: the campaign proposal.
Digital platforms earn advertising revenue in proportion to the time users spend on them, and many of their design choices (infinite scroll, autoplay, notifications) raise engagement at the expense of the user's experience. Whether competition between platforms disciplines such addictive design or amplifies it is a question for competition policy and for the regulation of digital markets.
Ichihashi and Kim, Addictive Platforms (Bank of Canada Staff Working Paper 2022-16, 2022; Management Science, 2023) model platforms that compete for a consumer's attention by choosing how addictive to make their services. Without costs of addictiveness they find that competition hurts the consumer when attention is scarce and helps her when it is abundant (a separate mission formalizes that comparison). Section 5 of the paper asks what changes when raising addictiveness is costly, for instance because it requires investment in technology. Its answer, Proposition 5, is that the comparison then depends on the size of that cost rather than on the scarcity of attention: for high costs competition leads to more addictiveness and lower consumer welfare than joint-profit maximization would, whatever the attention cap.
There are platforms and one consumer. Each platform chooses an addictiveness and pays , with . The consumer observes , joins a set of platforms and allocates attention to each , subject to the attention cap , where . Her payoff is if she joins nothing and otherwise
Platform earns the attention it receives, if and otherwise, minus its cost .
The utility has the form : addictiveness lowers the utility of any given amount of attention but raises its marginal value. The primitives satisfy the paper's Assumptions 1–3: is strictly increasing and concave, strictly decreasing, and strictly increasing in ; the attention cost is strictly increasing, convex and twice differentiable with ; the cost of addictiveness is increasing, strictly convex and differentiable with and ; and with the inverse of , the product is weakly decreasing.
Two outcomes are compared.
Consumer surplus , respectively , is the consumer's payoff at the equilibrium, respectively at the joint-profit maximizing outcome.
For every and the equilibrium is unique, with all platforms at the same positive addictiveness, and a joint-profit maximizing outcome exists. For every , including , there is a such that for every
The threshold may depend on the cap and the primitives but not on .
Proposition 5 separates two forces. When addictiveness is cheap, the consumer's participation constraint pins down the outcome under joint-profit maximization, and the platforms push her payoff to zero; competition then helps her because she can leave one platform. When addictiveness is expensive, each platform's marginal trade-off between attention and cost determines its choice, and competing platforms, which take attention from one another, choose more addictiveness than they would jointly. The result implies Corollary 1: for the platforms gain from a collective cap on addictiveness, which bears on the debate about industry self-regulation.
The result is proved in the paper; to our knowledge none of it has been formalized. A machine-checked proof would cover a game with a continuum of strategies for every player, a consumer best response defined at every profile, a fixed-point characterization of equilibrium, and a threshold argument in the cost parameter. Appendix D's proof is short and leaves steps to the reader, among them that is increasing in and that each , not only consumer surplus, is lower under joint-profit maximization. A formal proof has to supply these steps.
The obvious argument is to compute both outcomes from first-order conditions and compare. Three steps of that argument do not go through as written. First, the consumer's allocation (A.6) is derived from an unconstrained first-order condition and fails when a platform is so addictive that its formula gives negative attention, so a platform's payoff away from symmetric profiles is not given by the closed form (A.10). Ruling out profitable deviations into that region needs a separate argument. Second, uniqueness of the equilibrium is claimed among all profiles, not only symmetric ones. Third, the "if and only if" requires the set of costs where the joint-profit outcome is better to be an interval closed at its left end, which in turn needs monotonicity and continuity of both consumer payoffs in across the switch between the participation regime and the marginal regime.
Platforms are Fin K (the paper's platform 1 is index 0) and the cap is an extended nonnegative real ℝ≥0∞. Derivatives of , and on are one-sided. The consumer strategy is a choice at every profile, and the equilibrium requires optimality at every nonnegative profile. Without that requirement any profile could be supported by a consumer who punishes deviations. The joint-profit outcome uses its own restricted consumer problem ("join all or none") and the consumer-favourable tie-break among profit-maximizing profiles. Without the tie-break, profiles below the participation level would also count as outcomes. No value function is written as a supremum: equilibrium objects are characterized through maximizers. "Lower", "higher" and "decreasing" are read weakly. The proof yields only weak inequalities on both sides of , and at the two outcomes can coincide.
The statement adds the following disclosed hypotheses to the paper's assumptions:
Lemma D.1 also carries an interiority hypothesis, that every coordinate of (A.6) is nonnegative, without which it is false. The goal also asserts that a joint-profit maximizing outcome exists, so that its comparison cannot hold vacuously. ranges over ; the proof's use of as a cost-free benchmark is not part of any statement.
The hypotheses are satisfiable. A sanity check, not part of the mission, verifies all of them in Lean for every on the instance
A complete development needs Karush–Kuhn–Tucker conditions for a concave program over a simplex-like set, implicit differentiation for , a monotone fixed-point argument for the best response, and continuity of maximizers in a parameter. These parts are reusable beyond this mission. Proofs of the milestones, partial results under the closed-form allocation, and checks of the statements on concrete instances are all welcome. The goal is Proposition 5. Propositions 1–4, 6 and 7, Corollary 1 and the side claims of Appendices E–F are not posed here.
In industries built on a key component sold by one dominant supplier, such as smartphone chipsets, the supplier's contract terms shape how much its downstream customers innovate. Some suppliers require their customers to cross-license their own patents to each other as a condition of buying the component, so that each manufacturer's innovation also improves its rival's product. Wang, Huang and Lee (SSRN 3053682; published in Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2019.0477) ask when a supplier facing two manufacturers of unequal innovation ability benefits from imposing cross-licensing. Their answer runs through the equilibrium of the manufacturers' innovation game, which is the subject of this mission: Proposition 2 describes how much each manufacturer innovates and shows that the supplier never ends up selling to a single manufacturer.
A supplier sells a component at wholesale price to manufacturers and . Manufacturer chooses a quality improvement at cost . With cross-licensing of effectiveness , the quality improvement of is (), and its inverse demand is . The standing assumptions are
so is the superior manufacturer. The game has three stages.
The proof of Proposition 2 defines two candidate profiles in closed form: the interior candidate , which solves both manufacturers' first-order conditions, and the boundary candidate , where invests exactly up to . A threshold separates them, and if , otherwise.
Under the standing assumptions:
Proposition 2 is the paper's equilibrium characterization. Proposition 3 is its instance (no cross-licensing), and Proposition 4 compares the supplier's equilibrium profits with and without cross-licensing on the closed forms , and established here. The economic content is that, under cross-licensing, the supplier always ends up selling to both manufacturers. When the superior manufacturer's cost advantage is large it caps its own innovation exactly where the supplier stops preferring a monopoly.
The paper's proof states the closed forms and asserts the checks ("one can obtain", "we verify"). This mission produces a machine-checked version: a complete definition of the three-stage game, with the supplier's price defined as an optimization rather than by its solution, and the equilibrium claims stated against that game. To our knowledge no part of this result has been formalized before.
The innovation payoff of the superior manufacturer is discontinuous. When moves just above , the supplier switches from a duopoly price to a monopoly price, and 's gross profit jumps down. A first-order argument therefore does not show that is an equilibrium. One must also show that never gains by moving into the monopoly region, and that never gains by deviating above , where itself becomes the potential monopolist. The boundary candidate is an equilibrium only because the supplier breaks its indifference at the boundary toward the duopoly.
Part 1 quantifies over every equilibrium, not only . The paper checks monopoly infeasibility only at , so the general case needs its own argument. The equilibrium is not unique: for some parameters a mirrored profile with at its own boundary is also an equilibrium. Uniqueness is therefore not claimed. The remaining steps are polynomial and rational inequalities in involving .
Standing β k1 k2.NNReal). Equilibria use the published two-player predicate CompetingChains.Cournot.IsPureNash.HasDerivAt … 0) of Lemma 1's duopoly polynomials, because the game payoff is not differentiable at the boundary.Real.sqrt 3. Every denominator is proved nonzero in its regime, never assumed.Two trivializing formalizations are ruled out. Equilibria are never defined by first-order conditions or by the closed forms, and the supplier's price is never defined by Lemma 1's case rule. Both are theorems here.
The source is the authors' SSRN manuscript (abstract 3053682, version of 2023-04-27); its proofs are in the appendix, pp. A.1–A.9. The paper's equivalent threshold is not formalized. Proofs of any milestone are welcome. Lemma 1 and display (2) are self-contained, and the closed-form milestones need only real-algebraic inequalities with .
A rare disease affects few patients, so a drug for it has a small market and its research and development (R&D) cost is spread over few sales. Governments respond with two kinds of subsidy: cost subsidies that pay part of the manufacturer's R&D bill (orphan drug programmes), and price subsidies that pay part of what each patient is charged. At the same time two practices change how drugs are priced and paid for. In some markets an independent consortium negotiates the price instead of the manufacturer, and some manufacturers offer outcome-based payment ("No Cure No Pay", as in a programme of Bristol-Myers Squibb), under which the patient pays only if the drug works.
W. Olsder, T. Martagan and C. S. Tang ask how a government with a fixed budget should divide it between the manufacturer and the patients under each pricing and payment regime. This mission formalizes their analysis of the regime with a consortium price and outcome-based payment, Setting (2B) of the paper, where the answer depends on the price: for a high price only patients should be subsidized, and for a low price only the manufacturer. The source is the SSRN working paper 3481150 (version of 2019-11-13); the article later appeared in Management Science (2023) with possibly different numbering, which is not used here.
The market has size one. A patient's valuation of an efficacious drug is uniform on . The model has three positive primitives: the R&D cost scale , the government's budget , and the unit price , which the consortium fixes and which lies in .
A best response to is a maximizer of over .
The Lean development names these objects IsPolicy, profit, BR, welfare, spend, IsOptimal and IsAlphaMax, in the namespace RareDisease.ExogOutcome.
For , , and as above:
then there is a such that is optimal and every optimal policy equals . Only patients are subsidized. 3. If
then is optimal, every optimal policy equals it, and
Only the manufacturer is subsidized.
The thresholds are the printed ones. They are not the sharpest possible (see Formalization scope), but they are what the paper states.
In attack order: the best response (19), ; the reduced problem (20), giving welfare and spending at the best response; the fact that both expressions of (20) are increasing in and in ; and the marginal-rate identity from the proof of Proposition 3 (Appendix C, p. 37), whose sign is that of .
The result splits the decision between subsidizing patients and subsidizing the manufacturer by a single comparison of the consortium's price with thresholds that depend only on the budget and the cost scale. For a policy maker the consequence is concrete. A high negotiated price already gives the manufacturer enough incentive to develop an efficacious drug, so every unit of budget should lower what patients pay. A low price leaves the manufacturer short of incentive, so every unit should go to R&D. Splitting the budget is never optimal in either regime.
The formalization adds three things. First, it checks a statement whose printed form has errors. Part 2 of the proposition, "subsidize both" for intermediate prices, is false as printed: , , lies in the printed middle range, yet the unique optimum is manufacturer-only. The printed closed form for the patient subsidy in part 1 does not satisfy the binding budget constraint. Second, the proof in the paper is a marginal argument along the binding curve, and its extremal step takes a maximum over at the wrong end; the parts posed here stay true because their thresholds are stronger than needed, which a machine-checked proof makes explicit. Third, the game is stated as a game: the government's problem is posed over the manufacturer's best-response set, not over the reduced formulas, so the reduction (19)–(20) is itself a theorem. None of these results has a machine-checked proof yet.
The reduced problem (20) is a two-variable optimization with a nonlinear constraint, and its feasible region has no simple shape. The obvious first idea is to solve the first-order conditions of the Lagrangian, but the optimum of parts 1 and 3 is on the boundary of the policy square ( or ), so stationarity says nothing there. What has to be shown instead is a global sign property along the whole binding curve: trading manufacturer subsidy for patient subsidy changes welfare per unit of spending with the sign of , and this sign must be controlled for every the curve passes through. That requires knowing that the curve stays in , which comes from the monotonicity of spending. Two existence and uniqueness questions also arise. In part 1 a patient-only policy must exhaust the budget with , which is where enters. In both parts no other policy may tie the optimum.
All quantities are real numbers. The standing assumptions , and are hypotheses of every theorem. The paper uses them without stating them: with and the demand is not positive and the manufacturer has no best response with ; the closed form of divides by . As in the paper, the efficacy ranges over all positive reals and is not bounded by . Policies satisfy , a half-open interval.
The added hypothesis in part 1 is necessary. With the spending tends to as , so for larger budgets no patient-only policy exhausts the budget. The thresholds and are posed as printed; replacing them by the sharper values and would be a different theorem. Part 2 and the printed closed form of part 1 are not posed, because both are false as printed.
The formalization cannot be trivialized by defining the government's problem through the reduced forms (20), because welfare and spending in IsOptimal are evaluated at members of the best-response set BR. "Optimal" means attained and compared against every policy at every best response, not a supremum. is defined as the greatest affordable manufacturer-only subsidy, not by its closed form, which is part of the goal.
A complete development needs only real analysis from Mathlib: maximization of a concave quadratic, monotonicity of rational functions, one-variable derivatives for the marginal-rate milestone, and Real.sqrt for the closed form. Proofs of any milestone are welcome.
Private equity funds are organized as limited partnerships. Limited partners (LPs: pension funds, endowments, insurers) commit capital, and a general partner (GP) manages the fund and calls the committed capital over several years. A well-documented empirical regularity is that some LPs earn persistently higher returns than others, and that fund returns persist across a GP's successive funds (Kaplan and Schoar, 2005; Lerner, Schoar and Wongsunwai, 2007). The usual explanation is differences in skill.
Maurin, Robinson and Strömberg propose a different channel. Because capital is called gradually, an LP hit by a liquidity shock may default on the remaining commitment. GPs who raise money from LPs that tolerate illiquidity can invest efficiently. GPs who raise money from LPs that do not must call capital early to protect themselves against default, which distorts investment. When illiquidity-tolerant capital is scarce, GPs compete for it and pay its owners a premium. This mission formalizes the paper's main equilibrium result without a secondary market: that premium exists exactly when both kinds of funds are raised.
An investment pays per unit on success and on failure. It succeeds with probability if the GP exerts effort and with probability if the GP shirks, in which case the GP enjoys a private benefit per unit invested. Each GP has wealth and runs one fund of total size . A share of the fund is invested in period 0 and the rest, , in period 1; both investments succeed or fail independently.
A fee schedule pays the GP a fee per unit of investment that depends on which investments succeeded. It must satisfy limited liability, the fund's cash flow, and incentive compatibility: effort on both investments must be at least as profitable for the GP as shirking on either or both. Write for the expected fee under effort. LPs who receive the promised expected return per unit contributed supply , which ties the fund size to the fee through
LPs consume in periods 1 and 2. With probability an aggregate liquidity shock hits in period 1. After the shock an LP discounts period-2 consumption by . There are two types, and , with , holding the shares and of the LPs' total capital . Without a secondary market an LP honours the second capital call only if the claim is worth at least its cost:
A GP chooses to maximize the profit subject to (3) and (4). LPs invest in private equity when its value exceeds the value of cash. An equilibrium (Definition 2) consists of the fractions of GPs raising each fund type, the returns , and optimal contracts such that GPs raise only profit-maximizing fund types and each primary market clears.
The key quantities are the LPs' break-even return , the minimal safe early call , and the tolerance threshold . The Lean development uses the namespace PELiquidity.Primary, with grossReturn, xHat, deltaHat, xLow, xBar, IsFeasibleContract, IsOptimalContract, IsCapitalSupply and IsEquilibrium.
There are thresholds
such that for every an equilibrium exists, and every equilibrium satisfies the following:
The thresholds are existential, as in the paper. A variant pinning by (C.3) is a welcome strengthening.
The result shows that heterogeneous liquidity needs alone, without any difference in skill, produce a cross-section of LP returns: when capital from liquidity-tolerant LPs is scarce, those LPs earn strictly more than other LPs investing in otherwise identical funds. When it is abundant, they earn only their fair liquidity premium. This separates a liquidity explanation of return persistence from a skill explanation, and it is the benchmark against which the paper's second main result, the effect of a secondary market (Proposition 3, a separate mission), is measured.
The paper proves the result by hand. No part of it has a machine-checked proof. A formalization would check the three-case equilibrium argument, including uniqueness, which the paper treats briefly. It would also fix the readings of Definition 2 that the printed statement leaves open (see below) and record the hypotheses the proofs use without stating. The fee-design lemma (Lemma 2) is a small linear program of independent interest for moral-hazard models with several projects.
The equilibrium statements quantify over every equilibrium, and an equilibrium includes an optimal contract for each fund type, optimal against all fee schedules, call shares and fund sizes. The obvious approach, substituting the closed-form fee (15) and the optimal call (17) into the profit function, does not suffice. Uniqueness requires showing that no other combination of returns, fund fractions and contracts clears both markets. That includes returns at which a fund type is not raised. It also includes returns above the break-even rate, where the no-default constraint loosens and the fee falls. Ruling these out needs the GP's optimal profit to be decreasing in the promised return even when the no-default constraint binds. The boundary at , where the -market just clears with every GP raising an -fund, has to be placed correctly.
Everything is built from Mathlib's real numbers and finite sums. The fee-schedule linear program (Lemma 2), the contract problem (Proposition 1) and the equilibrium predicate are reusable for the secondary-market mission of the same paper. Proofs of any milestone, and the pinned-threshold variant of the goal, are welcome.
Many service platforms set a price paid by customers and a wage paid to the providers who serve them. A platform may instead announce how much of each transaction's price it will pass to providers, then choose prices after both platforms have announced their shares. These are different games: a price change in the second game changes both customer demand and provider pay. Hu and Liu's study of precommitments in two-sided competition asks which timing gives platforms a more favorable equilibrium. This mission isolates their comparison between a commission precommitment and no commitment, Proposition 3(b) of the submitted manuscript. The authors' Online Appendix, included in that manuscript, contains the proofs.
The comparison is useful where a platform must choose a contract with providers before it can adjust customer prices. It is not enough to know that either side of the market is competitive: the answer changes as demand-side and supply-side competition intensities move relative to each other. The mission makes the claimed parameter regions precise and ties them to equilibria of the two games.
There are two platforms, indexed by , with rival . Platform posts a consumer price and a provider wage . Fix a potential market size . The demand substitution factor measures how a rival's price raises demand for platform . The supply substitution factor measures how a rival's wage draws providers away. The paper uses the positive part :
The number of completed matches is . Profit is . Unmatched consumers or providers generate no revenue. Keeping the positive parts matters when a platform chooses a price or wage that leaves one side of the market empty.
In mode P, both platforms choose their prices and wages simultaneously, and each can change its own price and wage together while its rival's choices stay fixed. In mode C, each platform first commits to a pay-out ratio . The provider then receives per match and the platform keeps of its price. After observing both ratios, the platforms choose prices. Their profit in this second stage is
A subgame-perfect equilibrium in mode C specifies a price equilibrium after every admissible pair of ratios and an initial pair of ratios that resists unilateral deviation when prices are chosen again. The mission compares symmetric commission equilibria to the positive-profit equilibrium of mode P. In the paper's platform preference ranking, means that mode gives each platform a weakly higher price and profit, and a weakly lower wage and matching quantity, than mode .
Lemma 1 gives the simultaneous price-and-wage outcome. Writing , its price, wage, matching quantity, and profit are
Lemma F.2 says that second-stage commission prices equate demand and supply. Lemma 4 characterizes the symmetric commission equilibrium by the radical in equation (7), its price , and its profit in equation (9). These are the three milestones. The radical is transcribed exactly in the Lean definition associated with equation (7).
The goal compares the two equilibrium outcomes using all four components of the platform preference ranking:
The two informal proximity phrases are expressed by the existence of positive thresholds, with the threshold allowed to depend on . At , both rankings can hold because the outcomes coincide. The goal also asserts that the equilibria being compared exist for every admissible parameter pair.
The result identifies when committing to a provider share yields a platform outcome that is preferable to choosing price and wage together. Its four-way comparison is stronger than a profit-only ranking: the associated prices, wages, and match counts all move in specified directions. It makes clear that the relative competition intensities on the two sides determine whether the timing of the provider contract helps or hurts platforms. Without the comparison, the closed-form equilibrium results for modes P and C would not say which contract timing platforms prefer.
The result is proved in the cited manuscript, with derivations in Online Appendix §F; it is not an open mathematical conjecture. The remaining work in this mission is a machine-checked Lean proof of the equilibrium statements and the parameter-region comparison. The development will also provide a reusable formal model of simultaneous and two-stage decisions in a two-sided market. No existing machine-checked proof of this particular comparison is identified in the local Prove2Me index.
A change in a commission ratio changes the wage at any given price, while the subsequent price decision changes both demand and the wage again. That coupling makes the comparison more delicate than ordering two prices by inspection. The commission equilibrium ratio contains a square root, and the ranking must establish the directions of four outcome quantities in several parameter regions. The apparent shortcut of comparing profits alone would leave three of Definition 1's required inequalities unresolved. The positive-part demand and supply functions also admit zero-match equilibria that complicate an unqualified uniqueness statement.
The Lean development uses real-valued prices and wages, two platforms indexed by Fin 2, and all unilateral deviations in the stated strategy sets. Market size is positive, both substitution factors lie in , and pay-out ratios lie in . The paper does not spell out the strategy sets; these choices preserve the derivations in §3 and Appendix §F. The no-commitment uniqueness statement is restricted to equilibria where both platforms profit, because the literal unrestricted claim has zero-profit counterexamples. A second-stage strategy in mode C selects an equilibrium with positive profits for both platforms whenever one exists. This condition prevents off-path zero-profit punishments from making the printed symmetric SPE claim false.
The goal quantifies over equilibria derived from the demand, supply, match, and profit functions. It does not define an outcome to equal the paper's closed form, and it asserts equilibrium existence so that its universal comparisons have content. The radical for is a named expression; Lemma 4, rather than its definition, establishes its equilibrium role. A full proof needs reasoning about unilateral deviations, positive-part functions, equilibrium existence and uniqueness, the radical expression, and real inequalities. The general Nash condition and the paper's market primitives are intended for reuse in other two-player platform games. Contributions addressing these foundations and any of the three cited milestones are within scope. Wage- and price-precommitment modes are outside this mission.
Reinforcement learning in a changing environment has a difficulty that is absent from a fixed Markov decision process: transition data gathered earlier may describe a different system from the one the decision maker currently faces. A learning algorithm therefore estimates transitions from a recent window of observations. The estimate comes with a confidence region, a set of transition laws consistent with the data at a chosen statistical radius. In the general nonstationary setting studied by Cheung, Simchi-Levi and Zhu, their algorithm widens this region to ensure that it can contain a model whose states remain readily reachable. Such a model is needed for the paper's dynamic regret analysis. Section 7 isolates a structural condition under which widening is unnecessary: every destination is reachable from every state with a uniformly positive one-step probability under a suitable action. Cheung, Simchi-Levi and Zhu, §7.
This mission formalizes Proposition 4 of that paper, the precise claim that the original, unwidened transition region contains a model with a controlled diameter. It is one of three separate missions for the paper. The result supports the paper's no-widening variant of its learning algorithm; it is not a claim that every model in the confidence region has small diameter. Cheung, Simchi-Levi and Zhu, Proposition 4.
There are finitely many states and, for each state , a nonempty finite set of permitted actions. At each time , the system has a reward and a probability distribution for the next state. The distribution may change with . A trajectory records the observed state , chosen action , and successor state at each time . These are the model primitives in §2.2. Cheung, Simchi-Levi and Zhu, pp. 6–7.
An episode begins at and uses a window of length . At time in that episode, counts how often the pair appears between and ; . The empirical row counts observed successors and divides by . The corresponding average true row averages the time-varying transition probabilities over the same visits. Both are zero vectors when there are no visits. Cheung, Simchi-Levi and Zhu, equations (3) and (5).
Write , so this is the number of allowed state-action pairs. At confidence level , the transition radius is . The region consists of probability vectors within distance of . Here means no widening. The estimation event bounds the distance between and by that radius for each allowed pair. Cheung, Simchi-Levi and Zhu, pp. 12, 14.
For a stationary transition model and policy , the hitting time counts transitions until the first arrival at after starting at . This includes the first return time when . Its diameter is . Infinite expectations are possible in the definition. Cheung, Simchi-Levi and Zhu, Definition 1.
Assumption 2 supplies and an allowed action for every ordered pair of states, fixed across time, such that for all . Conditional on , Proposition 4 says that for every time in the horizon there exists a transition model whose every allowed row belongs to and whose diameter obeys
The target is existential: the region need only contain one such model at each time. The milestone list follows the two cases in the proof of Lemma 13, the lemma's model existence claim, and the expected hitting-time bound in the proof of Proposition 4. Cheung, Simchi-Levi and Zhu, pp. 21, 49–50.
Proposition 4 identifies a condition under which the algorithm can use while retaining a uniform diameter guarantee for at least one plausible transition model. The paper uses this to analyze a no-widening version of its dynamic regret bound, and later applies that viewpoint to inventory control. Without a bounded-diameter model in the region, the diameter-dependent regret argument does not apply in the same form. Cheung, Simchi-Levi and Zhu, §7.
The proposition and its appendix proof are known results of the paper. This mission asks for a machine-checked account of the exact confidence region, its pathwise estimation event, Lemma 13, and the diameter claim. A general finite MDP with probability-valued transition rows is already available as the published FiniteMDPLearning definition; the paper-specific window estimators and its return-time diameter still need formal proofs. The paper's headline Theorems 1–4 are not posed here because their displayed bounds hide constants in notation. Cheung, Simchi-Levi and Zhu, p. 6 and Theorems 1–4.
The obvious idea that the true transition law belongs to the confidence region can fail under drift: the region is centered on recent observations, while the law at the current time may differ from the laws that generated those observations. Even the average true row has a special case. At an unvisited pair, equation (5) sets it to the zero vector, which is not a probability distribution and therefore is not a member of the simplex-valued confidence region. The existence claim must cover visited and unvisited pairs while preserving one-step reachability for all targets under a single transition law. Cheung, Simchi-Levi and Zhu, pp. 12, 49–50.
The diameter also uses the paper's first-arrival-after-start convention. A library travel time that is zero when source equals target misses the return-time cases and would weaken the stated conclusion. Cheung, Simchi-Levi and Zhu, Definition 1.
States and actions are Fin S and Fin A; permitted actions are state-dependent finite sets. Extra MDP rows for disallowed actions are never consulted. The finite MDP type supplies valid probability rows and bounded rewards. Hitting times and the diameter use extended nonnegative reals, so infinite values are represented without a default real value. The diameter ranges over allowed deterministic stationary policies and over all ordered state pairs, including equal pairs. Time is zero-based in Lean: paper time is index , and the paper's window becomes the half-open interval [τm-W,t). The paper's is at least one, so its estimators never divide by zero. A result at arbitrary with covers every episode time without assuming any additional episode schedule property.
The Lean statement makes two domain conditions explicit: and . These ensure the paper's claim that the radius at an unvisited pair is at least one; it can fail when and the confidence level is close to one. Assumption 2 is required for every time in the horizon, with . The event is the estimation inequality at the selected time. The paper writes it as membership of in a simplex-valued region for every pair, but that literal wording is false at an unvisited pair because there. At visited pairs, the inequality and membership agree. This convention is disclosed in the definition item and keeps the theorem meaningful on ordinary early trajectories.
The region is centered at the exact empirical , uses , and constrains every allowed row of the constructed model. The diameter uses its full extended-real value, and is strictly positive; dropping any of these clauses would change the claim. Reusable contributions include finite-state hitting-time estimates and windowed transition estimation identities. Proofs of the four milestones and the goal, as well as small lemmas connecting the published MDP measure to successive transition rows, are welcome.
After a sudden-onset disaster, humanitarian organizations (HOs) raise most of their response budget from private donors within days. Donors increasingly earmark their gifts, restricting them to a region, a program or a type of expense. Earmarking makes an appeal more attractive to a donor but lowers the share of each dollar that the HO can deploy immediately. Aflaki and Pedraza-Martinez (SSRN 3705595, published in Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2023.1202) model how HOs set earmarking and fundraising effort under three institutional arrangements: competition, full collaboration (a coalition that fundraises and decides as one), and partial collaboration, in which HOs pool the cost of reaching donors on a common platform while each donor still chooses which HO to give to. Joint appeals such as the UK's Disasters Emergency Committee are of the last kind.
This mission formalizes the paper's equilibrium result for partial collaboration (Proposition 4): equilibria exist, equilibrium earmarking is determined by first-order conditions that do not involve the efforts, and only the HOs with the largest required funding relative to their unit performance pay for the platform, while the others free-ride.
There are HOs . HO chooses a base utility , the attractiveness to donors that its earmarking level induces, and an effort , the fraction of donors it pays to contact, at cost . Its unit performance is the fraction of each donated dollar usable now, and is its required funding. The mean donation is normalized to .
Pooled effort reaches donors. A contacted donor gives to HO with the multinomial-logit probability
the being the option of not donating, so HO expects donations and achieves total performance , of which only is useful. HO is lexicographic (problem (10)): given the other HOs' strategies, it first minimizes its funding gap over ; among the gap minimizers it maximizes its utility ; and an HO that is still indifferent picks a strategy maximizing its unconstrained total performance . A Nash equilibrium is a profile in the product of the boxes at which every HO's strategy is such a best response. Finally,
is the reach HO needs to close its own gap.
A pure Nash equilibrium exists. For every profile in the box, labelled so that , with : is an equilibrium if and only if (i) for every there are with
and (ii) and .
The proposition separates the two decisions. Equilibrium earmarking solves each HO's own first-order condition (11) and does not depend on anyone's effort, because the pooled reach multiplies every HO's donations by the same factor. Equilibrium effort is a pure coordination outcome: the platform is funded exactly up to the largest required reach , and only the HOs attaining it contribute. The paper uses these facts to compare earmarking and performance across the three arrangements (its Propositions 5 and 7), and the free-riding structure is what drives the comparison of partial collaboration with competition.
The result is proved in the paper's Online Supplement (pp. S13–S14). No machine-checked version exists. The mission asks for a Lean proof of the proposition as stated, with the equilibrium defined from the HOs' lexicographic problem rather than from its characterization; the effort-system milestones are self-contained statements about a piecewise-linear fixed-point system and are reusable for other pooled-contribution games.
The obvious argument, "each HO maximizes , and the rest is bookkeeping", skips the case analysis behind (S11). Whether HO 's gap can be closed depends on the others' efforts. When the others' pooled effort already covers HO 's requirement, HO 's gap and utility no longer depend on its base utility. Only the third, tie-breaking level of the best response then pins down, and without it (11) is false. The existence part needs a fixed point of the base-utility best-response map on ; when HO 's best response is not unique, that map is not even a function. In part (ii), the effort system is not a contraction, and the paper's proof by successive elimination of indices is informal.
HOs are Fin n with 0-based indices, so is the value at index 0, and [NeZero n] is assumed. Strategies are in base-utility coordinates: is a primitive function of , as in the paper's problem (10). The earmarking coordinates are not modelled. All definitions live in one Setting structure with a Standing predicate, which every theorem assumes:
is implicit in the paper; with all every base utility is an equilibrium strategy. Concavity of is used by the paper's proof. The HO problem (10) is printed with decision and cost . It is encoded with HO 's own effort and own cost , the reading used by the paper's proof and by part (ii). The paper's "without loss of generality" ordering is the hypothesis that is antitone in the index, and is the number of entries tied with the first; this gives when all tie. Partial derivatives are Mathlib deriv of . Every function differentiated is differentiable at the point by Standing. The pure-algebra milestones 3–4 use no game objects.
The equilibrium must not be defined by (S11) or (11); that would make the goal a tautology. The Setting defines it as the three-level lexicographic best response over the full strategy box, and (S11) is a milestone to be proved. A sorry-free check that the standing hypotheses hold for the paper's numerical primitives (, , , ) accompanies the draft.
A full development needs: KKT conditions for a differentiable concave function on a compact interval (including the degenerate interval ); log-concavity of the logistic share; a continuous-maximum (Berge-type) argument and Brouwer's fixed-point theorem on a product of intervals; and the algebra of the effort system. Contributions of the interval-KKT lemma and of the effort-system lemmas are welcome as separate theorems.
The source is the authors' SSRN version (abstract 3705595, dated December 2022); all proofs are in its Online Supplement, Section S3.
Platforms that rank content by engagement (time spent, items consumed) implicitly assume revealed preference: a user who stays longer is a user who is better off. Kleinberg, Mullainathan and Raghavan (arXiv:2202.11776, Management Science 2023, doi:10.1287/mnsc.2022.03683) model a user with inconsistent preferences, a forward-looking system 2 and an impulsive system 1, and show that engagement and utility can come apart. Because utility cannot be read off behavioural data, platforms also run post-session surveys. Section 5.1 of the paper asks what such surveys can reveal: if a survey gives an estimate of the utility of a session, does rise or fall with the session length , and what does that say about the content? Theorem 5.1 answers this in terms of two content parameters, the span and the moreishness .
A session proceeds in two phases (§2.1, pp. 5–7).
The Lean development names these objects geomLaw (the law , ), jointMass, condMeanTq (9) and condUtility (8), all in the namespace EngagementOpt.Survey. Write and
(phi), the function of the paper's (11) and Lemma D.1.
Assume , , and . For integer session lengths :
The goal is the conjunction of the five claims.
The theorem describes how span and moreishness affect the relation between survey utility and session length. When and , utility eventually increases; when , it eventually decreases. In the symmetric case , the sign is decided by against alone. These are conditional predictions for survey data, rather than a converse that identifies and from the sign by itself.
The result is proved in the paper; it has no machine-checked proof. Formalizing it checks the Bayes computation (9)–(10), including an arithmetico-geometric sum and a printed exponent slip on p. 20 ( for , harmless because it cancels), and the real-analytic Lemma D.1. It also makes explicit one hypothesis the printed theorem omits (below).
The closed form (10) needs the sum and care with in denominators. The main obstacle is that monotonicity is a statement about integer , while the natural tool, the derivative of the real extension, lives on real ; the integer statement must be recovered from bounds on over whole intervals, not at single points. Lemma D.1 is a two-level sign analysis of a function with a removable singularity at , and the two limits at and at are of L'Hôpital type. The obvious argument for 2(b), "", silently uses ; without it, since on , the claim fails.
jointMass.Real.log, Real.rpow, HasDerivAt, Filter.Tendsto and finite sums suffice. The inequality for is in Mathlib (Real.le_log_one_add_of_nonneg). Contributions of any milestone, of alternative discrete proofs of monotonicity that avoid the real extension, and of the full goal are welcome.Electric-vehicle makers such as NIO sell cars without the battery and lease the battery separately, a business model called Battery as a Service (BaaS). The leased battery can be swapped at a station in minutes, so a customer is not tied to one battery size: a driver who leases a small battery for the daily commute can rent a large one for a long holiday trip, and a driver who leases a large battery can downgrade for a while and pay less. Shi and Hu (M&SOM 2024, doi:10.1287/msom.2022.0587) ask whether such flexible battery leasing is good for all three parties at once: the manufacturer (profit), the customers (total cost) and the environment (total battery capacity that has to be produced). A business-model innovation of this kind is adopted only if it improves profit; it is defensible publicly only if it does not raise customer cost or the number of batteries in circulation. The paper's answer is a "win-win-win" region of parameters, and that result is the goal of this mission.
A manufacturer serves a unit mass of customers with two batteries. The low-capacity battery has range , lease rate and acquisition cost (normalizations). The high-capacity battery has range , lease rate and incremental acquisition cost . Driving a distance beyond the battery's range costs the customer the shortfall: a need served by range costs plus the lease rate.
Each customer has a regular need , known when choosing a primary battery, and a peak need with , independent of and learned later. A fraction of the time is regular usage, peak usage. The standing assumptions are , , and .
Simple leasing. The manufacturer sets ; each customer leases low capacity iff . With the low-capacity volume, the profit is , the total customer cost is the integral over of the cost each customer bears, and the total battery capacity is .
Flexible leasing. A two-period game. The manufacturer sets ; customers choose primary batteries anticipating the peak period; the manufacturer then sets an upgrade rate and a downgrade rate ; customers learn and choose whether to swap according to Table 1 of the paper (a low lessee pays after upgrading, a high lessee pays after downgrading). Upgrades in excess of downgrades must be met by buying extra high-capacity batteries. The peak-period objective is (1): , and the total profit is (2): . A flexible equilibrium is a lease rate with optimal peak rates, a lease volume that customers rationally expect, and a profit no other lease rate and continuation can beat. is the total expected cost of the customers' choices, and .
Write ; by Proposition 2 this is the cost at which the manufacturer stops buying extra batteries.
For , :
Lemma 1 and Proposition 1 (the benchmark), Lemma 2 (peak volumes), Lemma 3 (optimal peak rates), Lemma 4 (flexible lease volume), Proposition 2 in its first case (the flexible equilibrium for ), Proposition 4 near the corner (customer cost), and Proposition 5 in its first bullet (capacity is smaller iff and for an explicit ).
The result identifies conditions under which a pricing innovation helps the firm, its customers and the environment at the same time: a battery cost near and a high-capacity range close to the largest peak need. Flexible leasing reallocates high-capacity batteries from customers who do not need them in the peak period to customers who do, so fewer batteries have to be produced. But the manufacturer prices the up/downgrade options to extract the efficiency gain and may buy extra batteries, so lower customer cost and lower capacity are not automatic. Proposition 6 states where all three improvements coexist.
The paper proves its results by calculus on closed forms. Nothing here is machine-checked yet. A formalization adds three things. First, it derives the closed forms from the model itself (customer choices from Table 1, volumes as measures of customer sets, equilibria as maximizers), where the paper states them. Second, it settles which reading of "sufficiently close" and "sufficiently large" is true. Third, it records the regimes in which the intermediate lemmas hold, which the printed statements leave implicit.
The closed forms of Lemmas 1–4 are routine integrals of piecewise-linear functions. The difficulty is global optimality and the corner analysis.
The model is the paper's base model of §3–§4: flexible leasing introduced into an existing BaaS program with independent regular and peak needs. The extensions of §5 (correlated needs, range choice, launching with flexible leasing) and the numerical calibration (§4.1, Figures 2–5) are out of scope.
Representation. All parameters are real numbers. Expectations over are interval integrals divided by ; volumes of customers are Lebesgue measures of subsets of . Every volume, expected cost and equilibrium is defined from the model; the paper's closed forms are theorems, never definitions. Customers lease low when indifferent, upgrade on and downgrade on , following the proofs. The lease rate ranges over all of ; the paper's remark "we require " is not imposed, because the benchmark optimum can exceed 1. The peak rates range over the set , that the paper requires (p. 13). An equilibrium is optimal against every continuation at every lease rate.
Readings and added hypotheses.
What a complete development needs. Lebesgue measure of intervals, interval integrals of piecewise-linear functions, and maximization of concave quadratics with a kink. It also needs the kink-regime equilibrium on the side and continuity arguments at the corner. Lemmas 1–4 are reusable for any variant of the model, and proofs of the milestones in any order are welcome.
Start-ups that build a platform or a digital service increasingly raise their set-up capital by pre-selling tokens: claims on the future output of the service, redeemable once it exists. Between 2017 and 2019 such token offerings raised billions of dollars, and corporate finance asked whether a token is anything more than a disguised equity or debt claim. K. Malinova and A. Park (Tokenomics: When Tokens Beat Equity, SSRN 3286825, version of June 1, 2023; Management Science 2023) answer this in a stylized monopoly model. Without frictions, a well-designed token contract is equivalent to equity and to debt: all three leave the entrepreneur the project's full NPV (missions I–III of this series). With moral hazard, when the entrepreneur can influence demand through effort that investors cannot observe, the three instruments separate.
The question goes back to M. C. Jensen and W. H. Meckling (Theory of the firm, J. Financial Economics 3, 1976), who showed that outside equity dilutes the owner's incentive to exert effort, while debt, which leaves the owner the full upside above the repayment, dilutes it less. This mission formalizes where tokens sit in that ranking: strictly between debt and equity.
An entrepreneur needs a set-up cost and then produces a quantity at marginal cost against the linear inverse demand . The demand intercept is uniformly distributed on , and the expectation of a payoff is . Facing the realized , a monopolist produces and earns ; the project's NPV is .
Moral hazard. With effort the intercept is uniform on , without effort on , with . Effort costs the entrepreneur in value. It is chosen after the financing contract is signed and cannot be contracted upon. The project has positive NPV only with effort () and . Investors break even under effort, so every contract term is fixed by ; a project can be financed by an instrument when the break-even terms make effort the entrepreneur's best choice.
and the incentive constraint (27) compares under (minus ) and .
Write (19), (23) and (28).
Writing for the sets of parameters satisfying the standing assumptions at which equity, optimal tokens and debt can finance the project,
The two inclusions are universal statements; strictness is posed as the existence of separating parameter values.
The result places a new instrument in the classical ranking of financing by incentive strength. Under the optimal token contract the entrepreneur earns only from tokens issued beyond the pre-sale, so, like a debtor, she earns nothing in low-demand states; this makes effort more attractive than under equity. Because the break-even pre-sale is smaller in normalized terms than the break-even debt (), tokens still leave more of the low-demand upside to the entrepreneur than debt does, and debt remains strictly better. The separating instances show that neither inclusion is an artefact of the model's parametrization.
The paper proves the result by hand in Appendix A and illustrates it numerically in Appendix B; none of it has been machine-checked. The mission produces a checked version of the whole chain, including the two points where the printed statements need repair (Lemmas 6 and 7, see below), and a verified treatment of the two Appendix B instances, whose contract terms are roots of cubic equations rather than the rounded values printed.
Each step is elementary real analysis, and there are many of them. Three require care.
All objects are real functions of real parameters: the shared model (expect, pim, qm, npv, the debt and token payoffs, condition (16)) in TokenFinance.Debt, the financeability predicates and every theorem in TokenFinance.MoralHazard; there is no probability layer. Expectations are expect θ g, the interval integral over divided by , and every expectation in a definition is of a realized payoff: the closed forms (20), (24), (26), (29), (48) are theorems. This rules out the trivializing formalization in which the incentive constraints are written as their closed forms, which would turn Propositions 5–8 into algebra. Debt and token payoffs carry positive parts, so the paper's case split ("the moral hazard problem does not arise") is a theorem, not a definition.
Conventions committed to:
Needed infrastructure: interval integrals of piecewise polynomials, the intermediate value theorem and strict monotonicity for the break-even terms, and polynomial inequalities. A lemma computing of truncated quadratics is reusable across all four missions of the series. Proofs of any milestone, and of the Appendix B root bracketing, are welcome.
Firms can raise money before production by selling claims on future output. In the model of Malinova and Park, these claims are tokens: a buyer prepays for a quantity of the good, and the final contract also gives token holders a share of tokens issued after demand becomes known. The firm must choose how many tokens to pre-sell. A larger pre-sale brings in more finance but changes the allocation of later sales revenue. The paper identifies contract terms that preserve the firm's monopoly output choice and determines the pre-sale quantity by investors' break-even condition (Proposition 3, p. 24). Proposition 4 asks how that quantity responds when financing need, production cost, or expected demand changes. These comparative statics make the contract's financing response explicit rather than leaving the break-even equation as an isolated root.
An entrepreneur pays a set-up cost to launch production and then incurs a marginal cost per unit. After financing, a demand intercept is drawn uniformly from , where . At output , the inverse demand price is . Without financing distortions, the monopoly quantity is and its profit is . For a realized payoff , expectation means the average . The venture's net present value is , equal in this domain to (equation (3), p. 14).
Under the optimal token contract of Proposition 3, investors buy tokens at time zero, and token holders receive the fraction of new tokens issued when output exceeds the pre-sale. A refund rule applies when output falls below the pre-sale. The resulting positive break-even pre-sale size is determined by equation (16):
For a positive-NPV venture, this equation has one positive root, in (Appendix A, pp. 40–41). The mission treats the root as a solution of the equation, so statements about the optimal quantity apply to every value satisfying it.
Proposition 4, p. 25, asserts three strict directions. If denotes the unique positive root of (16), then, while both endpoint ventures have positive NPV,
Thus a larger set-up cost or marginal cost requires more pre-sold tokens, while a higher demand level requires fewer. The Lean goal compares arbitrary positive roots directly. It places the NPV condition at the higher cost in the second comparison and at the lower demand level in the third; these are the restrictive endpoints. The first comparison places it at the higher set-up cost.
The milestone list follows the Appendix A proof: existence and uniqueness of the root of (41); the negative derivative (42); the positive derivative (45); the negative derivative (46); and the derivative in of the expression in (46), equation (47). These are source claims, with their displayed constants retained. Equation (42) and equation (45) contain printing errors in the SSRN copy; the formal statements use the actual derivatives and the milestone quotes retain the printed text.
Proposition 3 establishes that the chosen token contract can finance a positive-NPV venture while keeping the efficient monopoly output. Proposition 4 then describes the contract's response to the model's three principal parameters. Its strict inequalities distinguish an actual response from a weak monotonicity claim that could allow the pre-sale to remain unchanged. The demand comparative static is economically specific: a higher raises the demand intercept on average, but the quantity of tokens needed to finance the same set-up cost falls.
The paper proves these results analytically. This mission seeks machine-checked proofs of the root comparison and its stated derivative milestones. A completed development would provide reusable results about parameter-dependent roots of rational functions, especially when the root is specified by a break-even condition rather than by an explicit formula. The current Lean files are compiled statements with proof placeholders; compilation does not establish the mathematical results.
Equation (16) is cubic in a quantity that also occurs in a denominator, so the root does not offer a convenient closed expression for direct comparison. The endpoint restrictions matter: the meaningful root lies strictly between zero and , and derivatives that have the desired sign in that interval need not keep the same sign outside it. In particular, the derivative in (42) reaches zero at the upper boundary. The demand derivative in (46) also vanishes at , making its strict sign in the interior a separate claim. A literal transcription of two printed derivatives would give incorrect equalities even though their intended sign conclusions survive. The formal development therefore needs both careful domain control and the corrected expressions.
The namespace TokenFinance.Statics represents all quantities as real functions. Uniform expectation is the interval integral divided by . Monopoly output and profit use max to encode zero production below cost. The common Setting definition file also records the equity and debt payoffs and the token contract's case split, following the series-wide model. The break-even condition is exactly the closed-form equation (16), while NPV remains the integral of realized monopoly profit minus . The goal assumes the paper's standing , , , and positive NPV, written as using equation (3). Derivative statements state their own regions and nonzero-denominator conditions. The token size is quantified over positive roots rather than chosen by an arbitrary selection function.
The root cannot be defined to have the claimed monotonicity, and the derivative signs cannot be inserted as hypotheses of the goal. The missing work includes real-variable derivative calculations, root existence and uniqueness on the economic interval, and the strict parameter comparisons. The secondary token market, redemption mechanics beyond the contract payoffs, bankruptcy costs, consumer welfare, and the paper's institutional discussion are outside this mission's scope.
A reinforcement-learning agent chooses actions while learning how those actions affect future states. In a stationary model, observations collected long ago remain relevant to the current transition law. In a nonstationary Markov decision process, rewards and transition probabilities may change at each round. Old observations can then bias an estimate even when the agent has collected many samples. The challenge is to keep learning from recent observations without becoming blind to actions that the agent has not tried recently. Cheung, Simchi-Levi and Zhu study this tension for finite-state average-reward learning and introduce confidence widening in their SWUCRL2-CW algorithm Cheung et al., §4.
The paper's broad regret theorems suppress constants inside asymptotic notation. Proposition 2 gives an explicit one-round inequality that exposes the roles of estimation error, temporal variation, confidence widening, and the diameter of a plausible transition model. This mission targets that proposition and the stated auxiliary results used around it Cheung et al., pp. 14, 38–41.
Let be a finite state set. Each state has a nonempty finite set of permitted actions. At round , taking action in state gives expected reward and moves to state with probability . The one-step variation is the greatest change over permitted pairs; is the corresponding greatest distance between transition rows. These definitions make no stationarity assumption Cheung et al., pp. 6, 33.
At the start of an episode, the algorithm counts visits to each pair in a recent window of length . It divides empirical sums by , where is the visit count. Thus an unvisited pair has estimated reward and transition vector equal to zero. Reward confidence sets lie in ; transition confidence sets lie in the probability simplex and use an radius enlarged by a nonnegative parameter . Write and for their respective radii. The algorithm chooses a stationary policy and an optimistic model, gain , and bias from extended value iteration Cheung et al., pp. 11–13.
The diameter of a transition model is the largest, over ordered source and target states, of the smallest expected number of transitions needed to reach the target under a stationary policy. Source equal to target means a return time after at least one transition. The round- optimal gain is the value of the stationary occupancy-measure linear program for with only permitted actions. From the window's first round through the round before , let and be the sums of the corresponding one-step variations Cheung et al., pp. 8, 14, 33.
The main target is Proposition 2. Condition on the local reward and transition estimation events at . Assume that the widened transition confidence sets contain every permitted row of an MDP of diameter at most . For a round in which , the target is
The five milestones are the paper's Lemmas 2–5 and displayed inequality (32): a dual-bias span bound, a drift estimate for window averages, bounded optimistic bias, optimism under drift, and a transition-value error bound. Their exact constants are part of the targets Cheung et al., pp. 33, 38–39.
Proposition 2 separates the per-round change in optimal gain from the cost of the current action. Its first term tracks changes in the optimistic bias along transitions; the other terms identify window drift, reward and transition estimation, and widening. This decomposition can be summed across episodes when analyzing the algorithm. The result has a concrete role even though the later horizon-wide theorem is given in asymptotic notation Cheung et al., pp. 14, 41.
The paper proves these claims mathematically. The mission asks for machine-checked proofs of the explicit statements and for reusable definitions of finite nonstationary MDP variation, window estimators, confidence sets, occupancy gain, and hitting-time diameter. The source's Theorems 1–4 are not posed here: their displayed bounds hide constants in and, in one case, use an unspecified failure probability Cheung et al., pp. 14–25. This proposal supplies statements for solvers; it does not claim that these new statements already have machine-checked proofs.
The current model need not resemble the model that generated every observation in the window. A direct stationary confidence argument cannot control the resulting temporal error. The challenge is especially visible at a pair with no recent visits: its comparison transition vector is zero, although a genuine transition row has total mass one. The paper's Lemma 3, read literally for every pair, fails in that case. The mission states its positive-count condition explicitly while keeping the proposition and the later optimism and transition milestones valid at unvisited pairs Cheung et al., pp. 12, 38–40.
There is a separate issue with the printed dual-bias lemma. Feasibility alone permits an arbitrarily large dual gain and does not force the asserted span bound. The mission adds to Lemma 2 and records the change for audit. The EVI output is represented by its selected-model membership, bias normalization, optimism, and near-optimality properties; this is the contract stated for the algorithm's output, rather than a formal execution of extended value iteration Cheung et al., pp. 13, 33, 35–36.
States and ambient actions are Fin S and Fin A; permitted actions are state-dependent finite subsets. The setup has , , , and a nonempty action set at each state. Time is zero-based in Lean, while the paper's rounds are one-based; in particular its is represented by . Counts and confidence sets are evaluated at the episode start. Variations continue up to the target round. The estimation events are assumed at the episode start, which is the only time used by these statements.
Hitting times and diameter take values in extended nonnegative reals, so an unreachable target does not acquire a false finite diameter. The diameter includes return times and minimizes over deterministic stationary policies. The confidence-radius product counts actual permitted pairs. At an unvisited pair, the comparison averages remain zero and ; the large confidence radii under the stated bounds are essential. The local transition event uses the error condition: literal membership of the zero comparison vector in a simplex would make the paper's event fail. The printed coordinatewise maxima in Property 1 imply the standard joint-distribution optimism condition used here. The free printed in the last radius of Proposition 2 means , as the proof's context confirms Cheung et al., pp. 12, 14, 36, 40–41.
Two milestones carry a pinned hypothesis because the printed statement is false without it: Lemma 2 assumes the dual gain satisfies (an arbitrary feasible can make the bias span exceed ), and Lemma 3 assumes the pair was visited in the episode-start window (at an unvisited pair the comparison averages are zero). Proposition 2 is stated for every round before the horizon at which the action is the episode policy's choice, which covers the rounds of episode ; the coefficient of is kept as printed.
The witness MDP has genuine probability rows in the widened sets and a diameter bound. The EVI tuple obeys both stated properties, and the chosen action obeys its policy. These conditions prevent an unconstrained bias, a spurious zero diameter, a confidence event at the wrong time, or a reward bound for an unrelated action. The published FiniteMDPLearning model supplies probability rows and rewards in ; its different travel-time convention is not substituted for the paper's diameter. Contributions to the MDP linear program, finite-state hitting times, window-average inequalities, and confidence-region geometry are all useful beyond this mission.
Same-day and on-demand delivery services (groceries, meals, parcels) must decide how to assign incoming orders to drivers. One option is flexible dispatching: any driver may serve any order in the service region. Another is districting: the region is cut into districts, one per driver, and each driver serves only the orders from their own district. Districting is easier to run, since drivers learn their territory, routes are short and responsibility is clear, but it gives up the flexibility of pooling. A basic question is when a districting policy loses nothing against the best flexible policy.
Carlsson, Liu, Salari and Yu (Operations Research 72(1), 2024; accepted manuscript SSRN 3915544) answer this in heavy traffic, the regime where the drivers are almost always busy. Their comparison point is the policy of Bertsimas and van Ryzin (1993), whose expected delivery time has an explicit leading-order formula in heavy traffic. Their Theorem 6 gives two integral conditions on a partition under which districting matches to first order.
Timeline.
A service region is compact and convex and contains a depot . Orders arrive at rate at random locations drawn from a demand density on , Lipschitz, with . There are identical vehicles with speed and capacity , and each order needs an on-site service of mean . The constant comes from the Beardwood–Halton–Hammersley theorem.
The workload factor of the fleet is
the long-run fraction of time a vehicle spends in on-site service and in travel to and from the depot. The system is stable when it is below , and heavy traffic is the limit in which it tends to from below, with only varying.
Theorem 3 of the paper (Bertsimas and van Ryzin) states that achieves
in heavy traffic. A policy is asymptotically optimal if in heavy traffic.
A region partitioning policy fixes a partition of and dedicates one vehicle to each . District then receives orders at rate with conditional density . Its vehicle runs the single-vehicle version of , so Theorem 3 with gives its delivery time . The policy's overall expected delivery time is .
If for every
and and every obey Theorem 3, then
These are the displayed steps of the printed proofs of Theorems 5 and 6 (pp. ec5–ec6):
The result. Theorem 6 turns a question about stochastic, dynamic routing into a static geometric condition: find a partition that gives every district a share of two measures, (local tour length) and (service plus round-trip load). The rest of the paper builds on this. It computes such partitions with convex pieces, bounds the loss when the shares are only approximately equal (Proposition 3, the subject of the companion mission), and tests the policy in simulation. The theorem also shows that the arrival rates need not be equal across districts. What has to be equal is the combined load.
Formalizing it. The result has a short pen-and-paper proof, and no machine-checked version exists. The mission records exactly which part of the argument is real analysis (integral identities over a partition, and how heavy-traffic limits pass to ratios) and which part is borrowed from Bertsimas and van Ryzin. It also gives the platform a first districting and continuous-approximation development. Its definitions (workload factor, Theorem 3's leading term, heavy-traffic filter, conditional subregion data) can be reused for other results in the continuous-approximation literature.
The algebra in the proof is simple once Theorem 3 is applied to each district with its own rate , density and one vehicle. The obstacle is in the limits. Theorem 3 for district holds along that district's heavy-traffic limit, where its own workload factor tends to , while asymptotic optimality is measured along the fleet's limit. These are different limits unless the second equitable condition makes the two workload factors equal as functions of . A tempting shortcut is to state the district hypothesis directly with the fleet's quantities, such as and the fleet's workload factor. That assumes milestones 2 and 3 and empties the theorem. Division also needs care: and the ratios have denominators that must be shown nonzero from the hypotheses, not assumed.
The plane is EuclideanSpace ℝ (Fin 2) with the Euclidean norm, and integrals are Bochner set integrals for Lebesgue measure. The definition file CarlssonPartition.Equitable.Setting contains:
Conventions:
Filter.comap (fun λ => workload) (𝓝[<] 1): the arrival rates along which the workload factor tends to from below. Every "" is a ratio tending to .Two formalizations would make the goal trivial and are ruled out: defining or as the leading-order formula, and writing the district hypothesis with fleet quantities or the fleet's filter. The verification development checks that the heavy-traffic filter is not the bottom filter whenever .
Welcome contributions: proofs of the milestones; a general lemma on averaging ratio limits under a probability vector; and finite additivity of set integrals over a.e.-disjoint partitions in the form used here.
Reinforcement learning in a changing environment needs a benchmark that remains meaningful when the transition law and rewards vary from round to round. For a stationary Markov decision process (MDP), the optimal long-run average reward is a standard benchmark. In a nonstationary MDP, summing those stationary optima across rounds is convenient, but it need not equal the best expected reward achievable over the whole horizon: today's action changes tomorrow's state. Cheung, Simchi-Levi and Zhu use Proposition 1 to quantify this gap in their analysis of nonstationary reinforcement learning (preprint, pp. 7–8). This mission formalizes that proposition and the explicit estimates in its proof.
The paper develops algorithms for MDPs with drifting rewards and transitions. Its oracle comparison is useful before any algorithm is chosen: it relates a sum of local, stationary benchmarks to the reward of every non-anticipatory policy, including policies that adapt to the observed trajectory. This separates a property of the environment from the performance of a learning rule. The paper was published in Management Science in 2023; this mission follows the numbered statements and pages of the authors' pinned arXiv preprint (Cheung et al., 2020, pp. 6–8).
A finite nonstationary MDP has a finite state set , a nonempty available-action set at each state , and a horizon of rounds. At round , taking action in state gives a stochastic reward with mean and moves to a new state according to the probability distribution . A non-anticipatory policy selects an allowed action using the current state and observations from previous rounds. The target concerns expected sums of the mean rewards, so the distributional shape of the reward noise does not enter its formula (preprint, §2.2, pp. 6–7).
The one-step reward variation is the largest value of over allowed state–action pairs. The transition variation is the largest distance between the corresponding transition distributions. Their variation budgets are and , exactly as in equation (1). The budgets are computed from the MDP sequence; they are not independent inputs to the theorem (preprint, p. 6, (1)).
For the stationary MDP at round , is its optimal long-run average reward. The mission represents it as the optimum of the paper's occupancy linear program (15), whose variables are nonnegative state–action occupancies, satisfy flow balance, and sum to one. A diameter bounds the least expected hitting time between any two states under an allowed stationary policy. The paper's Definition 1 includes equal initial and target states, so this includes a return time. Assumption 1 requires a finite diameter at every round; is a common bound on those diameters (preprint, pp. 7–8, Definition 1 and Assumption 1; p. 33, (15)).
Write . For and the necessary small-budget condition , the target is
for every initial state and every allowed non-anticipatory policy . Quantifying over every policy expresses the paper's maximum over policies without introducing a supremum over an unbounded real-valued function space. The first five targets follow Appendix A.2: a bounded optimal dual potential, the gain-drift inequality (18), the pathwise dual inequality (19), the window inequality (23), and the full-horizon inequality (24). Their constants and index ranges are part of the targets (preprint, pp. 8, 33–34).
The result gives a finite-horizon comparison between two different benchmarks. The sum of stationary gains is additive over time, while the best expected cumulative reward accounts for how actions alter later states. Proposition 1 says that their difference is controlled by variation and diameter under its hypotheses. This is the paper's justification for using the additive oracle in its dynamic-regret definition; the authors note that the later algorithmic bounds are larger than this comparison term (preprint, p. 8, text after Proposition 1).
The mathematical result is already claimed in the paper. This mission asks for a machine-checked version with explicit finite-horizon distributions, the occupancy LP, the diameter convention, and the drift sums. The new Lean statements currently have placeholders for their proofs; the imported finite-MDP definitions are already published. A completed development would provide reusable code for time-dependent MDP trajectory laws and for comparing stationary LP values as a model drifts. It would also make the precise domain of the square-root bound reviewable independently of the algorithms in the remainder of the paper.
The stationary gain is not a per-round reward guarantee. An action can collect reward now and put the process in a state whose future reward is poor, so summing stationary optima does not directly bound a nonstationary trajectory. Conversely, treating each round as an independent stationary experiment discards the state dependence that the policy exploits. The diameter controls the cost of that dependence, and variation controls changes between the stationary problems. The proof must connect these objects while preserving the exact factors , , and in Appendix A.2 (preprint, pp. 33–35).
There is also a small-budget obstruction in the printed Proposition 1. Its stated permits , where the displayed inequality is false: a two-state, one-action example with a slowly returning state, , and reward drift has an oracle sum near while the proposed lower bound on that sum is near . The mission therefore adds and records the difference from the page. Inequality (24), posed separately, retains the paper's every-integer-window form and needs no such pin.
States and actions are Fin S and Fin A; available actions form a nonempty Finset at each state, and . The imported FiniteMDPLearning structure supplies reward rows in and transition probability rows. It has rows for actions unavailable at a particular state; all mathematical maxima, LP constraints, policy restrictions, and drift formulas use only allowed pairs. The source's time is stored at Lean index . No value of the MDP sequence after the horizon enters a stated budget or reward sum.
The occupancy LP has a nonempty bounded feasible-value set under the standing MDP assumptions; its real supremum denotes . Hitting times and diameters use extended nonnegative reals to retain infinity, rather than silently converting an infinite hitting time to zero. The diameter includes same-state return times and minimizes over deterministic stationary policies; such policies attain the hitting-time minimum. The policy used for cumulative reward is a history-dependent randomized kernel on state–action histories. Conditioning an action rule that also observes past rewards on that history yields the same state–action trajectory law. The nonstationary measure samples the next state with the current round's transition law and is a probability measure.
The fixed is constrained to bound every round's diameter; it is not an unrelated parameter. The stated pin rules out the false small-budget case. In (23), the paper's last-window drift sum includes , which equation (1) does not define; the formal sum retains all defined terms through . The goal and milestones do not weaken , restrict the policy class to a convenient subclass, or omit a time step. Contributions on LP duality, finite-horizon trajectory expectations, hitting-time bounds, and drift inequalities are useful beyond this proposition. The paper's headline Theorems 1–4 are not posed here because their notation hides constants (preprint, p. 6, §2.1).
Blood platelets, fresh produce and many pharmaceuticals have a fixed lifetime: a unit not used within periods of its arrival must be discarded. Optimal ordering for such products depends on the whole age profile of the stock, and the dynamic program that describes it has an -dimensional state. It is intractable beyond small (Nahmias, 1982; Nandakumar & Morton, 1993), so practice relies on base-stock policies, which raise the total stock to a fixed level every period.
Bu, Gong and Chao (SSRN 3724966, accepted by Management Science, 2022) give the first performance guarantees for base-stock policies in this system. Under first-in-first-out (FIFO) issuance a heuristic base-stock level is asymptotically optimal in the lifetime, the demand population, the penalty cost and the outdating cost (missions 1–4 of this series). Under last-in-first-out (LIFO) issuance, which models a customer who picks the freshest unit from the shelf, a simple base-stock level is asymptotically optimal in the penalty cost and, when demand can be arbitrarily small, in the outdating cost (Theorem 5, mission 5). This mission formalizes the complementary negative result: when the demand is bounded away from zero, no base-stock policy is asymptotically optimal under LIFO as the outdating cost grows.
Demands are i.i.d. copies of a nonnegative random variable with and distribution function . The lower support is , and the newsvendor level is with .
The product has lifetime . At the start of period the state is , where is the stock with remaining lifetime at most ; the system starts empty. The firm orders , which arrives at once, raising the total stock to . Demand is served youngest stock first, unmet demand is lost, and stock reaching the end of its lifetime outdates. Under LIFO the outdated amount and the next state are
Each period costs with and . A policy is admissible if its order in period is a nonnegative measurable function of the current state. Its long-run average cost is , and . The base-stock policy orders , with cost . The subscript marks the outdating cost; , , and the demand law are fixed.
If and , then
where is the best base-stock cost. The goal asserts that both costs are finite, and that the limit exists and is strictly positive.
The proof also uses Lemma 3 (, p. 16) and inequality (EC.22) (p. ec8). Both are milestones of mission 5 of this series and are not restated here.
Proposition 1 marks the boundary of Theorem 5(c). Together they show that under LIFO, with a large outdating cost, base-stock policies are asymptotically optimal exactly in the trivial cases or , and when . In the remaining case some optimality gap persists however large is. Under FIFO the heuristic level is asymptotically optimal in without conditions (Theorem 4), so the result separates the two issuance rules: a manager facing fresh-first customers and costly waste should look beyond base-stock policies.
The result is proved in the paper; nothing in it is machine-checked. A formal proof would give the first verified statement about the long-run cost of a perishable inventory system. It would also produce reusable pieces: the LIFO recursion, the base-stock cost under LIFO, and a time-dependent policy whose cost can be computed exactly.
The obvious argument compares two limits. The limit of the best base-stock cost needs a lower bound valid for every base-stock level at once, and that bound must be uniform as changes. The lower bound of Lemma 3 controls the outdating only through , so the limit of its minimum has to be computed separately. The upper side cannot use a base-stock policy at all. It needs an explicit policy that is not stationary. That policy must be shown never to outdate along every demand path, and its periodic cost has to be bounded strictly below . The strictness needs the facts that and that , which is where and enter. A long-run average over a non-stationary policy is a of Cesàro means, and the step from per-period bounds to the average has to be made explicitly.
CappedBaseStock.DemandLaw: a probability law on with finite positive mean. The demand path carries the i.i.d. product law. The newsvendor cost and are backorderCost and newsvendorLevel of the published LostSalesOrderUpTo.Asymptotic.Backorder.Fin (m - 1) → ℝ with , so is allowed. Levels range over .The work needs a Cesàro-limit toolkit for -valued sequences, the LIFO sample-path recursion, and convexity facts for the newsvendor cost. Proofs of the milestones, and of the definitional sanity facts (, ), are welcome.
For every and every integer , there exists a total Boolean function with and .
The construction refines the tournament recursion of OpenAI/math. It keeps all four sensitivity profiles, sharpens the target-row count to fifteen, and bounds the gate contribution by separating the cases with and without a sink.
At depth , use tournament parameter , label alphabet , and disjoint OR copies. The proof obtains a finite seed and integers satisfying global sensitivity , block sensitivity at zero , and the exact integer comparison . This implies ; the shared finite-certificate theorem supplies arbitrarily large sensitivity and the campaign conclusion.
The shared campaign definitions are retained. The local proof was checked in Lean 4.33.1 with Mathlib 0df444a360eaa60ab8c11dca51a86af692955474. This draft targets a certified campaign improvement; no global optimality claim is made
A manufacturer that already sells directly to consumers may also supply an independent retailer. Adding the retailer can reach consumers who prefer its service, but the two channels then compete for some of the same buyers. A wholesale price affects both the retailer's ability to serve consumers and its retail pricing. The manufacturer's choice of distribution channel therefore depends on the pricing tools available to each firm. Jullien, Reisinger, and Rey study this choice when either or both firms can charge prices tailored to individual consumers in Personalized Pricing and Distribution Strategies. The source used here is their authors' manuscript of March 2022, whose proof of Proposition 3 appears in Online Appendix A.
This mission addresses a particular case of that analysis: the manufacturer charges a single retail price, while the retailer may charge either a single price or a price tailored to each buyer. The consumers' valuations for both channels move in the same direction with their type. Under those conditions, the paper claims that opening the retailer channel raises total industry profit under either retailer pricing policy. This is a question about the distribution decision, with the downstream retail game determining the profit achieved by each decision.
A consumer type is a real number in , with unit density. Firm A is the manufacturer and direct seller; firm B is an independent retailer that obtains each unit from A. Their values to a consumer are
There are no fixed costs of opening a channel and no variable production or distribution costs. The market parameters satisfy and . These conditions express the positively correlated case in §5 and keep the market large enough that its upper boundary does not limit B's demand. The two values cross at , with common value . Types below value A's offer more; types above it value B's offer more, until valuations fall to zero.
A two-part tariff has a fixed fee and a wholesale price per unit B buys from A. The fee divides profit between the firms. Total industry profit is what consumers pay, so cancels from that total. The wholesale price is nonnegative. At the wholesale stage, the firms compare the total industry profit attainable with both channels against the profit from A selling alone. As on p. 9 of the manuscript, a tie is resolved in favor of mono distribution; a strictly greater profit is required for dual distribution.
When A sells alone and charges a uniform price , its profit is times the measure of types for whom . If both firms charge uniform prices, denoted UU, they set and simultaneously. A consumer buys the product with highest nonnegative net utility. A earns on each of its retail sales and on each B sale. B earns on each of its sales. A downstream Nash equilibrium requires each price to maximize its firm's variable profit against the other price, including deviations into market regions where demand is zero or the identity of the preferred firm changes.
If A charges a uniform price and B tailors its price, denoted UP, A announces first. B then responds separately to each consumer. Under the continuation selected in the manuscript, B serves a type when exceeds both zero and A's nonnegative consumer surplus. Its price is . Otherwise, A sells if its price does not exceed the consumer's value. A chooses its uniform price to maximize its retail receipts plus wholesale receipts. Industry profit is the integral over of the price actually paid by each consumer.
The mono-distribution benchmark is
The paper derives a wholesale price and retail prices for the UU game, together with a profit satisfying
For UP it derives , A's leader price , and a profit . Equation (15) gives . The milestone list follows these source results, including the consumer demands and the two profit identities. Its last comparison completes the UP side after the UU gain is established.
The goal is Proposition 3: for each of UU and UP, some nonnegative wholesale price admits a downstream equilibrium and every equilibrium at that price yields industry profit strictly greater than A could earn with any uniform price in mono distribution. The goal leaves the wholesale price existential, as the proposition does. It does not assume the paper's calculated candidates are the only possible wholesale prices that work.
Proposition 3 identifies a robust distribution choice within the positively correlated case: while A uses uniform pricing, permitting the retailer channel raises joint profit whether B uses uniform or personalized retail prices. The conclusion separates the effect of B's pricing technology from the effect of A's own pricing technology; the latter changes the distribution comparison in Proposition 4 of the same manuscript. The result also supplies a precise instance in which additional downstream competition and additional market coverage must be assessed together.
The paper proves Proposition 3 in its Online Appendix A. The remaining work for this mission is a machine-checked derivation of the downstream equilibrium conditions, the demand and payment integrals, and the strict profit comparisons. The Lean statements here are open proof obligations. A complete development would make the consumer-choice and profit model reusable for related distribution games, while the rational formulas and equilibrium calculations are specific to this paper's linear valuations.
The paper writes simple linear demand expressions in the region where both firms have positive sales. Actual demands are measures of consumer choice sets and change formula at market boundaries, when a price excludes a product, or when all consumers refuse to buy. A first-order condition within one region does not by itself establish a global best response in the full retail game. The UU equilibrium milestone consequently states global Nash optimality and uniqueness at the selected wholesale price. In UP, A's leader price must likewise maximize its variable profit over every real uniform price after B's per-consumer response. The integral of actual payments must then be shown to equal the paper's closed form.
Lean represents consumer types by real numbers in and their mass by Lebesgue volume. The Model fields are ; Model.Standing records exactly and . The valuations and crossing point are defined from these fields. Retail demand is clipped to the consumer interval, and profit is calculated from demand or actual payments. The expressions printed as (12) and (14) are theorem conclusions, not definitions of industry profit. A real supremum is unnecessary for mono distribution: the theorem bounds profit at every price and proves attainment at .
The UP response uses the manuscript's selected personalized-pricing continuation. At indifference, the choice rules assign UU ties between the firms to A and give B a sale in UP only with a strict margin. Ties occur only at isolated types at the candidate equilibrium prices; zero-price deviations can create ties across the flat zero-valuation tail, and the rules specify their outcome. Global best responses quantify over all real retail prices, including zero and negative deviations. The goal restricts wholesale prices to , the range used in the manuscript's analysis. The fixed fee is omitted from the model because it transfers profit between firms without changing industry profit. The goal includes existence of a continuation equilibrium, so a vacuous universal statement over an empty equilibrium set cannot establish dual distribution.
The development needs elementary properties of Lebesgue measure on real intervals, measurable piecewise choice sets, interval integration, and algebraic inequalities for the rational candidate prices. Proofs of the equilibrium and integral milestones, or reusable lemmas about volumes of intervals cut by affine utility comparisons, are welcome contributions. The shared primitives are duplicated in the companion mission on personalized pricing by A because unpublished draft definitions cannot be imported across proposals.
source.pdf, SHA-256 25a6c84ac0c48c6720f6a9e1f9b1f1ec516412c31dac044ac84c1d4c72dfc253, printed pp. 5–14 and Online Appendix A, pp. 1–4.Blood platelets, fresh produce, dairy and many pharmaceuticals have a fixed shelf life: a unit that is not used within periods of its arrival must be discarded. Managing such products is a classical problem of inventory theory (Nahmias 1982, Operations Research 30(4), doi:10.1287/opre.30.4.680). The optimal ordering policy depends on the entire age profile of the stock, so it is computationally intractable beyond very short lifetimes, and practitioners use base-stock policies, which raise a single aggregate quantity to a fixed level every period.
Bu, Gong and Chao (SSRN 3724966, accepted manuscript, 2022; Management Science) give the first theoretical performance guarantees for base-stock policies in perishable systems. This mission covers §5 of the paper: the backlogging system with a positive replenishment lead time , where unmet demand waits and orders arrive periods after they are placed. Earlier missions of this series treat the zero-lead-time lost-sales system under FIFO issuance (missions 1–4) and under LIFO issuance (missions 5–6).
Demands are i.i.d. copies of a nonnegative random variable with . The product has lifetime , the lead time is , and the unit costs are (holding, per unit left over), (backlogging, per unit per period) and (outdating, in addition to holding). Throughout, .
In period the order placed in period arrives and serves backorders first. The firm then observes the state : for , is the on-hand stock with remaining lifetime at most minus the backorders, and for it adds the pipeline orders that arrive by period . The firm orders , which raises the inventory position to . Demand is served oldest-first (FIFO), the shortfall is backlogged, and with the outdated quantity the state moves by
The system starts empty. The cost of period is , where is the net on-hand inventory.
An admissible policy orders with each measurable. Its long-run average cost is , and . The base-stock policy orders ; its cost is . The heuristic level is any minimizer over of
For and every minimizer , the gap
(a) is at most for all lifetimes , with independent of ;
(b) if the one-period demand has the population form of (7), with and the moment assumptions of Theorem 2, is at most for all large , for every fixed lifetime ;
(c) tends to as , for every choice of minimizers.
Lemma 5 (p. 19): for and , , and is at most the same expression with replaced by . Proposition 4 (p. 23): for . Inequality (28) (p. 24):
Theorem 7 says that a policy computed from one convex function of one variable is nearly optimal for a control problem whose state has dimension , in three practically relevant regimes: long shelf life, high-volume demand, and expensive waste. The bound (28) is explicit and computable from the demand distribution, so it also certifies, for any given instance, how far can be from optimal. Lemma 5 gives two-sided bounds on the cost of every base-stock policy without solving for a stationary distribution of the age profile.
The paper proves Theorem 7 by sketch (§6.2: "We omit the details for brevity"), relying on the arguments for the zero-lead-time Theorems 1, 2 and 4. None of these results has a machine-checked proof. The mission's work is therefore to formalize the lead-time bookkeeping (EC.29)–(EC.33), the lower bound of Proposition 4 with its conditional-Jensen step, the convergence argument in each regime, and the omitted details of the sketch.
The lower bound on must hold for every admissible policy, including those that use the full age profile and the pipeline, whose optimal form is unknown. The obvious route, comparing with the non-perishable backlogging system where a base-stock policy is optimal (Karlin–Scarf), gives a lower bound that ignores outdating entirely and is too weak to make the gap vanish; outdating costs incurred by an arbitrary policy have to be accounted for, and the lead time means that units outdate up to periods after the order that created them. The standing assumption is exactly what keeps the coefficient of the outdating term in nonnegative. The upper bound requires the long-run cost of although the age-profile chain need not have a stationary law that is easy to describe.
In the limits, the heuristic level moves with the varying parameter. For (a), a uniform bound on in is needed; for (b), the newsvendor level of the compound demand grows with and concentration of is required (Scarf's bound and a Bernstein inequality in the zero-lead-time case); for (c), must be shown although the coefficient of (28) grows linearly in .
PerishBaseStock.Backlog. Demand laws, the i.i.d. path law, the lead-time sum law and the newsvendor expectations are imported from the published definitions CappedBaseStock_Model and LostSalesOrderUpTo.Asymptotic.Backorder.d t is .Fin (m + L - 1) → ℝ of cumulative levels; when it is empty and .ℝ≥0).Params.Standing; is an explicit hypothesis of Proposition 4, (28) and Theorem 7. Proposition 4 is formalized for FIFO issuance, the only issuance rule the paper specifies for this system.Trivializing formalizations are ruled out: is an infimum over all measurable state-feedback policies, not over base-stock policies; is the long-run average of the simulated cost; neither , , nor the demand law is fixed; and no gap is stated through a truncated subtraction or an infinite .
A complete development needs the long-run behaviour of the base-stock dynamics, conditional Jensen for policies adapted to past demand, exponential tail bounds for sums of i.i.d. demands, and, for (b), renewal-count moments and concentration. The sample-path lemmas (EC.29)–(EC.30) and Lemma 5 are reusable for other perishable models with lead times. Proofs of any milestone and of the individual parts (a), (b), (c) are welcome.
Blood platelets, fresh produce, bakery items and many pharmaceuticals have a fixed lifetime: a unit that is not used within periods of arrival must be discarded. Replenishing such a product is a classical problem of inventory theory (Nahmias 1982), and its optimal policy depends on the whole age profile of the stock, so it cannot be computed for realistic lifetimes. Practice therefore relies on base-stock policies, which raise total stock to a fixed level every period.
Bu, Gong and Chao give the first theoretical guarantees for such a policy. Under first-in-first-out (FIFO) issuance they choose the level by minimizing an explicit surrogate of the long-run cost and show that its optimality gap vanishes in four regimes. This mission is the fourth: a large unit outdating cost . The regime matters in practice because outdating is expensive. Slonim et al. (2014) put the component cost of a unit of blood sold to U.S. hospitals at about $570, and disposing of expired products often requires costly handling.
Demands are i.i.d. copies of a non-negative random variable with and distribution function . The product lives periods. At the start of period the state is , where is the stock with remaining lifetime at most . The firm orders , raising the total stock to (lead time zero). Demand is served oldest first and unmet demand is lost. The quantity outdates, and the state evolves by
The system starts empty. The period cost is
with holding cost , lost-sales penalty and outdating cost .
A policy is admissible if each period's order is a non-negative measurable function of the current state. Its long-run average cost is , and is the infimum of over admissible policies. The base-stock policy orders , and is its long-run average cost. The heuristic level is any minimizer over of
The lower support of demand is .
for every selection of minimizers, with , , and the demand law fixed. The statement holds for every demand law, whether is zero or positive.
The goal's proof also uses inequality (21), . That inequality, together with Lemmas 1–2 and Proposition 2 behind it, is posed in mission 1 of this series and is not restated here.
Theorem 4 says that when outdating is expensive, a policy computed from a one-dimensional convex function is as good as the optimal age-dependent policy. A base-stock policy does not need to track the age distribution, and its level can be found by simulation and golden-section search between explicit bounds. Together with Theorems 1–3 it shows that is asymptotically optimal in all four regimes of the paper. Remark 2 of the paper notes that the plain newsvendor level fails in this regime.
The result is proved in the paper (Management Science, 2022). It has not been formalized. This mission adds a machine-checked model of the FIFO perishable system with lost sales: the age-structured dynamics, admissible policies, long-run average costs and the optimal cost over all policies. The model is reusable for the other missions of the series and for the wider perishable-inventory literature. The paper's proof leaves several steps to the reader: the monotonicity of , the identity , and continuity of the newsvendor cost. Each of these becomes an explicit statement.
The obvious argument compares the heuristic with an optimal policy directly. That fails because the optimal policy has no tractable form. The proof instead goes through (21), a lower bound on obtained by a sample-path argument, and then has to show that the outdating term of the heuristic level vanishes faster than grows. That needs uniform control of as . The level must eventually fall into , where no stock survives periods of demand, and the newsvendor cost there must match the restricted minimum. A naive reading of " decreases in " holds only for the least minimizer. For an arbitrary selection, the argument has to work through the bound (EC.16) alone.
PerishBaseStock.Outdating and builds on the published demand layer CappedBaseStock_Model (i.i.d. demand path, demand law with ) and the newsvendor functions of LostSalesOrderUpTo.Asymptotic.Backorder.Fin (m - 1) → ℝ≥0 of cumulative levels, with . When the state is empty and everything left over outdates. Levels range over .atTop there. The goal asserts that is finite and that the difference of real values tends to , so no convention enters.When customers request a customized product, their requests can reveal information about what they value. A seller can use that information when setting a price, while a customer can choose a request with the resulting price in mind. The question is whether customers with different preferences can make different requests in equilibrium. Liang Guo's The Voice of Customers in Customization, §3.3, studies this question in a two-type model of buyer-led product design, called O-Learning. It compares O-Learning with a separate game in which the seller chooses quality after a customer's cheap-talk message. This mission concerns only the O-Learning game.
Proposition 3 of the SSRN author copy identifies when a particular cheap-signaling equilibrium exists: each type asks for the quality it would prefer if its type were known. Section 3.3 then asks whether a different pair of requests could separate the types when that equilibrium fails. The Appendix, under “No Other Separating Equilibrium under the O-Learning Customization,” establishes nonexistence below the same threshold. It is this latter claim, for every request pair and every admissible off-path belief, that is the mission's target.
A buyer has one-unit demand and a privately known quality preference , where . A fraction of buyers have the high preference. Quality is a real number . Producing or delivering a product of quality costs , while preparing to sell it costs , with . The latter is sunk before the price is determined. These are the assumptions of §2 of the paper, pp. 5–9.
Under O-Learning, the buyer requests a quality. The seller observes the request, forms a perceived type , and accepts or rejects. If rejected, both parties receive zero. If accepted, the price-setting stage follows the paper's reduced-form bargaining rule: the seller has the opportunity to make the price offer with probability and the buyer has it with probability . The buyer's expected payoff, conditional on acceptance, is equation (9):
The seller accepts precisely when , including equality. A separating pure-strategy equilibrium consists of two distinct, nonnegative requests and , plus a belief about the buyer's type after each possible request. The seller identifies the correct type at and ; away from those two requests its belief can vary. Given that belief and the seller's acceptance rule, neither buyer type can improve its payoff by making any other nonnegative request. The pricing stage is represented by the payoff formula rather than by a separate bargaining game, as in §3.3 of the source.
For a buyer whose type is known, equation (10) gives the complete-information request
Proposition 3 defines three ratios and their combined threshold:
The prior is part of the model, although the separation threshold does not depend on it.
The goal says that, whenever the standing assumptions hold,
Equivalently, the existence of any such equilibrium requires . The goal quantifies over all pairs of nonnegative requests and all belief functions consistent at those requests. It does not prescribe the requests or Proposition 3's supporting off-path beliefs.
The milestone list follows the two failure regimes stated in the Appendix, pp. 28–29. When , it first identifies the low type's equilibrium request and then rules out separation. When , it records the form of and the bounds on acceptable equilibrium requests before ruling out separation in either order of and . These are the author's stated intermediate claims, with their source text attached to each milestone.
Proposition 3 shows when the two complete-information requests can be sustained as a separating equilibrium. The Appendix result strengthens the interpretation of its threshold: below , changing the requests or the off-path beliefs cannot restore separation. This matters for the paper's comparison of who controls quality design and when customization can reveal preferences. Without the nonexistence result, the failure of the cheap-signaling request profile would leave open another separating profile with distorted qualities.
The result is proved in the SSRN author copy, and this mission asks for a machine-checked version of that proof. The proposed definitions and statements compile as Lean declarations, but their proofs are open. A completed development would also supply reusable calculations about the seller's acceptance range and buyer payoffs with quadratic costs and endogenous beliefs. The milestones identify these specific pieces of work; they do not claim that a general signaling-game library is already formalized.
Ruling out just the request profile would be insufficient. An equilibrium candidate can use another pair of qualities and can assign either type to requests outside its path. Acceptance changes the payoff discontinuously: a request that would be attractive if accepted instead pays zero when rejected. The buyer's conditional payoff also contains two terms, so a polynomial formula obtained on an accepted range need not hold at every quality. The main challenge is to control all deviations and beliefs under the actual acceptance rule, while maintaining the strict threshold inequalities in both failure regimes.
Lean uses a two-constructor buyer type, a model with real parameters , and a predicate for the paper's standing assumptions: , , , , and . Requests and deviations are restricted to . Beliefs are total functions from real requests to the two named types, constrained only at the equilibrium requests. Seller acceptance is the printed inequality and accepts at equality; a rejected request pays zero. The conditional payoff retains both maxima from equation (9), and is the printed expression, not a value defined through equilibrium existence. No fixed cost for learning or customization is included, as in the paper's main analysis.
The equilibrium predicate does not fix off-path beliefs, require the requests to equal , or replace seller acceptance with a derived threshold. The proof therefore cannot become a restatement of Proposition 3. The local O-Learning definitions duplicate the draft model of the companion mission because unpublished drafts cannot be imported. The paper's last sentence on p. 19 calls the cheap-signaling equilibrium “the only separating equilibrium.” The Appendix proves nonexistence when the ratio is below ; it does not establish global uniqueness when the ratio is above it, and global uniqueness is false. This mission states the Appendix's precise claim.
News publishers depend on direct visits for advertising revenue, while social platforms can show publishers' content inside their own feeds. That arrangement can move reading time from the publisher's site to the platform without changing how much news a consumer reads. It can therefore change the publisher's return from improving content quality. De Cornière and Sarvary study this question in a sequential model of a monopoly newspaper, a social platform, and consumers who divide a fixed amount of attention between the two sites. Their Proposition 1 says that unilateral content bundling lowers the publisher's profit, yet can either raise or lower its equilibrium quality depending on the cost of quality. De Cornière and Sarvary, working paper, pp. 7–12.
This mission concerns the paper's unilateral content bundling regime: the platform can incorporate news into its feed without a payment or a negotiated agreement with the newspaper. The source for theorem numbering is the Toulouse School of Economics Working Paper n° 1152, August 2021. The article later appeared in Management Science in 2023. The working paper's Proposition 1, Lemmas 1–4, and equation (2) are the targets here. The paper separately studies subscription pricing, voluntary participation, and negotiated bundling; those are separate settings. De Cornière and Sarvary, working paper, §§4–6.
A newspaper first chooses news quality . A platform next chooses a news share in its feed. Consumers finally allocate one unit of time between the newspaper's site and the platform. Write for newspaper time and for platform time. The newspaper shows only news. A fraction of platform time exposes the consumer to news; the remaining fraction exposes the consumer to user-generated content (UGC). News and UGC consumption are
The representative consumer obtains utility . When unconstrained by the available mix, the consumer wants news consumption . The platform earns , where one unit of UGC time yields one unit of revenue and one unit of news time yields . The newspaper earns : direct time pays per unit and indirect news time pays . Producing quality costs , giving newspaper profit . De Cornière and Sarvary, working paper, pp. 8–9, equation (1).
A subgame-perfect equilibrium (SPE) specifies consumer attention after every feasible pair , a platform news share after every feasible , and an initial quality. At each stage the chosen action maximizes that stage's payoff given the continuation strategies. The no-bundling benchmark is the same game with , which forces . Consumer surplus is utility at the equilibrium attention allocation. De Cornière and Sarvary, working paper, pp. 9–10, §4.1.
The goal is Proposition 1, comparing every bundling SPE with every benchmark SPE. Both sorts of equilibrium must exist. Publisher profit is strictly lower under bundling. Away from the crossover cost, quality and consumer surplus increase exactly in the low-cost regime:
where . A further clause records that at there is an equilibrium with quality below the benchmark. De Cornière and Sarvary, working paper, p. 12, Proposition 1; p. 31, proof.
The milestones follow the paper's named results and displays: Lemma 1 gives benchmark quality and profit ; Lemma 2 gives consumer attention ; Lemma 3 identifies the platform share ; equation (2) gives the publisher's two-branch profit; the displayed definitions on p. 12 identify the branch maximizers and ; and Lemma 4 characterizes equilibrium quality. The proof of Proposition 1 also states the ordering and relates surplus to the optimal content mix. De Cornière and Sarvary, working paper, pp. 10–12, 31.
The profit and quality effects answer different questions. Even if total news consumption stays at the consumer's preferred level, moving some of that consumption onto the platform reduces the publisher's direct traffic and hence its profit. Quality responds to a comparison of the publisher's gains from direct and indirect readers. The cost threshold distinguishes when the equilibrium moves toward a higher-quality strategy that attracts direct visits and when it moves toward a lower-quality strategy consumed through the platform. Because surplus in this model rises with equilibrium quality, the same threshold governs consumer surplus. De Cornière and Sarvary, working paper, pp. 12–13, 31.
The paper proves these claims mathematically; the Lean theorems in this proposal are open statements awaiting machine-checked proofs. Formalizing the complete sequential game would produce reusable specifications for attention allocation, contingent strategies, and equilibrium comparisons in platform markets. The first-stage profit identity and the best-response theorems are also usable independently of the final comparative-static result. This mission does not assert that the article's other models have already been formalized.
Checking only the realized quality and platform share does not establish subgame perfection. A different quality chosen by the newspaper changes the platform's subsequent action and then the consumer's allocation; those continuation choices must be valid after every feasible deviation. The publisher's resulting objective also changes form at . At the cost the two candidate qualities both maximize profit, so an assertion about “the” equilibrium quality requires care. The article prints a low-quality choice at equality, while the game itself admits both. De Cornière and Sarvary, working paper, pp. 11–12, equation (2), Lemma 4; p. 31, proof.
The Lean model uses real parameters . The standing assumptions are exactly Table 1: , , , and . Quality, attention, and platform share range over , , and respectively. The paper's earlier convention is superseded here by its Table 1 interior range; appears only as the benchmark instance. Real division in the candidate formulas is used under assumptions that make every denominator nonzero. De Cornière and Sarvary, working paper, pp. 8, 10, Table 1; p. 31, proof of Lemma 4.
The pin applies only to Proposition 1's two “if and only if” comparisons. At equality, Lemma 4 is stated with both possible equilibrium qualities, and the goal retains the strict publisher-profit comparison. The platform's share theorem excludes , where platform time is zero and its choice is indifferent. The consumer-attention theorem assumes before dividing by . The benchmark is an SPE with cap zero, and surplus is evaluated from utility; neither is inserted as a closed formula. Equilibrium strategies are defined by best responses after all feasible histories, and explicit existence clauses prevent claims about all SPEs from holding vacuously. These choices rule out defining equilibrium quality, benchmark quality, or surplus by the expressions that the milestones are meant to establish.
The development needs real arithmetic and interval sets from Mathlib, a model-specific strategy profile, utility and revenue definitions, and the three stagewise best-response conditions. Contributions establishing the consumer, platform, or publisher stages, the crossover case, and the final profit and surplus comparison are within scope. Subscription pricing and negotiated bundling require different games and are outside this mission.
Blood platelets, fresh food and many pharmaceuticals have a fixed lifetime: a unit that has not been used within periods of its arrival must be discarded. A retailer of such a product faces the usual trade-off between leftover stock and lost sales, plus the cost of discarding outdated units. The issuance policy, the order in which units of different ages are handed to customers, changes the problem. Under first-in-first-out (FIFO) the oldest units go first, as in a blood bank. Under last-in-first-out (LIFO) the newest units go first, as when shoppers pick the freshest milk at the back of the shelf, so that old stock tends to accumulate and outdate.
The optimal ordering policy of a perishable system depends on the full age profile of the stock (Nahmias 1975) and is intractable to compute except for small lifetimes. Practice uses base-stock policies, which raise the total inventory to a fixed level in every period. Bu, Gong and Chao (SSRN 3724966, accepted in Management Science, 2022) give the first theoretical guarantees for such policies in perishable systems. This mission covers their LIFO results (§4.1).
Demands are i.i.d. copies of a nonnegative random variable with and distribution function . Its lower support is , and is unbounded when for every . Units live for periods. Leftover stock costs per unit, a lost sale costs , and an outdated unit costs an extra .
At the start of period the state is , where is the stock whose remaining lifetime is at most periods, and . The firm orders , which raises the total level to . Demand is served newest-first and unmet demand is lost. The amount outdated and the next state are
The system starts empty. A policy is admissible if each order is a nonnegative measurable function of the current state. Its long-run average cost is
and is the infimum of over all admissible policies. The base-stock policy orders , and its cost is .
The paper bounds between two explicit functions (Lemma 3):
The heuristic level is any minimizer of on . The newsvendor level is . The proof also uses and its minimizer .
All three parts are stated for every minimizer , and in (b) and (c) for every selection of minimizers as the parameter varies.
Part (a) gives a gap of order that holds for every demand law with finite mean. Parts (b) and (c) identify regimes in which a single explicit base-stock level is asymptotically optimal. Part (c) is sharp: the companion Proposition 1 (mission 6 of this series) shows that when and , even the best base-stock policy stays a positive distance from optimal as . Under FIFO the corresponding gap decays exponentially in (Theorem 1, mission 1), so the two issuance rules behave differently. Whether the LIFO gap also decays exponentially is left open in the paper.
The results are proved in the paper but are not machine-checked anywhere. Prove2Me has no perishable lost-sales model with LIFO issuance. This mission provides one, built on the published demand layer and newsvendor functions, together with the sample-path recursion (EC.18), which is specific to LIFO.
is a long-run average over a Markov chain on an -dimensional state, and no closed form is known. The upper bound needs an accounting argument over windows of periods. The lower bound needs the exact recursion (EC.18) for the outdating of a base-stock policy under LIFO, which differs from the FIFO recursion. Treating the system as a newsvendor problem with a correction term fails: the outdating cost of lies strictly between the two bounds, and the minimizer of one bound is not a minimizer of the other. In (b) the absolute gap does not vanish, so the argument needs . In (c) the levels and move with , and the limits must be controlled uniformly over all minimizers.
Fin (m - 1) → ℝ of cumulative levels, with . The case (empty state) is included.leadTimeLaw.No trivializing reading is admitted. OPT ranges over all admissible policies, not only base-stock ones. is not a formula. No gap can hold through or division by zero. The parameters , , and the demand law are not specialized.
Proposition 2 holds under any issuance policy. Its FIFO instance and the FIFO lemmas are posed in mission 1 of this series, and only the LIFO instance is posed here. Lemma 3 and (EC.22) are also used in mission 6. Proofs of any milestone are welcome. Reusable infrastructure includes the law of the maximum of i.i.d. demands, convexity and continuity of the newsvendor cost, and existence of minimizers of and .
Social services such as public housing, food banks and free clinics are congested: the users who arrive wait in a queue they cannot see, and some of them could do almost as well elsewhere. A provider who sees the queue can decide what to tell arriving users about it. Telling low-need users that the queue is long sends them to their outside option and shortens the wait for everyone else; telling them too much may send away users the provider would rather serve. Information design (Bayesian persuasion, Kamenica and Gentzkow 2011) studies what a sender who commits to a signaling rule in advance can achieve.
Anunrojwong, Iyer and Manshadi (2023) build on the queueing persuasion model of Lingenbrink and Iyer (2019) and ask how much welfare information design can add in a congested service. Their answer depends on whether users are heterogeneous. This mission formalizes the homogeneous case, Proposition 1: when every user is low-need, the simplest policy, full disclosure of the queue length, is already within an explicit factor of the best signaling mechanism.
A single server with exponential service times of rate one serves users first come, first served. Low-need users (type L) arrive as a Poisson process of rate and may leave for an outside option worth ; high-need users (type H, rate ) always join. The total rate is . A type- user who joins with users present receives utility , where , is strictly decreasing, for large , and the increments are non-increasing (Assumption 1).
By Lemma 1 of the paper, an obedient signaling mechanism is described by the stationary distribution of the queue length on it induces. The admission policies are the probability distributions with
and the signaling mechanisms are those that also satisfy the obedience constraints
The welfare of low-need users is .
A threshold policy with , , , admits L-users below queue length , admits them with probability at , and turns them away above . denotes . The full-information threshold is the least with , and the full-information mechanism is . The homogeneous setting is .
In the homogeneous setting, with
the goal asserts three facts:
The paper phrases parts 1 and 3 for "the optimal signaling mechanism sm". They are stated here for every element of , which implies the paper's form for any maximizer and requires no existence result.
Proposition 1 bounds what persuasion can do when users are alike. The ratio is at most , so the gain from optimal signaling is small whenever full information already admits a few users. The paper contrasts this with the heterogeneous setting (§4.2), where information design can Pareto-improve on full information substantially. The homogeneous bound is the baseline for that comparison: it shows that the gains there come from the presence of two types, not from pooling queue states.
The result is proved in the paper. Nothing in this model has been machine-checked so far. A formal proof would check the reduction from an arbitrary signaling mechanism to a threshold mechanism (Theorem 1), the unimodality of threshold welfare (Lemma 5(2)), and the obedience calculation on p. 40. It would also confirm that these hold at , where the stationary distribution of the always-join policy no longer exists. The model layer defined here is shared with three sibling missions on Theorems 1 and 6 and Proposition 3 of the same paper.
The two finite inequalities, the bound on and the comparison of with , are elementary. The difficulty lies in part 1 for an arbitrary , which is a distribution on an infinite state space. Restricting attention to threshold policies is not free: Theorem 1 only says that Pareto-efficient mechanisms are thresholds. An arbitrary obedient must either be shown to be dominated by a threshold mechanism, or bounded directly. The sets are not compact in the obvious topology at , so the existence of an optimal mechanism cannot simply be assumed.
Part 3 needs a strict comparison. When , the proof must exhibit an obedient threshold policy strictly better than full information, which requires the obedience constraint to hold for thresholds slightly below .
Lean represents queue lengths as ℕ and distributions as functions ℕ → ℝ, inside the namespace NeedPersuasion.Homog. Every statement carries the standing assumptions M.Standing: , , , , for some , strictly decreasing, and non-increasing. The homogeneous statements add . The type-H utility stays a field of the model so that the definitions coincide with those of the sibling missions; with it does not enter .
Conventions the formalization commits to:
The following trivializations are excluded: defining "sm" as , defining it through sSup of an unbounded set or Classical.choose, computing from Lemma 5's closed form, or stating part 3 with both sides about the same threshold. A sorry-free sanity check exhibits a model satisfying all hypotheses (, , , ) with .
A complete development needs:
ℕ.The perturbation arguments behind Theorem 1 and the lemmas about threshold policies are reusable in the sibling missions. Proofs of any milestone are welcome. So are intermediate lemmas, such as closed forms for and of a threshold policy in the homogeneous case.
Social services such as public health clinics, legal aid offices and food banks are congested: users wait in a queue whose length they cannot see. Some users have no alternative (high need) and others have an outside option (low need). A provider cannot price access, but can decide what to tell arriving users about the queue. Anunrojwong, Iyer and Manshadi (Management Science, 2023; read as arXiv:2005.07253v3) study how far such information design can raise the welfare of both groups. Their model builds on the obedient signaling framework of Lingenbrink and Iyer (Operations Research 67(5), 2019). This mission formalizes their Section 5. It compares the best signaling mechanism with the first-best: the admission policy a provider would choose if it could see user types and order users to join or leave.
A single server with exponential service times of rate one serves an unobservable first-come-first-served queue. High-need users (type H) arrive at Poisson rate and always join. Low-need users (type L) arrive at rate and either join or take an outside option worth . Write . A type- user who joins behind users gets utility . The standing assumptions are , , each strictly decreasing, and the increments non-increasing (Assumption 1).
An admission policy is a distribution on with
their set is . It is the steady state of a queue in which a low-need user arriving at length is admitted with probability . A signaling mechanism is an admission policy that low-need users obey when it is announced as a join/leave recommendation. The obedience constraints are
and the signaling mechanisms form . The welfares are and . For a weight , . Then is the set of maximizers of over , and the set of maximizers over . Under no information (ni) every low-need user joins with the same equilibrium probability . Finally,
is a low-need user's expected utility in an M/M/1 queue with load . It has a unique root .
The goal does not fix or give it in closed form. It asserts only that exists, that is positive, and that the optimal signaling mechanism splits into these two regimes.
In the order the proof in Appendix D uses them:
Theorem 6 says that over a large range of weights the obedience constraints cost nothing. The optimal signaling mechanism coincides with the first-best admission policy, even though that benchmark presumes the provider sees user types and can enforce decisions. In that range the signal acts only as a coordination device, and no user is indifferent between the recommended action and the alternative. This differs from typical Bayesian persuasion, where optimal schemes make some receiver indifferent. The two regimes of the theorem coincide with those of Theorem 5. Where no information is already Pareto-efficient, efficient signaling and efficient admission agree for all weights. Elsewhere, signaling falls short of the first-best only for weights that favour high-need users.
The paper proves these results on paper. To our knowledge none of them has a machine-checked proof. The mission produces a formal model of obedient binary signaling in an unobservable queue, with admission policies, obedience constraints, welfare and Pareto efficiency within a class. It also formalizes the structural theorems and the first-best comparison. Formal proofs would also check the steps the paper calls "straightforward" or leaves out, such as Theorem 2's omitted proof and the coupling arguments.
Each step of the proof uses a different tool. The threshold monotonicity in is a revealed-preference argument, and it needs of threshold policies to be strictly decreasing. Obedience propagates upward only along threshold policies, through the shape of in Lemma 6. The positivity of needs the optimal admission policy for small to violate (LEAVE). Below , the binding (LEAVE) constraint must pin a single threshold. The tempting shortcut is to argue only with the scalarized problem , and it fails for two reasons. At maximizers need not be Pareto-efficient (footnote 12). Also, and are sets, so set equality needs both inclusions and non-emptiness. Existence (Lemma 2) rests on a weak-compactness argument over distributions on , which is delicate at .
Hypotheses added relative to the page, all stated in the items:
Encodings that would trivialize the goal are excluded:
The work needs:
The model layer and the threshold structural theorems can be reused by the companion missions of this series. Proofs of individual milestones are welcome independently.