Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A manufacturer selling through several retailers rarely publishes the terms it gives each of them. Wholesale prices, slotting fees and rebates are negotiated bilaterally, and a retailer usually sees its own contract but not its rival's. Much of the supply-chain contracting literature nevertheless assumes observable contracts, and under that assumption a well-known ranking holds: the manufacturer, the channel and social welfare do better with two-part tariffs (a fixed fee plus a marginal wholesale price), while the retailers do better with plain wholesale-price contracts.
The industrial-organization literature has long known that secrecy changes the manufacturer's problem. Hart and Tirole (1990), O'Brien and Shaffer (1992) and McAfee and Schwartz (1994) showed that a manufacturer that cannot commit publicly to the terms it offers each retailer is tempted to undercut itself bilaterally: it offers one retailer a better deal, at the expense of the others, and the retailers anticipate this. Li and Liu (Manufacturing & Service Operations Management, SSRN 3339702) ask what this does to the ranking of contract types in a simple model of price competition. Their answer, Proposition 3, is that the ranking reverses when competition is intense: the manufacturer prefers wholesale prices once the competition parameter reaches , the retailers always prefer them, and the whole industry prefers them once the parameter reaches .
A manufacturer with zero unit cost sells one product through two retailers . Retailer charges price and faces demand
where measures how intensely the retailers compete.
The manufacturer offers each retailer a contract , a fixed fee and a marginal wholesale price . In the two-part tariff game contracts range over ; in the wholesale-price game over . The contract type is common knowledge, but retailer does not observe the terms offered to retailer .
Each retailer, seeing only its own contract, accepts or rejects and chooses a price and an order . A retailer holding the belief about its rival's price conjectures the profit
and if it rejects. The manufacturer earns from each retailer that accepts.
Because no proper subgame exists, the solution concept is the contract equilibrium with passive beliefs: a pair of contracts and, for each retailer, a strategy giving an action at every contract of the class, such that
The equilibrium profits are the manufacturer's , retailer 's (computed with the actual prices), and the industry's .
For every , both games have a passive-belief equilibrium, and for every equilibrium of the tariff game and of the wholesale-price game,
together with the strict versions of the two equivalences ( iff ). At the thresholds the two profits coincide.
Proposition 3 shows that the textbook ranking of supply-chain contracts depends on an observability assumption that is often false in practice. Under secret contracts the fixed fee loses its usual advantage: a manufacturer offering two-part tariffs cuts marginal wholesale prices to zero, retail competition becomes as fierce as possible, and all profit has to be collected through fees out of a shrinking pie. A wholesale price keeps marginal costs, and therefore retail prices, high. For this "win-win" makes both the manufacturer and the retailers better off; as the manufacturer's gain approaches 100 percent and the industry's 200 percent (p. 18).
The proposition is proved in the paper's Online Appendix. No machine-checked proof of it, or of the underlying equilibria, is known. A formalization would fix the solution concept precisely (quantification over off-path contracts, the tie-break at zero conjectured profit, the domain of contracts), establish uniqueness of the equilibria, which the page asserts only implicitly, and provide a reusable encoding of contract equilibria with passive beliefs for later missions on vertical contracting.
The closed forms of Propositions 1 and 2 make Proposition 3 a comparison of rational functions. The work is in the equilibrium layer. The retailers' strategies must be optimal at every contract, including contracts never offered, and the manufacturer's deviation is evaluated against those off-path responses while the rival's action is held fixed. Each retailer's belief is pinned to the rival's equilibrium price, so the equilibrium is a fixed point of a belief map composed with two optimization problems, the retailer's and the manufacturer's bilateral one. Uniqueness of the equilibrium is part of the claim, and the retailer's problem is non-smooth because of the in sales and the accept/reject choice. At a zero marginal price the optimal order is not unique, so order quantities cannot be pinned down.
Everything lives in the namespace ContractUnobs.Compare, with one definitions module, ContractUnobs.Compare.Model. Retailers are indexed by Fin 2 with rival 1 - i; all quantities are real. A contract is a structure with fields K and w; a retailer's action records accept : Bool, a price p and an order Q. IsPassiveEq θ cls E is the equilibrium condition above for a contract class cls (tariffClass or wholesaleClass); mfrProfit, retProfit and industryProfit are the realized profits.
Conventions committed to, each disclosed in the item statements:
Stating Proposition 3 with the closed-form values of Propositions 1 and 2 substituted for the equilibria is a different, nearly trivial theorem and is not the goal; the goal quantifies over equilibrium profiles, and its existence conjuncts exclude a vacuous reading.
The observable benchmark (Lemmas 1–3), the corollaries, and the extensions of §6 (buyback contracts, asymmetric retailers, downstream merger) are not part of this mission. Contributions welcome: proofs of the milestones, a general lemma on maximizing over , and a reusable treatment of passive-belief contract equilibria.
Firms carry risks they cannot insure directly. A farmer's revenue depends on local yield and on local price; an airline's cost depends on jet fuel at a specific airport; an energy retailer's margin depends on load and on weather. Exchange-traded derivatives are written on standardized indices, so the exposure that matters is only partly claimable. Guiotto and Roncoroni (Operations Research 2022) study the design of a combined custom hedge: one over-the-counter claim written on the claimable part of the firm's risk, plus a second claim written on a side index that is correlated with the unclaimable part. The question is when such a pair is well defined, that is, when the firm's mean–variance hedging problem has one and only one optimal pair of claims.
Single-claim custom hedging goes back to Chowdhry and Howe (1999) and Caldentey and Haugh (2006; 2009, Operations Research 57(1)), whose framework prices claims through a pricing kernel known to the firm; that framework is adopted here. With two claims on two different random elements the optimal pair is coupled, and existence and uniqueness are no longer automatic.
Fix a probability space carrying three random elements, valued in arbitrary measurable spaces: the claimable term , the nonclaimable term and the side index . Write and . The firm's business position is for a Borel revenue function , assumed square-integrable.
A claim on is a random variable that is -measurable and has finite variance; the set of such claims is , and is defined likewise. The centered subspace consists of claims with .
Claims are priced by a pricing kernel , the density of an equivalent martingale measure : it is positive almost surely, has mean one and is square-integrable, and . The firm ranks positions by the mean–variance criterion
The value-centered design problem is
A maximizer is an optimal combined claim pair. The dependence between and is measured by the maximal correlation
with the Pearson correlation. Finally is the optimal hedging kernel, , and .
If , then
The result. Theorem 1 makes the combined hedge an object: without it the optimal pair may fail to exist or may be non-unique (the paper points to Appendix EC.1(F) for non-uniqueness), and the paper's later results, the design integral equation (Theorem 2) and the value of combining claims (Theorem 3 and Definitions 1–3), are stated for the optimal pair whose existence and uniqueness Theorem 1 provides. Equation (7) separates the optimal claim into a part determined by the kernel alone and a cross-claim feedback through . The condition is checkable: for jointly lognormal it reduces to for the underlying normals (Example 4).
Formalizing it. The theorem is proved in the paper; no machine-checked version exists. A formal proof needs a Hilbert-space treatment of conditional expectations onto two σ-algebras, a formal maximal-correlation index, and an existence argument for the maximization problem itself, which the paper's proof leaves implicit (see below). The intermediate statements are general facts about pairs of σ-algebras with maximal correlation below one and are reusable outside hedging.
The optimal pair is coupled: the claim on depends on the conditional expectation of the claim on given and conversely, so neither can be computed first. When and share information, the two claim spaces overlap and the sum need not be closed in ; a maximizing sequence can then escape, and two different pairs can produce the same hedge. The condition excludes this, and the work lies in turning it into a quantitative bound on the alternating conditional-expectation operator.
A second difficulty is a gap in the printed argument. The paper derives the first-order system (5) as a necessary condition and then proves that the resulting fixed-point equation has a unique solution. It does not show that the pair built from that solution is optimal for (4), so existence of a maximizer needs a separate argument that the first-order condition is also sufficient or that the maximum is attained. The goal is stated for maximizers of (4), so this step cannot be skipped.
Everything lives in the namespace CustomHedge.Exist. A Market bundles , , , , the revenue function, the kernel D , rho and a; Standing collects the assumptions above. Conventions:
U over all feasible pairs; uniqueness and the equations (5), (7), (EC.25), (EC.27) hold -almost surely.condExp.A trivializing formalization is ruled out: the goal quantifies over maximizers of (4), not over solutions of the first-order system or of (EC.27), which are separate milestones. A sorry-free check confirms the standing assumptions and hold together with a non-trivial .
Needed infrastructure: conditional expectation as an orthogonal projection, the identity for -measurable , Banach's fixed-point theorem on a closed subspace of , and concave maximization over a closed affine subspace. The maximal-correlation file is reusable beyond this mission. Proofs of individual milestones, and a proof of the goal by any route, are welcome.
Restaurants that take orders online promise each customer a pickup time when the order is placed. A static quote promises every customer the same lead time , the form in common use. Once the promise is fixed, the kitchen still decides when to start each order. Starting too early means the food waits and cools (an earliness cost). Starting too late breaks the promise (a tardiness cost). Farahani, Dawande and Janakiraman (SSRN 3557605; published in Operations Research, 2022, doi:10.1287/opre.2021.2203) model this as a single-server queue and propose simple threshold policies. To judge those policies against the unknown optimum they need lower bounds on the optimal long-run average cost, and their first such bound is the subject of this mission.
The bound uses a clairvoyant relaxation: a decision maker who knows every future arrival and service time can do no worse than one who does not. Relaxations of this kind are standard for finite-horizon stochastic dynamic programs, where the relaxed problem is deterministic and its expected value can be estimated by Monte Carlo simulation (Brown, Smith and Sun, 2010, doi:10.1287/opre.1090.0796). Brown and Haugh (2017, doi:10.1287/opre.2017.1631) extended them to discounted infinite-horizon problems. The queue here is an undiscounted infinite-horizon problem: the clairvoyant problem involves an infinitely long sample path, which cannot be simulated directly. Theorem 4 of the paper resolves this by showing that the clairvoyant cost per customer over any finite number of customers is already a valid lower bound.
A probability space carries inter-arrival times and service times . The are identically distributed with mean , the are identically distributed with mean , the whole family is mutually independent, and (the queue is stable). Customer arrives at
and is due at , where is the quote time. The arrival rate is .
A schedule assigns to each customer a service start time , which may depend on the sample path. It is FCFS-feasible if on every sample path
Customer departs at and pays , where
The long-run average cost of a schedule is (the paper's form (4))
The perfectly-clairvoyant cost of customers on a sample path (program (12)) is
In Lean these are StaticQuote.Clairvoyant.Model with Standing, rate, arrival, due, g, IsFCFSSchedule, cost, IsSchedule and gamma.
For every FCFS-feasible schedule and every ,
The paper writes the left side as , the optimal cost. The statement here holds for every schedule, so it covers the optimum whenever one exists.
The result. Theorem 4 turns an infinite-horizon lower bound into a finite computation: for any , the deterministic clairvoyant problem over customers can be solved on simulated sample paths, and the sample mean, scaled by , estimates a lower bound on the optimal long-run cost. The paper uses this bound, with its refinements (Theorems 5 and 6), to certify the numerical quality of its threshold policies (§7). Without it, the only available benchmark is the asymptotic clairvoyant cost, which cannot be computed.
Formalizing it. The paper proves the theorem with an informal argument. No machine-checked proof of this bound, or of the sample-path GI/G/1 objects it needs, is known to exist. The mission produces a sample-path model of a single-server queue with due dates, a clairvoyant value defined as an extended-real infimum, and the measure-theoretic step that the clairvoyant cost of a block of customers has the same expectation as that of the first block.
Most steps are monotonicity of integrals and of . The substantive step is block stationarity (milestone 4). and are not functions of the same random variables, and depends on the absolute arrival times , which carry the whole history . The equality of expectations needs the clairvoyant value to be expressed as a function of relative arrival times and service times only. It also needs that function to be measurable (it is an infimum over uncountably many schedules) and the joint law of a block of an i.i.d. family to be invariant under shifting the block. The doubling argument then has to pass from horizons to all horizons , which in the extended reals needs no integrability.
Many sellers accept returns of standard goods but restrict returns of customized goods. A customized item is more likely to fit its buyer, yet it may be harder for the seller to recover value when it comes back. Choosing a return policy therefore changes both what customers buy and how many units they return. Esenduran, Letizia, and Ovchinnikov study this tradeoff in a two-product market and show that permitting customized-product returns can, for some parameters, raise the firm's profit while reducing its total return volume (accepted manuscript, Proposition 2, p. 11). The result is an existence statement about a firm's optimal policy, not a claim that permissive returns always have this effect.
A unit mass of consumers has taste uniformly distributed over . The standard product is located at and has baseline willingness to pay . The customized product changes both a direct-value attribute and a taste-related attribute; its baseline willingness to pay is . Here may have either sign, while measures the taste improvement. These are the paper's normalized expressions, with the reservation value set to one (§2.2, pp. 5–6).
Product matches a consumer's needs with probability ; after a mismatch, the consumer values it at only , where . The firm chooses a nonnegative price and a nonnegative return fee for each product. A buyer learns whether the product matches after buying and keeps it exactly when keeping gives at least the payoff from returning it. Before purchase, the consumer compares the two expected utilities, including this return option, and buys only if the best one is positive. A tie between products goes to the standard product. These rules determine the buyer volumes , the mismatch-return segments , and the keep segments . The expected number of returns is (§2.3, p. 7; problem (3), p. 10).
With production cost and recovered value on a returned unit, the firm's expected profit and total return volume are
An optimal policy maximizes this profit over all nonnegative prices and fees. In the paper's disallow counterfactual, the standard product's price and fee remain at the original optimal policy's values, while the customized price and fee are chosen to maximize profit subject to . The proof writes this as problem (5) in the Solution 2 region (Online Appendix pp. 14–15).
The goal is Proposition 2. There exist admissible parameters and an original optimum such that customized returns occur, and for every original optimum and every associated disallow-counterfactual optimum,
Both optimization problems must attain their maxima. The quantified claim is what “can increase profits and reduce total returns” means in this model; it does not replace an optimum by a preselected formula.
Three milestones trace the part of the paper used for this existence result. Solution 2 characterizes an original optimum with positive customized-return and standard-return segments, a positive standard-keep segment, and no customized-keep segment. Solution 2b characterizes the corresponding optimum when customized returns are disallowed and the standard terms stay fixed. Their returns identity expresses the difference in total return volumes as a factor containing ; away from the boundary , that difference is negative exactly when (Online Appendix pp. 4–5, 15).
The paper's claim separates the total number of returns from the permissiveness of one product's return policy. A permissive customized policy may induce some consumers to switch away from standard goods. Since customized goods match preferences more often, those switches can outweigh returns from newly served buyers; profit can rise at the same time. Thus a firm cannot infer total return volume by looking only at the customized product's own returns (§3.2, p. 11).
The paper proves the result analytically. This mission records its model, optimization comparison, and three central statements in Lean; the theorem proofs are open formalization work. A completed development would certify the global optimum comparison, including existence and all admissible nonnegative policies, as well as the algebraic segment identity. The definitions of consumer choice, return volumes, and the constrained counterfactual can also support formalizations of the paper's other solution regions and robustness results.
The return option makes each consumer's expected utility piecewise linear in taste. Which product a consumer buys depends on the upper envelope of two such functions and zero, so the volumes change formula when thresholds cross. The firm's objective is consequently piecewise rather than one differentiable expression on the full policy space. A stationary formula for one segment ordering is insufficient to establish a global optimum; the proof must account for policies on other orderings and their boundaries. The paper's displayed Solution 2 region also includes parameter points where a fee becomes negative or a segment leaves , so those expressions alone do not characterize the intended interior policy (Online Appendix A.2, pp. 3–5).
Lean represents every parameter, price, fee, threshold, profit, and segment size as a real number. Consumer volumes are Lebesgue measures of subsets of ; a consumer purchases only when expected utility is strictly positive. The latter convention follows the proof of Proposition B1 and Table 2, which exclude a buyer with nonpositive expected utility. The paper's p. 7 prose uses a weak inequality; at a zero fee that choice could create a positive-volume tie incompatible with its return accounting. The standard product wins ties between products. The standard product has in the definitions (Table 1, p. 7; Online Appendix p. 11).
The standing assumptions include Table 1's parameter ranges, the ordering condition , , and . The lower bounds and are made explicit. Milestone formulas that divide by or assume and . The Solution 2 and 2b milestones additionally require an interior feasible region: positive return segments, a positive standard-keep segment, nonnegative standard fee, and less than full market coverage. These added conditions select the solution described in the appendix. The displayed customized price of Solution 2 is not used: at the rational consistency witness it conflicts with the displayed segment sizes. The statements retain those segment sizes and the standard terms, which are the quantities needed for Proposition 2.
The goal quantifies over the firm's actual feasible policies and asserts that both optima exist. Defining “optimal” through a closed-form candidate, omitting the disallow maximum, or using a zero-volume population would erase the comparison. Contributions may address global optimality, the consumer threshold and measure calculations, the counterfactual optimum, or the returns identity. The measure and piecewise optimization results would be reusable for other product-line models.
A seller choosing a simple way to sell several items faces a problem when one buyer values both individual items and combinations. Pricing each item or offering the entire set as one bundle is easy to describe; an optimal lottery menu can use many more options. The question is how much revenue this simplicity can cost. Eden, Feldman, Friedler, Talgam-Cohen and Weinberg give a guarantee controlled by how many potentially valuable combinations contain any one item. Their result applies to valuations with complements and feasibility constraints that also create substitutes. The preprint used here is arXiv:1612.04746v2; its theorem and page numbers are the source for this mission.
The paper's lower-bound examples show that dependence on the complementarity degree is needed, up to constants, for the mechanisms under study (§6, pp. 13–15). The mission targets the upper bound, including its stated constant. It does not claim that the stronger lower-bound examples have already been formalized.
Let be a finite set of items. A hyperedge represents a combination with a nonnegative bonus . A fixed feasible family is downward closed and contains the empty set. A buyer receiving bundle can obtain the bonuses of a feasible subset , so the induced valuation is
Each weight is sampled independently from a distribution with finite support; together they induce a population of valuations. As in §2, pp. 4–5, weights outside are zero, and normalizes the empty bundle's value. The population has complementarity degree at most when every item belongs to at most hyperedges for which a positive weight is possible.
A mechanism gives each reported valuation in the finite type space a lottery over bundles and a payment. The buyer evaluates a lottery by expected value. The mission uses incentive compatibility and individual rationality for truthful mechanisms: a buyer prefers their own report, and participating gives nonnegative utility. Let be such a mechanism's expected payment.
BREV is the best expected revenue from a single price for the grand bundle, namely . SREV* is a conservative separate-price benchmark. At item prices , item contributes its price only when some bundle containing has strictly positive surplus and every bundle omitting has nonpositive surplus. The supremum is over all real price vectors; it is the paper's , rather than a favorable tie-breaking convention for an ordinary item-pricing menu (§2, p. 5).
The goal is Theorem 3.2, p. 6. For every population of degree at most and every truthful mechanism ,
The milestones follow the paper's two benchmark terms. Corollary 3.1, p. 6 bounds revenue by NON-FAVORITE plus SINGLE. Theorem 4.6, pp. 9–10 specifies a partition of hyperedges returned by Partition-Edges, and Proposition 4.1, p. 7 bounds SINGLE by . For NON-FAVORITE, Lemma 5.1, p. 10 introduces the CORE and TAIL terms at a cutoff ; Propositions 5.5 and 5.7, pp. 12–13 bound those terms; and Proposition 5.10, p. 13 gives . These seven statements are the mission's intermediate targets.
The theorem gives a concrete revenue guarantee for two simple selling formats even though the valuation can contain overlapping complementary bonuses and feasibility constraints. It says that, within the stated finite-support model, the better simple benchmark captures at least a fraction of the revenue of any truthful, individually rational lottery mechanism. The paper also establishes lower bounds showing that a factor growing with is inherent for its simple-mechanism comparison (§6).
The mathematical result is proved in the paper. The Lean goal and milestones here are statements awaiting proofs; compilation checks their types and definitions, not their truth. Completing them would create a reusable finite product model for mechanism-design arguments, an explicit version of the strict separate-sale benchmark, and a machine-checked combinatorial partition theorem. Those pieces can support later work on revenue bounds with constrained bundles.
The first apparent shortcut is to compare revenue directly with the best bundle price. It cannot account for instances where value is spread among item prices, while item pricing alone cannot account for large complementary bonuses. The paper therefore has to control two different contributions to its revenue benchmark. In the favorite-hyperedge contribution, overlapping edges make independently chosen bundle prices interact. In the nonfavorite contribution, large weights require a different estimate from bounded weights. The duality benchmark also uses ironed virtual values for discrete distributions; replacing them by un-ironed slopes can change SINGLE. These are specific obstacles to closing the Lean goal, beyond the routine finite-sum bookkeeping (§§3–5).
The Lean model uses Finset bundles, a downward-closed finite family , and positive masses on finite supports for each hyperedge law. A finite product support gives the expectation and probability operators. The valuation is computed from a realized hypergraph; mechanisms operate on the resulting finite valuation type space. The goal quantifies over each valid mechanism. It does not use a real supremum over mechanism revenues, whose default value on an unbounded set would make the statement misleading. BREV and SREV* do use real suprema over all real prices, matching the paper's price domains.
Favorite regions compare nonempty hyperedges, with an injective rank resolving ties. The paper specifies a lexicographic tie rule; quantifying over ranks includes that choice. SINGLE uses the slope of the least concave majorant of the finite revenue curve, the discrete ironed virtual value implicit in the paper. Figure 1 is represented by its actual sweep and loop, and Theorem 4.6 excludes the empty hyperedge because that input prevents the stated procedure from terminating. Proposition 5.5 specifies , the domain on which its printed inequality holds. These conventions and the explicit individual-rationality requirement prevent zero-valued or arbitrary-payment cases from trivializing the target.
Contributions toward the published milestones are welcome, including the duality and ironing argument behind Corollary 3.1, the combinatorial theorem for Figure 1, and the finite-support estimates for CORE and TAIL. The listed milestones do not include every supporting lemma from the paper; the remaining posted-price, concentration, and independent-event results may be developed as reusable lemmas where needed. No milestone is weakened to make its proof fit the current library.
Optimal stopping asks when to halt a stochastic process so as to maximize an expected reward. Examples are exercising an American option, selling an asset, or ending a clinical trial. The optimal policy is the solution of a dynamic program over the whole state space. In high dimension it cannot be computed exactly, and the usual approximations (regression on basis functions, as in Longstaff–Schwartz) produce policies that are hard to read: a decision maker cannot see why the policy stops in a given state.
Ciocan and Mišić (Interpretable Optimal Stopping, Management Science 2022; arXiv:1812.07211) propose to restrict the search to tree policies. These are binary decision trees whose split nodes compare one state variable with a threshold and whose leaves say stop or go. The tree is fitted by maximizing the average reward over a finite set of simulated trajectories, which is a sample average approximation (SAA) of the true problem. This mission formalizes the consistency guarantee that justifies the method: as the number of trajectories grows, the optimal SAA value over trees of bounded depth converges almost surely to the optimal true value over the same trees.
The state of the system is a vector . The process runs for periods and starts at a fixed state . Stopping in period in state pays , and rewards are discounted by a factor per period.
A stationary policy is a map . Its stopping time on a path is , and if the policy never stops. Its value is
where a path on which never stops earns . Given trajectories for , the sample-average value is the average of the same discounted reward over the trajectories.
A tree policy is given by four things:
A state descends to the left child of when and to the right child otherwise, and receives the action of the leaf it reaches. is the class of tree policies of depth at most . Once is fixed, the skeletons form a finite set, but the split points range over a continuum.
The paper's standing assumptions are:
Fix a depth and . With probability one there is a finite such that for all ,
This is the paper's headline consistency result: the optimal SAA value converges almost surely to the optimal tree-policy value.
Corollary 1 is what makes the SAA tree-fitting procedure a consistent estimator of the best interpretable policy. A decision maker who optimizes a depth- tree on enough simulated trajectories obtains an in-sample value that approximates, to any precision, the true value achievable by depth- trees. The paper also shows (Section EC.1.2) that the conclusion fails when the depth is unbounded, so the depth restriction is part of the result and not a convenience. Theorem 1, the uniform law behind it, has its own uses: it also controls the out-of-sample value of the SAA-optimal tree.
The results are proved in the paper's electronic companion. To our knowledge they have no machine-checked proof. Formalizing them yields a reusable model of finite-horizon stopping with stationary policies and decision-tree policies, and a uniform strong law for a class of indicator-type functionals that is discontinuous in its parameters. The latter is a pattern that recurs in empirical-risk results for trees and threshold rules.
The strong law gives convergence for one policy at a time, outside a null set that depends on the policy. Uncountably many split points mean uncountably many null sets, so the pointwise law does not yield Theorem 1. The usual fix, a Lipschitz or continuity argument in the parameter, fails because is a step function of : moving one threshold past a sampled state changes a decision and the sample value jumps. The jumps of the true value must instead be controlled by the probability that the process visits the thin slab between two thresholds, which is where Assumption 3 enters. The jumps of the sample value must be controlled by the empirical frequency of such visits, uniformly in the thresholds. The first period is excluded throughout, because is deterministic and Assumption 3 does not apply to it.
Fin n → ℝ, whose Mathlib norm is the sup norm . Paths are Fin T → (Fin n → ℝ), and periods are 0-indexed (k : Fin T is period , so is β ^ k).μ, a probability measure, with and almost surely.g k are measurable. Both are readings of "discounted" and of the expectation on the page.μ, measurable and mutually independent (iIndepFun). The page says only "trajectories of the process" and its proofs use the strong law. averages the first m samples, and "with probability one" is ∀ᵐ.Fin n and leaf actions. Split points are a function of the node address. A split sends ties left (). A leaf has depth . is the type of (skeleton of depth , split points), and the suprema in Corollary 1 are real suprema over it. They are genuine suprema because the type is nonempty and the values are bounded in (for , almost surely).The statements cannot be met by a degenerate policy class or a junk value. is the expectation under the true law, the average over i.i.d. trajectories, and the suprema range over every tree of depth at most with arbitrary real split points. The hypotheses are jointly satisfiable with a nonconstant reward and a split that changes the action. One example is , , , uniform, and .
A complete development needs:
strong_law_ae.Proofs of the milestones in any order are welcome, as are alternative proofs of Theorem 1 through Glivenko–Cantelli or VC-type arguments.
When a bank or firm in a network of mutual obligations cannot meet its liabilities, some rule must decide how much each debtor pays each creditor. The rule used almost universally in the systemic-risk literature is the proportional rule of Eisenberg and Noe (2001): every agent pays its liabilities in full if it can, and otherwise distributes its whole asset value over its creditors in proportion to their claims. Central banks and regulators use it to measure contagion in interbank markets; Elsinger, Lehar and Summer (2006) apply it to the 881 banks reporting to the Austrian Central Bank, and Upper (2011) surveys fifteen such studies.
The rule is usually taken as given. Csóka and Herings (2021) ask which properties of a bankruptcy rule single it out, without assuming in advance that payments depend only on an agent's asset value and liabilities. Their answer is an axiomatization: five basic axioms together with one axiom on splitting an agent into identical copies.
For claims problems (one estate, several claimants) the proportional rule has classical characterizations through nonmanipulability by merging and splitting claims (O'Neill 1982, de Frutos 1999, Moreno-Ternero 2006, Ju, Miyagawa and Sakai 2007). Csóka and Herings show that the network analogue of nonmanipulability is too strong (no rule satisfies it together with the basic axioms) and replace it by invariance to mitosis.
Agents are natural numbers. A financial network consists of a nonempty finite set of agents, endowments for , and a nonnegative liability matrix on with ; is what owes . The class of all financial networks is . The relative liability matrix is if and otherwise.
A payment matrix is an element of , the nonnegative matrices with zero diagonal; is the amount pays . Agent 's asset value is and its equity is . For rows, means for all with strict inequality for some .
A bankruptcy rule assigns to each a payment matrix (Definition 2.1). The proportional rule assigns the solution of
The axioms, in the order of the paper:
Part (a) makes a well-defined bankruptcy rule; part (b) says that satisfies the axioms and that every rule satisfying them is .
The theorem justifies the proportional rule by properties rather than by convention. Because the axioms make no assumption on the form of the rule, consequences such as the absence of pairwise netting are derived, not assumed. Together with the paper's Theorem 5.3 (no rule satisfies the basic axioms and full nonmanipulability), it shows that invariance to mitosis is the strongest splitting requirement compatible with the basic axioms.
The result is proved on paper; no part of it, and no part of the Eisenberg–Noe clearing theory, has a machine-checked proof on this platform. A formalization contributes a reusable layer for clearing payments in financial networks: the system (2.1), its existence and uniqueness under strictly positive endowments, nonnegativity and zero-equity properties of clearing vectors, and their continuity in the data. These are the objects every stress-testing model on top of Eisenberg–Noe starts from.
Existence and uniqueness of a solution of (2.1) is a fixed-point statement about a nonlinear, non-contracting map; uniqueness holds only because every endowment is strictly positive, and fails without it (two agents owing each other one unit with no endowments admit both and ).
In the characterization direction, impartiality only equalizes payments to equal claims, and invariance to mitosis only relates networks that differ by splitting one agent into identical copies. Neither axiom speaks directly about payments to unequal claims, and splitting reaches only ratios of positive integers. Passing from rational to real liabilities needs continuity of the rule and continuity of , and the latter rests on uniqueness of the clearing vector, so the two halves of the theorem are not independent.
Finset ℕ; a fixed finite type cannot express mitosis, which creates fresh agents. Endowments, liabilities and payment matrices are functions on (resp. ) that vanish outside the population, as part of the network structure and of . All quantities are real.OrderHom.lfp, the uniqueness argument under positive endowments, and lemmas on the split network (sums over the copies, the relative liabilities of copies) that serve both Part (I) and Lemma A.1.Emergency departments (EDs) are crowded in part by patients whose condition could have been treated by a primary care provider (PCP), while other patients first visit a PCP, are found to be critical, and are sent on to the ED, paying for two visits. Teletriage — a nurse telephone line that assesses symptoms and recommends where to seek care — is widely offered by health systems and insurers as a remedy for both. It is not error-free: a nurse can undertriage a critical patient (advise primary care) or overtriage a sick one (advise the ED). Whether such an imperfect advisor reduces ED usage, or merely sends more worried-but-well patients to the ED, is the question this mission formalizes.
Çakıcı and Mills (M&SOM, 2020; accepted manuscript at SSRN 2849635) model a patient who does not know whether she is merely sick or critical, chooses between the PCP, the ED and a teletriage call, and updates her belief after the call. Their Proposition 3 answers the question in closed form when every patient calls: teletriage reduces ED usage exactly when the overtriage rate is below an explicit threshold, and reduces double-dipping exactly when the undertriage rate is below another.
A patient is in one of two states, sick () or critical (), and holds a belief , the probability that she is critical. Three actions are available.
Without teletriage the patient's cost is , minimized by the ED exactly when . With teletriage it is
Teletriage is informative when . Proposition 2 of the paper identifies an interval where calling is strictly optimal, bounded by two thresholds
Write and for the probabilities that a patient with belief who acts optimally ends up at the ED, resp. double-dips, without teletriage, and , with it. When beliefs are uniform on , the population rates are the averages , and likewise for the others.
Assume informative teletriage, beliefs uniform on , and : with teletriage everyone calls, and without it some patients go to the PCP and some to the ED. Then
The result separates the two failure modes of a triage line. Overtriage alone governs whether ED visits fall, and undertriage alone governs whether double-dipping falls, with thresholds that depend only on the copays (through ) and the belief range. A health system can therefore read off, for a given patient population, the overtriage rate a teletriage service must achieve before it relieves the ED. In the paper's example (, beliefs uniform on ), : with an overtriage rate of 2.5% or more, teletriage does not reduce ED usage even though every patient calls.
The result is proved in the paper; no machine-checked version exists. Formalizing it means checking the full chain from the patient's optimization to the population averages: that the argmin of produces the threshold structure of Proposition 2 with the stated thresholds, that the per-belief probabilities on p. 11 follow from the optimal actions (including the boundary cases the page leaves implicit), and that the integrals evaluate as claimed. Two printing slips in the proofs (a right-hand side for , and a denominator for ) are corrected in the milestone statements.
The final integrals are elementary once the integrands are known. The work is in the integrands. is not given; it comes from which of three costs is smallest at , and, for a caller, which provider is chosen at each of two posteriors that are rational functions of . On the calling range the patient must go to the PCP after the prediction sick and to the ED after critical, i.e. , and this is what makes . That in turn needs the inequalities and , which use and informativeness, and the linearization of the teletriage cost in the middle range. Reading off the display on p. 11 skips exactly this argument.
Everything lives in the namespace Teletriage.OneShot and in ℝ. A single definition file holds the parameters , the standing assumptions, the posteriors, the costs, the optimal actions, the probabilities, the uniform average and all thresholds.
Conventions:
Not in scope: the traditional-access model (Propositions 4–5), the open- vs traditional-access comparisons (Propositions 6–7, Corollaries 1–2), the sequential POMDP (Lemma 1, Propositions 8–9), and the uninformative cases of Proposition 1.
Welcome contributions: proofs of the milestones in any order. The algebra of milestones 3–4 is self-contained and reusable for the traditional-access analogue (Proposition 4).
Loot boxes are a selling format for virtual items in video games and digital collectibles: the customer pays a fixed price for a box whose content is a random item from a catalog. They generate a large share of revenue in the game industry and have drawn regulatory attention because the customer does not know what they are buying. From the seller's side they are a form of probabilistic selling, close to bundling: a box is a lottery over the catalog, and repeated purchases let a customer assemble a collection.
Chen, Elmachtoub, Hamilton and Lei (Loot Box Pricing and Design, Management Science 2021; the mission follows the authors' manuscript submitted in August 2019) compare two designs. A unique box never repeats an item the customer owns; a traditional box draws uniformly from the whole catalog, so duplicates occur. Their headline asymptotic results are that, as the catalog grows, the optimal unique box earns the mean valuation per item, as much as the grand bundle (Theorem 2), while the optimal traditional box earns exactly a fraction of it (Theorem 3). This mission formalizes the traditional-box result.
A monopolist sells distinct virtual items. A customer's valuations are i.i.d. with a law on with mean and finite variance . A second copy of an item is worth nothing.
The seller offers a traditional box at a fixed price in every period. Each box contains an item drawn uniformly at random from , independently of the valuations and of earlier draws. Let be the set of distinct items owned before the -th box, so . The expected utility of the -th box is
The customer is myopic: they buy the -th box if and only if , and the first time they leave for good. The normalized revenue at price and the optimal normalized revenue are
The milestones use a random walk. For i.i.d. with law , the first passage above a level is ; the paper's is . Also , where is the Euler–Mascheroni constant.
It holds for every valuation law in the model, with no condition on the shape of beyond non-negativity and a finite variance.
whose right-hand side tends to when .
The result. Theorem 3 quantifies the price of duplicates. A traditional box loses a factor against the unique box, the grand bundle and the upper bound of the paper's Proposition 1, for every valuation distribution, so in large catalogs the unique box earns about more per item. The constant comes from the interplay between the coupon-collector waiting times and the price at which the myopic customer stops; the identity and the bounds expose that interplay as a statement about the first passage of a random walk.
Formalizing it. The result is proved on paper, not formalized. Two of the printed steps of the proof need repair: the harmonic-number rewriting in (16) drops one term, and the per-price upper bound (25) derived from it is false at small prices (for , , the revenue is while (25) gives ); its maximization also ignores prices above . The milestones state the corrected claims, and the limit survives. A machine-checked proof therefore settles the headline result independently of the printed argument.
The number of boxes a myopic customer buys depends on all valuations and on the random order in which distinct items arrive, and the index at which the customer stops is not a stopping time of the forward purchase process: whether the customer continues depends on valuations of items not yet collected. Applying Wald-type identities directly to the purchase sequence therefore fails. The revenue identity (16) also mixes two sources of randomness, the coupon-collector waiting times and the values in order of collection, whose independence must be established rather than assumed. On the upper side, the expected first-passage index needs an overshoot bound for renewal processes (Lorden's inequality), which Mathlib does not contain, and the limit needs an upper bound that is uniform over all prices, including prices far above where the per-price estimate of the paper breaks down.
All declarations live in the namespace LootBox.TB. The valuation law is a probability measure F : Measure ℝ with F (Set.Iio 0) = 0 and MemLp id 2 F; is ∫ x, x ∂F and the centred second moment. The sample space for items is valuations × draws, (Fin N → ℝ) × (ℕ → Fin N), with the product of Measure.pi of and Measure.infinitePi of the uniform law on Fin N; draw is the item of the -th box. The purchase count is the first with , valued in ℕ∞; expectations are lower Lebesgue integrals and revenues live in ℝ≥0∞, so no expectation is truncated by toReal. The paper's is a supremum over . The goal is indexed by so that the uniform law is defined. The page's backward walk , extended by virtual i.i.d. variables, is represented by the partial sums of an i.i.d. sequence under walkLaw F = Measure.infinitePi (fun _ => F).
The hypothesis appears in the milestones that divide by , not in the goal: when nothing is bought and both sides of the limit are . A formalization in which revenue is a real number obtained by toReal, or in which prices may be (where a customer with zero valuations buys forever), could make bounds vacuous; neither is used here.
A complete development needs the coupon-collector decomposition of the purchase count, the exchangeability of the values in order of collection, Wald's identity and Lorden's overshoot bound for i.i.d. non-negative walks, Chebyshev's inequality (meas_ge_le_variance_div_sq), Jensen's inequality for , and the bounds and (Mathlib's NumberTheory/Harmonic). Wald's identity and Lorden's bound are reusable well beyond this mission. Proofs of individual milestones, and of the renewal-theoretic lemmas they need, are welcome.
Convex optimization often minimizes a function obtained by applying one convex function to the output of another map. The inner map may be vector valued, and its components need not be linear. To understand sensitivity, optimality conditions, and dual formulations for such a convex composite, one needs its Fenchel conjugate. Standard formulas for an affine inner map do not directly describe a nonlinear, partially defined map. Burke, Hoheisel, and Nguyen treat this setting in finite-dimensional Euclidean spaces and identify conditions under which the conjugate has an exact, attained representation over a polar cone (Burke–Hoheisel–Nguyen, pp. 3, 10).
The paper distinguishes monotonicity of the outer function along the particular epigraph of the inner map from monotonicity throughout the entire cone order. This matters when the outer function behaves well on the points the inner map can reach but does not satisfy a stronger global condition. Its Theorem 12 gives a conjugacy formula under a point-based condition on relative interiors; subsequent results use it to describe subgradients and additive composites (Burke–Hoheisel–Nguyen, pp. 8, 10–13). The mission isolates the conjugacy theorem and the source results that support it.
Let and be finite-dimensional real inner-product spaces. A closed convex cone defines the relation when . Its polar cone is . A possibly partial map , where adjoins one formal value , has an effective domain on which its values lie in . Its -epigraph is
The map is -convex when this set is convex. The paper assumes throughout §4 that is nonempty (Burke–Hoheisel–Nguyen, pp. 6, 10).
The outer function belongs to : it is proper and convex but need not be lower semicontinuous. The composite equals on and outside . The key monotonicity condition, numbered (7), is whenever . It is restricted to the epigraph of , unlike global -increasingness (Burke–Hoheisel–Nguyen, pp. 6, 8).
For an extended-real function , the Fenchel conjugate is . The scalarization takes value on and elsewhere. Its conjugate and the conjugate are combined in the dual function
Here means interior relative to the affine hull, and means the set where is finite (Burke–Hoheisel–Nguyen, pp. 4, 6, 10).
The goal is Theorem 12(c). Suppose is a closed convex cone, is proper and -convex, satisfies (7), and the Slater-type condition (10) holds:
Then the formula has an actual minimizer at every and the effective domain has an exact description:
The milestones follow results stated in the paper: Theorem 2 on conjugacy and infimal convolution; Lemma 6 on support functions; Lemma 4 on the relative interior of a -epigraph; and parts (a) and (b) of Theorem 12, which establish a closure bound and properness with attainment for (Burke–Hoheisel–Nguyen, pp. 5–7, 10).
The theorem turns the conjugate of a nonlinear composite into a minimization over the negative polar cone. It also identifies exactly which dual arguments give a finite value. Attainment matters because later subgradient formulas can use a specific minimizing multiplier rather than only an approximating sequence. In this paper, Theorem 12 is followed by a subdifferential formula for and a formula for the additive composite (Burke–Hoheisel–Nguyen, pp. 10–13).
The mathematical theorem is proved in the source paper. The formalization task is to give its statement a machine-checkable meaning and then prove that statement from a reusable collection of facts about extended-real conjugacy, support functions, cones, and relative interiors. The imported definitions of conjugacy and closed convex cones already have published formal interfaces; the paper-specific definitions and theorems in this mission are draft statements and do not yet have machine-checked proofs.
The main obstruction is the interaction between closure and conjugacy of a sum. A direct interchange of a supremum over primal points and an infimum over cone multipliers does not itself establish equality or the existence of a minimizing multiplier. Theorem 2 supplies a finite-dimensional conjugacy rule under a relative-interior qualification, while Lemma 4 identifies the relative interior of the relevant epigraph. The source then needs to account for the extended-real values of a partial map and for an outer function that is convex but may not be lower semicontinuous (Burke–Hoheisel–Nguyen, pp. 5–6, 10–11).
The Lean model uses finite-dimensional real inner-product spaces and EReal for extended-real values. The partial map is a pair : is its domain, and values of the total representative outside are ignored. Properness of is the explicit hypothesis . The effective domain of an extended-real function excludes ; this corrects a printed in the paper's definition. Conjugacy, epigraph convexity, , closed convex cones, and polar cones reuse published definitions. The lower semicontinuous hull follows the paper's sequential-limit definition, and is Mathlib's intrinsic interior. Pairings on are sums of the two component inner products.
The theorem keeps the infimum and minimizer inside , uses relative rather than ordinary interior in (10), and retains the properness and finite-dimensional hypotheses. These conventions prevent a vacuous or weaker encoding. Attainment is a separate existential statement, including the case where the minimum is . The printed in Theorem 12(a)'s scalarization clause is read as because each scalarization has domain ; the paper's Lemma 10 uses that same space. Theorem 2's closure identity is stated under the added hypothesis . With the paper's definition of as the lower semicontinuous hull, the unconditional identity fails when . The cited source theorem uses a closure that is identically for improper functions.
The mission develops the definitions of effective domain, closure, infimal convolution, indicators and support functions, -epigraphs, scalarizations, condition (7), and . Contributions proving the listed milestones or building general lemmas for those definitions are in scope. Corollaries 14 and 16, the other corollaries of §4, and the applications of §5 are outside this mission (Burke–Hoheisel–Nguyen, pp. 11–27).
Mean field games describe Nash equilibria of games with very many symmetric players by a single limiting object. Whether, and how fast, the equilibria of the -player game converge to that limit is the convergence problem. For games with common noise, a source of randomness shared by all players, the standard route goes through the master equation, a PDE on the space of probability measures whose solution gives the equilibrium value of a representative player as a function of the population's distribution (Cardaliaguet, Delarue, Lasry and Lions, 2019, arXiv:1509.02505).
For finite state spaces the distribution is a point of the simplex. Bayraktar, Cecchin, Cohen and Delarue (J. Math. Pures Appl. 147, 2021) introduced a common noise of Wright–Fisher type, the noise of population genetics, which keeps the distribution in the simplex and makes the master equation uniquely solvable. Its -player counterpart is not obvious, because the Wright–Fisher diffusion is the limit of a resampling of the population, not of independent player noises. The paper behind this mission (Bayraktar, Cecchin, Cohen and Delarue, Mathematics of Operations Research, 2022, arXiv:2012.04845) builds such a game, in which players carry weights that are resampled at random times, and proves that its normalized equilibrium values converge to at a polynomial rate.
There are states and players. Player is at a state and carries a weight ; the weights are rational and sum to , and the set of such weight tuples is . The players interact through the weighted empirical measure
a point of the simplex .
Each player controls the rates at which it jumps between states, at quadratic cost. A drift pushes players towards nearly empty states, where is non-increasing and Lipschitz, equal to on and to beyond . At rate the common noise draws and replaces every weight by . Players pay per unit time and at time .
The equilibrium values divided by the weights, , solve the normalized Nash system: a countable family of ordinary differential equations in , indexed by , with the Hamiltonian and the terminal condition .
The limit object is on , solving the master equation
with . Here are the intrinsic derivatives on the simplex, , and the last term is the Kimura operator of Wright–Fisher diffusions. The mean-field prediction for player is .
For large enough, there are and such that for every , , , and ,
The exponent is existential, so an improvement of the rate does not invalidate the target.
Theorem 2.4 gives a convergence rate for a finite-state mean field game whose common noise keeps the population on the simplex. It shows that the master equation of the earlier paper is the right limit of a concrete finite game, and with a diffusion-approximation argument it yields the paper's second main result, the weak convergence of the equilibrium empirical measure to the Wright–Fisher-type SDE (Theorem 2.6). The bound is not uniform in : it degenerates near the boundary of the simplex and for spread-out weights, which reflects the singular coefficient in the resampling.
None of these results has a machine-checked proof. The mission produces a formal statement of the convergence problem for a game with weighted players, a formal Nash system on a countable state space, intrinsic derivatives on the simplex, and multinomial moment estimates.
The usual proof of convergence plugs into the Nash system, controls the rest, and closes with a Gronwall argument along the -player dynamics. Here the rest is small only on , away from the boundary of the simplex and for moderate weights; the second derivatives of may blow up at the boundary, and the resampling ratio is unbounded as . A uniform estimate of is therefore not available, and the comparison must be weighted by functions of whose expectations along the dynamics can be controlled. The weights are unbounded and enter through their moments.
States are Fin d and players Fin N, with and (no ). Weights are rational, and every equation and conclusion is required only for and . The simplex is Mathlib's stdSimplex. Intrinsic derivatives use lineDeriv; multinomial expectations are finite sums over Finset.Nat.antidiagonalTuple. The resampling ratio is when , as in the paper. Solutions of the Nash system and of the master equation are classical in , with one-sided derivatives at and . The Nash system is solved by any bounded classical solution; Proposition 3.1 says there is exactly one.
The formalization commits to the following readings of the source.
The bound is not trivial. Since and the right side is at least of order , a constant chosen after would make the theorem empty; precedes . The functions and enter only through the Nash system and the master equation, and the class of is not empty: for the function is in it.
The mission takes as given. Its existence for is Theorems 3.2 and 3.4 of Bayraktar, Cecchin, Cohen and Delarue (2021), quoted as Proposition 2.1, which is not a target. Also outside the mission are the -player game itself (Propositions 2.2–2.3), Theorem 2.6, and the process estimates of §4.1 (Theorem 4.1, Remark 4.2, Propositions 4.3–4.4), which need a continuous-time Markov chain with a martingale-problem characterization. Contributions are welcome on every milestone; the multinomial estimates and the simplex calculus are reusable elsewhere.
Allocating divisible resources among agents with money-like budgets is the setting of Fisher markets. When agents report their preferences, a central planner can compute a market equilibrium, and by the Eisenberg–Gale convex program that equilibrium maximizes the Nash social welfare, the budget-weighted geometric mean of utilities. This objective is a standard compromise between efficiency and fairness, and is scale-free in each agent's utility.
The catch is that agents may misreport. Brânzei, Gkatzelis and Mehta (arXiv:1607.01569v3, published in Operations Research, 2022) ask how much Nash social welfare is lost when agents act strategically in simple market mechanisms, measured by the price of anarchy: the worst ratio between the optimal Nash social welfare and the welfare at a pure Nash equilibrium. One of the mechanisms they study is the Trading Post game of Shapley and Shubik (Shapley–Shubik 1977), in which each agent splits its budget into bids on the goods, and each good is shared in proportion to the bids it receives.
For agents with Leontief (perfect-complements) utilities, the plain Trading Post game may have no pure equilibrium at all (Example 4.4 of the paper). The paper repairs this with a small entrance fee : a bid below buys nothing. This mission formalizes the main result of §4.2: with a small enough fee, every pure Nash equilibrium has Nash social welfare within a factor of the optimum.
There are agents and divisible goods, one unit of each. Agent has a valuation vector , a budget , and a demand set , assumed nonempty. Its Leontief utility for a bundle is
so the agent wants the goods in the fixed ratio . An allocation is feasible if and for every good. With , the Nash social welfare is
In the Trading Post game with entrance fee , , agent chooses bids with . A bid is effective, , if , and otherwise. Agent receives of good when , and nothing otherwise. A profile is a pure Nash equilibrium if no agent can raise its utility by switching unilaterally to another bid vector.
Throughout §4 the paper assumes perfect competition: each good is demanded by at least two distinct agents.
The proof passes through Fisher-market prices. Given prices , let be the cost of one unit of utility for agent . A pair is an -market equilibrium (Definition 4.6) if goods with positive price are sold out, every agent spends exactly its budget, and no bundle that agent can afford gives it more than .
For every and every entrance fee , every pure Nash equilibrium of satisfies
for arbitrary budgets .
The proof has two halves, and the milestones follow them.
The result shows that a decentralized, prior-free mechanism, in which agents only place bids, implements the Nash social welfare objective for perfect complements up to an arbitrarily small loss. By contrast, the paper shows that the centralized Fisher market mechanism with strategic Leontief agents has price of anarchy (Theorem 3.9), so the bound here is a strong guarantee for a simple mechanism. Theorem 4.8, which the authors flag as of independent interest, says that approximate Leontief market equilibria are approximately optimal for Nash social welfare. That is a robustness statement about the Eisenberg–Gale optimum, useful independently of any game.
The result is proved on paper; nothing here is open mathematically. To our knowledge none of it has been machine-checked. A complete development produces a reusable formal model of Fisher markets with Leontief utilities, -market equilibria and the Trading Post game, the first such model on the platform, and checks two printed slips that the formalization repairs (see the scope section).
Without the fee, equilibria need not exist, and the natural argument "an equilibrium is a market equilibrium" fails: agents can leave tiny bids on goods they barely need, and the induced prices then misrepresent demand. With the fee, an equilibrium is only an approximate market equilibrium. Each agent is forced to leave a bid of exactly on its non-tight goods, and the money spent there must be shown to cost at most a factor in utility. That accounting is where the bound and the normalization enter.
The second half needs a welfare comparison between an approximate equilibrium and the unknown optimum. The paper uses duality for the Eisenberg–Gale program, in the dual form due to Devanur (2009, manuscript). An exact-equilibrium argument does not transfer directly, because approximate optimality of each agent's bundle must be converted into a product bound over all agents with budget weights.
Agents and goods are Fin n and Fin m; all quantities are real numbers. The standing assumptions are bundled in Standing: , , , and for every agent. Perfect competition is a separate predicate. It is a hypothesis of every Trading Post statement and not of the Fisher-market statements. The utility is a finite minimum over . The Nash social welfare uses real powers of nonnegative bases. Prices are , as in the proof. Deviations in the game range over the whole strategy set, including bids below the fee.
Three encoding choices are disclosed in the statements:
The goal is not trivialized by an empty equilibrium set. A sorry-free sanity check exhibits, for two agents and two goods with and , a pure Nash equilibrium of for every , and an -market equilibrium for every .
A complete proof needs weighted AM–GM, which is in Mathlib as Real.geom_mean_le_arith_mean_weighted. It also needs elementary but careful reasoning about best responses in the Trading Post game. The Fisher-market milestones and Theorem 4.8 are reusable for any later work on Leontief markets. Contributions to either half are welcome independently.
An online display impression often reaches an advertiser through a chain of ad exchanges and networks instead of through a direct sale. Each intermediary runs its own auction among its downstream bidders and decides what to report to the auction above it. Its profit depends on whether it wins upstream and on what it can charge downstream. Even when every local auction is a second-price auction, the sale becomes a sequential game in which agents choose mechanisms. Balseiro, Candogan and Gurkan study this game on a symmetric tree. They characterize a subgame perfect equilibrium in which every intermediary applies a projected virtual value to its highest downstream report (SSRN 2661459; journal version in Manufacturing & Service Operations Management, 2020, doi:10.1287/msom.2019.0854). The single-auctioneer case is Myerson's optimal auction (Myerson 1981). In it, a seller facing i.i.d. bidders with increasing virtual values sets the reserve at the zero of the virtual value.
The seller occupies tier of a symmetric -tree, intermediaries occupy tiers , and buyers are the leaves at tier . Every tier- node has downstream agents. Buyers' values are i.i.d. draws from a law on with lower support end , a continuous strictly positive density on its support, and a finite mean. Buyers report their values.
An intermediary's mechanism is a reserve and a nondecreasing reporting function . If its highest downstream report satisfies , it reports upstream. If it wins upstream, it allocates to that downstream agent. The seller runs a second-price auction with a reserve . A winning agent pays the minimum report that would still have won (Definition A.1). An intermediary's profit is what its winning child pays minus what it pays upstream.
For a law with cdf and density , the virtual value is and its inverse is . The projection point is . The projected virtual value equals below , equals from up to , and equals beyond. If has an atom at , these objects use the positive part (Definitions 3.1–3.2).
The anticipated reports are laws defined by recursion: and , the projected virtual value of the maximum of i.i.d. copies of (Definition 3.3). Assumption 3.1 asks that, for , has finite mean and its positive part has a continuous positive density and a strictly increasing virtual value.
form a subgame perfect equilibrium. Fix any tier and any history: arbitrary mechanisms in for tiers and any seller reserve. Then no tier- node gains by switching to any mechanism in . The seller gains nothing from any reserve instead of .
The theorem identifies optimal mechanisms at every tier from the distribution of the reports directly below that tier alone. It also gives the seller's reserve after the network has transformed the buyers' values. Every later result of the paper is stated at this equilibrium. Examples are the profit ratios along chains with generalized Pareto values, the effect of market size, and the comparison of network shapes. Without the characterization each of these would need its own strategic analysis.
The paper proves the result on paper; none of these statements has a machine-checked proof yet. Formalizing it means building a finite tree auction with threshold payments and laws of maximum reports. It also needs virtual values for laws on unbounded supports and with an atom at zero, and Myerson-type reserve optimality for such laws. The last two are standard tools of auction theory that are absent from Mathlib in this generality.
In a single second-price auction, truthful bidding is dominant and the reserve is the only choice. An intermediary is different. Its report changes its chance of winning upstream, while its reserve and reporting function change what it can charge downstream. So the local second-price argument does not settle its choice. In a tree, a deviation must also be evaluated after arbitrary upstream histories, including reporting functions that are flat on intervals or jump. There, ties and payment thresholds matter. The paper's closed payment formula (2) can disagree with the minimum report that actually wins under a fixed tie rule. With that formula, a deviation with a jump beats , so the theorem would be false. The anticipated reports also carry an atom at zero from tier on, so the one-stage lemma is needed in its atom version.
Laws are probability measures on ; is the pushforward of a product measure under . The density is the derivative of the cdf, read only at , where it also gives the virtual value of the positive part. The support of a positive part is the interval , and "" means . The general objects (virtual value, projection, regularity, reserve objectives) are a separate definition module, reusable beyond this mission.
The tree has buyers with a product law. A report below the reserve is no report, which is never allocated. Ties go to the lowest index, and a report equal to a reserve wins. Payments are minimum winning reports. Buyers report truthfully (Lemma 2.1(B)). The seller's reserves range over , and in Lemma 3.1 the competing bid is independent of the buyers. Strict increase of is an explicit hypothesis: Assumption 3.1 starts at tier , but and Lemma 3.1 need it at tier .
Expected profits are single integrals of realized profits. The equilibrium profit is nonnegative pointwise, so a non-integrable deviation never violates the inequality. Deviations range over all of , and histories over all upstream mechanisms and reserves, so the equilibrium cannot hold for want of competitors. With rate-one exponential values and one intermediary with one buyer, the intermediary earns . Proofs of any milestone, and the measure-theoretic groundwork (measurability of , laws of maxima, Myerson's reserve on unbounded supports), are welcome.
A game option (or Israeli option, introduced by Kifer, Game options, 2000) is an American option whose seller may also cancel the contract at any time, paying the exercise payoff plus a penalty. Pricing it is a Dynkin game: a zero-sum optimal stopping game in which the buyer chooses an exercise time to maximise the discounted payoff and the seller chooses a cancellation time to minimise it. Such contracts model, for instance, a public concession that the granting authority may revoke against compensation.
In the classical theory the drift of the underlying asset is known. De Angelis, Gensbittel and Villeneuve (arXiv:1705.07352v4, 2019; Mathematics of Operations Research, 2021) study the perpetual game call option when neither player knows whether the asset pays a dividend: the return is with an unobservable . Both players learn about only by watching the price. The paper's headline results are that the game has a value, that the value is globally , and that under explicit conditions on the parameters the game has a Nash equilibrium in pure strategies given by entry times into the two players' stopping regions. This mission formalizes the equilibrium result for the case .
Timeline. Kifer (2000) introduced game options. Ekström and Villeneuve (AAP 2006) proved existence of the value for one-dimensional diffusions without uniform integrability and analysed the perpetual call with . Ekström and Peskir (SICON 2008) proved existence of the value and of Nash equilibria for Markov processes under uniform integrability. Yam, Yung and Zhou (Game call options revisited, Mathematical Finance, 2012) treated the perpetual call with a known dividend (). De Angelis, Gensbittel and Villeneuve (2017–2019) treated the case with an unknown dividend, .
Fix a discount rate , a dividend jump , a volatility , a strike and a penalty , and set and . On a probability space carrying a Brownian motion and an independent random variable with , the asset is
The players observe only : their stopping times are stopping times of , the filtration generated by and augmented by the null sets, with values in . For such (buyer) and (seller) the expected payoff is
with payoff on . The upper value is and the lower value . A saddle point is a pair with for all .
The filter is the players' posterior belief that a dividend is paid; it has the closed form with the likelihood ratio of the observed path. The pair is Markov. With the value, the stopping regions are (buyer) and (seller), and the entry times are
Finally . In the coordinates one has , so the sign of decides whether this time-like variable increases or decreases.
Under Assumption 7.1, , and : for every and ,
The goal asserts the shape of the equilibrium (entry times into the model's own stopping regions), with no constant to be improved.
In attack order: the filter identity (§2, p. 5); the regularity of (Lemma 3.1); the value, the seller's optimality, and the super- and submartingale properties (Theorem 3.2); positivity of (Remarks 3.3); the location of the stopping regions (Proposition 4.1, Lemma 4.2 (i), (iii)); the boundaries (Corollary 4.5) and finiteness of (Lemma 4.6); the parabolic change of coordinates (5.1)–(5.4); connectedness of the regions in parabolic coordinates (Lemmas 5.2, 5.4); the boundary of (Corollary 5.5, (5.20)); and positivity of (Lemma 7.2).
The result. Existence of the value does not give an equilibrium: without uniform integrability the buyer's natural candidate may fail to be optimal, and in the complete-information case the pair is indeed not a saddle point (Proposition C.1). Proposition 7.3 shows that partial information about the dividend restores a pure-strategy equilibrium when , and identifies it: each player stops on entering their own stopping region, which is described by monotone free boundaries. This makes the option's hedging and cancellation policies explicit.
Formalizing it. The result is proved on paper; nothing of it is machine-checked. The mission provides a Lean model of a continuous-time game with an unobservable parameter, built from Mathlib's Brownian motion, stopping times and martingales, and a decomposition of the proof into the paper's own lemmas. The theory the proofs use (optimal stopping games for Markov processes, Itô's formula, Girsanov's theorem) is largely absent from Mathlib.
The obvious argument fails at the buyer's side. The seller's optimality comes with the value (Theorem 3.2); for the buyer one needs for every , i.e. that the submartingale can be sampled at . The payoffs are not uniformly integrable (), so optional sampling cannot be applied directly and the term must be shown to vanish. That requires a pathwise bound on the price before , which in turn needs the geometry of in both coordinate systems, monotonicity of (), and strict positivity of the boundary (Lemma 7.2, which needs ). Theorem 3.2 itself rests on the Ekström–Peskir theory of Markovian Dynkin games applied to a degenerate two-dimensional diffusion.
filter_condexp ties to and records its observation measurability and continuous paths, while eq_5_3 ties the encoding to the paper's coordinates .Setting carries a measure , a Brownian motion with all paths continuous (a continuous modification), and uniform on independent of ; then realises every prior on one space, so is defined at every state.WithTop ℝ≥0, so infinite stopping times are allowed.lintegral) in , with payoff on ; , and as a real number (finite since ).hittingAfter … 0 into and , equal to if never reached.Call centres and hospital wards are run in the Halfin–Whitt regime: the number of servers exceeds the offered load by a margin of order , so that delays are short and servers are nearly always busy. With several customer classes, the operator must also choose a scheduling policy: which waiting class is served next. In the diffusion limit, every such policy becomes a control of an -dimensional piecewise-linear diffusion (Atar, Mandelbaum and Reiman 2004; Harrison and Zeevi 2004). Ergodic control of this diffusion, and the justification that its optimal policies are asymptotically optimal for the queues, both need the diffusion to be stable under every admissible policy, with bounds that do not depend on the policy.
A. Arapostathis, H. Hmedi and G. Pang (arXiv:1812.03528v3) prove that positive spare capacity alone gives this: the limiting diffusion is exponentially ergodic, at a rate and with constants that are uniform over all stationary Markov controls.
Timeline.
Fix classes, service rates , abandonment rates , and write , , , . Control values lie in the simplex ; is the fraction of the queue made up of class . The spare capacity is . The controlled drift is
and the diffusion is with a constant positive diagonal and a standard Brownian motion . The generator under the control value is .
A stationary Markov control is a Borel map , used as ; the class is . Its transition probability is , the law of started at . An invariant probability measure satisfies .
The Lyapunov function is built from the convex cut-off ( on , on ): for ,
For a weight , the -norm of a signed measure is .
Assume , and . Then there is such that for every there is with
and there are such that, for every , an invariant probability measure exists with
The rate and the constant do not depend on the control: that uniformity is the content of the theorem.
The result. Uniform exponential ergodicity makes the ergodic control problem for the multiclass Halfin–Whitt diffusion well posed over all stationary Markov policies: invariant measures form a tight family with uniformly integrable exponential moments, and long-run averages converge at a policy-independent geometric rate. In the paper it is the base for the prelimit results of Section 3, where the drift inequalities of Lemma 2.1 are compared with those of the -server queues. With the condition is sharp, since gives transience under every Markov control (Arapostathis, Pang and Sandrić 2019).
Formalizing it. The theorem is proved in the paper; none of it is formalized. The mission produces a machine-checked version with two printed slips corrected (see Formalization scope). Its analytic half, Lemma 2.1, (2.13), (2.10), (2.31) and the Foster–Lyapunov equation, is finite-dimensional calculus and is reachable now. The probabilistic half needs Itô's formula for SDEs with additive noise, existence and uniqueness for SDEs with Borel drifts, and a Harnack-type minorization, none of which Mathlib has.
The control enters the drift only through , but a Markov control may switch arbitrarily, so no single linear or quadratic Lyapunov function works for all policies; Dieker and Gao's common quadratic Lyapunov functions cover one static priority only. The function mixes an -scaled workload term with a -weighted idleness term, and the drift inequality must hold on both half-spaces and with explicit constants, which forces case splits over the classes with and .
For part (b), a Foster–Lyapunov inequality alone gives ergodicity for each control but not a control-independent rate: the constants of the standard Meyn–Tweedie argument depend on a minorization on a small set, and that minorization must be shown uniformly over all Borel controls, for which there is no regularity in to exploit.
EuclideanSpace ℝ (Fin m); classes are Fin m; control values are vectors in stdSimplex ℝ (Fin m). The model data is the published ManyServerQED.Scheduling.DiffusionData with its drift ; the SDE equation, invariant measures, generator and weighted total-variation norm use published GPhNGIDiffusion.EMError definitions. The local IsStrongSolution and IsMarkovTransition specify measurable, adapted solutions and their transition laws. The cut-off is the published cutoff.Measure.map returns a junk zero measure, so a local predicate is used here.The Hospital Readmissions Reduction Program (HRRP), created by the US Affordable Care Act and run by the Centers for Medicare & Medicaid Services since 2012, cuts the Medicare payments of hospitals whose 30-day readmission rates exceed a benchmark computed from other hospitals. It is a form of yardstick competition in the sense of Shleifer (1985): a regulator that cannot observe a provider's costs pays it according to what comparable providers achieve. The penalty differs from Shleifer's scheme in three ways: it is scaled by a multiplier that grows as the benchmark readmission rate falls, it is capped, and no bonus is paid for beating the benchmark.
Arifoğlu, Ren and Tezcan (2021) build a game-theoretic model to separate the effect of each feature. Their Proposition 1 isolates the multiplier: with the cap and the no-bonus rule removed (the scheme they call HRRP-I), hospitals still choose readmission rates below the social optimum and treatment costs above it. Medical and policy researchers had argued informally that the multiplier distorts incentives; Proposition 1 is the paper's precise version of that argument.
There are identical hospitals. Patients arrive at each hospital at rate . Hospital chooses a readmission rate and a marginal treatment cost in the action box
and pays an investment cost to reach them. Each admitted patient is readmitted with probability , so the hospital treats patients per unit time at cost each.
Standing assumptions on (p. 10 of the paper): is twice differentiable, decreasing in each variable, and jointly convex; on ,
where subscripts denote partial derivatives.
The regulator's objective is the social welfare
where is a fixed total patient utility. A maximizer of over is the first best (Lemma 1 of the paper: it exists, is unique and is interior).
The regulator observes every hospital's cost, readmission rate and investment, and computes the yardsticks
Under HRRP-I hospital receives
and earns the profit . The factor multiplying the excess readmission rate is the multiplier. An equilibrium is a pure-strategy Nash equilibrium: a profile of actions in from which no hospital can raise its profit by changing its own action within . A symmetric equilibrium is an equilibrium in which every hospital plays the same action.
For every :
and for every equilibrium is symmetric.
The goal is the conjunction of milestones 2–4; Lemma 1 supplies the comparison point.
Proposition 1 is the paper's first main result and the base for its later analysis: the capped scheme HRRP-II and the actual HRRP (Propositions 2 and 3) are studied relative to the HRRP-I symmetric equilibrium, and the remedy the paper proposes (m-HRRP, Proposition 4) removes the multiplier precisely because Proposition 1 identifies it as a source of distortion. The ordering says that hospitals over-invest in readmission reduction; says that, as a consequence, they under-invest in reducing treatment costs.
The paper's proofs are in its online appendix, which is not part of the source this mission cites (the authors' accepted manuscript, LBS Research Online eprint 1402). No machine-checked proof of any statement of the paper is known. The mission produces a checked version of the model and of all three claims of Proposition 1; the two-hospital claim in particular has no published argument in the cited source.
Lemma 1 is the routine part. The ordering claim is harder: a symmetric equilibrium need not be interior (in simple examples ), so the first-order conditions of the hospital's problem hold only as variational inequalities on , and the comparison with must work from those inequalities and the curvature hypotheses alone. The existence claim needs a fixed-point theorem for the best-response map of a hospital facing yardsticks , and therefore continuity of the best response, which rests on strict concavity of the hospital's profit; Brouwer's theorem is not in Mathlib. The two-hospital claim is a uniqueness-type statement about a two-player game with non-separable payoffs; the obvious route through contraction of the best-response map does not follow from the stated assumptions without further estimates.
The Lean development lives in the namespace ReadmissionsHRRP.HRRPI. A Model carries lam (, a Lean keyword), V, the box bounds and the curried cost R r c. Partial derivatives are deriv of the sections of R. Profiles are maps Fin N → ℝ × ℝ (first coordinate , second ); the averages divide by the real number . The equilibrium notion is the published pure-Nash relation CarbonDoubleCount.Planner.IsPureNash, with every hospital's feasible set equal to ; deviations keep the other hospitals' actions, so the yardsticks of the deviating hospital do not move.
The standing assumptions are one predicate, Model.Standing: the inequalities on the box bounds, (implicit in the paper), of class on an open set containing , non-increasing in each variable on , jointly convex on , and the two pointwise curvature conditions on . The paper's Appendix A, which imposes boundary conditions "to ensure that optimal actions are interior", is not in the cited manuscript; it is replaced by the separate hypothesis Model.FirstBestInterior, that every maximizer of over is interior. Every theorem assumes .
The first best is a maximizer of over , never a solution of the first-order conditions; the ordering claim quantifies over every such maximizer, and the existence claim is part of the goal so that the ordering claim is not vacuous. A sorry-free sanity file checks that the hypotheses are jointly satisfiable for , , .
Useful infrastructure: strict concavity on a box from a Hessian condition, variational inequalities at constrained maxima, continuity of argmax maps, and Brouwer's theorem on a planar box (proved on the platform as AGT.brouwer_fixed_point). Contributions to any of these, or to the hand proofs of the separate claims, are welcome.
The apparel industry produces far more garments than it sells. A large part of its environmental footprint comes from overproduction: inventory made against uncertain demand and then burned, landfilled or downcycled. Mass customization (MC), where a garment is made to order after the customer specifies it, is often promoted as a remedy. Under MC, supply matches demand exactly for the products it makes.
Alptekinoğlu and Örsdemir (MSOM, 2022; SSRN 3685235) ask whether this intuition survives once the firm's profit motive is taken into account. A firm that adopts MC does not abandon mass production (MP). It runs a hybrid system and re-optimizes its mass-produced line around the new option. The paper characterizes exactly when adopting MC is a win-win, meaning more profitable and better for the environment, and when the hybrid firm ends up overproducing more than the pure MP firm would.
Consumers' ideal products are spread uniformly on the Hotelling line . A consumer at distance from a mass-produced product priced gets utility . The total market size is random: with probability , otherwise, where , , and . Units cost , and offering variants costs .
The MP firm chooses the number of variants , the market share of each variant (which fixes the price ) and the stock of each variant before is known. Its expected profit is
The hybrid firm can also make any consumer's ideal product to order, at price , but the consumer then bears a waiting cost . It adds MC share , with , and earns an additional .
The environmental impact counts per sold unit (production, use, disposal) and per leftover unit (production, overproduction):
MC is made to order and leaves no leftovers.
The standing assumptions are , , and . Products are classified by the cost-adjusted value as high-value (), moderate-value () or low-value (). The paper's thresholds are closed-form functions of the parameters (Table 2 of the paper).
Adopting MC is a win-win if and only if
Here "win-win" means that both firms' problems have optimal decisions and that every optimal hybrid decision is strictly more profitable and has strictly lower expected impact than every optimal MP decision.
The result separates the two ways MC changes the footprint. It adds sales, because the gaps between mass-produced variants are now served, and each such sale carries the impact . It also reshapes the mass-produced line: the market served by MP shrinks, each variant captures a smaller share at a higher price, and stocking for the high market size can become profitable (§4.2, pp. 16–17). That raises overproduction even though the MC part produces none. Proposition 3 states exactly when the net effect, together with the profit gain, is a win-win. The paper's policy section (§6) builds on this characterization to study how promoting MC, a disposal fee for overproduction, and recycling move the win-win region.
The paper proves the result by hand, with case analyses across nine orderings of thresholds. No part of the model or its proofs has been machine-checked. A complete development gives a checked solution of a newsvendor-type stocking problem embedded in a Hotelling variety model, which is a common pattern in operations-management research.
Both optimization problems are non-concave. Profit is piecewise in (Lemma 1), and after substituting the optimal stock it is piecewise in , with a kink at and a corner at full coverage . The global optimum therefore switches between four solution types, and the switching thresholds include , a root of a non-polynomial equation. A comparison of first-order conditions alone does not settle which type is optimal. The goal compares two such case analyses, MP and hybrid, at once, so the threshold orderings ( versus , versus , versus ) have to be established across all three product-value classes.
Contributions are welcome on any milestone. The stocking lemmas and Lemma 2 are elementary. The root lemmas need monotonicity analysis of . Propositions 1 and 2 are the bulk of the work.
Approximate counting asks for the number of marked items in a list of items, to within a multiplicative factor , when the marked set can only be accessed through a membership oracle. Brassard, Høyer, Mosca and Tapp (arXiv:quant-ph/0005055) gave a quantum algorithm that uses queries, which is optimal. Their algorithm combines Grover iterations with phase estimation, and so it needs the quantum Fourier transform (QFT). Counting is a basic subroutine in quantum algorithms for estimation, numerical integration and Monte Carlo speed-ups, so the circuit it requires matters.
Aaronson and Rall (arXiv:1908.10846, SOSA 2020) give an algorithm with the same query complexity that uses only Grover iterations and classical post-processing of measurement outcomes. Its analysis is short and elementary, and every constant in it is explicit. This mission formalizes their Theorem 1, the rotation lemma it rests on, and the numbered estimates of its proof (arXiv:1908.10846v6, pp. 4–10).
Timeline (as recounted on pp. 1–3 of the paper):
Let be a nonempty marked set with . The algorithm first pads the list to items, the added items being unmarked, and then works on . The membership oracle is the diagonal unitary . The uniform superposition is , and the Grover operator is
Preparing for an odd costs queries. Measuring it in the computational basis yields a marked item with probability given by the Born rule. With this probability is , so repetitions give a count of marked outcomes.
The algorithm has two loops. Step 1 tries , the largest odd integer at most , for , with measurements per round. It stops at the first at which at least 95% of the outcomes are marked. Step 2 keeps a bracket , initially and . In round it computes from the bracket by the rotation lemma (Lemma 2):
It then measures times, with , and shrinks by the factor : it raises if at least 12% of the outcomes are marked and lowers otherwise. It stops once and returns .
For nonempty , :
In the order of the proof:
Theorem 1 shows that the optimal query complexity of approximate counting is achieved without the quantum Fourier transform. The circuits involved are powers of the Grover operator followed by computational-basis measurements, and the classical control is a pair of loops with explicit thresholds. The same argument gives QFT-free amplitude estimation (Theorem 3 of the paper), and its rotation lemma is a reusable tool for any algorithm that brackets a rotation angle by biased coin tosses.
The result is proved on paper but not formalized. The platform has Grover's iteration for a single marked item; it has no Grover state for a marked set, no counting algorithm and no query-complexity statement of this kind. A complete development would provide a machine-checked quantum query algorithm whose output law is derived from the Born rule and the actual Grover operator. It would also provide a Chernoff bound in Kullback–Leibler form for the binomial distribution, which Mathlib does not have.
The deterministic estimates are elementary but numerous, and each constant (0.96, 7.5%, 16.5%, 1.102, 0.27, 0.42) must be checked against interval arithmetic for and . Two printed steps are numerically loose, (8) and (26), and must be replaced by correct intermediate values.
The probabilistic part has two difficulties. First, the success event of step 1 is not a single tail bound. Termination too early is controlled by a union bound over rounds , and the additive Hoeffding bound is too weak there: it needs the KL form (13). Second, step 2's output law is defined by a recursion whose bracket is random, and Lemma 2 applies to a round only while the bracket still contains . The union bound over rounds has to be carried through this recursion. Third, the paper bounds the queries only on its "ideal" event. Part 2 of the goal requires the bound on every run that ends with an accurate estimate, including runs in which step 1 stopped late.
Fin N' → ℂ, operators are Matrix (Fin N') (Fin N') ℂ, and is vecMulVec ψ (star ψ). The padding embeds Fin N as the first indices of Fin N'.approxCount N S ε δ F : PMF (Option (ℝ × ℕ)) is defined, not quantified. Its outputs are some (K̂, queries), or none when either loop runs out of its fuel F. Fuel exhaustion counts as failure. Measurement counts are Mathlib's binomial law with the Born probability computed from , and .round breaks ties upward, a choice the paper permits. The step-2 threshold is "at least 12%", as in the algorithm box; Lemma 2 is stated for both "more than" and "at least".Contributions of reusable infrastructure are welcome, in particular the KL-form Chernoff bound for ProbabilityTheory.binomial and lemmas on powers of a reflection product acting on a two-dimensional invariant subspace.
New brand-name drugs, in particular biologics, are expensive. Their benefit is also uncertain: a given patient cannot know in advance whether the treatment will work for her. Outcome-based pricing (also called performance-based or risk-sharing agreements) responds to this. The manufacturer is paid only when the treatment reaches a pre-specified goal and rebates the price otherwise. Agreements of this kind between manufacturers and payers have been signed for cholesterol, diabetes and oncology drugs. Carlson et al. (2010) give a taxonomy. Whether such a contract actually helps the parties that must agree to it is a question about incentives. It cannot be settled by noting that the patient bears less risk.
E. Adida (Management Science, 2021; accepted manuscript at eScholarship) studies it in a three-stage game between a monopolist firm, a payer and risk-sensitive patients. The patients follow prospect theory (Kahneman and Tversky 1979; Tversky and Kahneman 1992). The paper's headline result is that, in the region where the payer covers the drug under both systems, the firm and the payer typically disagree about outcome-based pricing. A side payment from the firm to the payer can make both strictly better off, but only for high-risk drugs. This mission formalizes that result and the chain of equilibrium computations that leads to it.
There are patients with values , , a unit cost , a co-insurance rate and a success probability . On success the payer gains a fixed surplus . The game has three stages.
Under uniform pricing the price is paid on every purchase, and the buyer's welfare is . Under outcome-based pricing it is paid only on success, and the welfare is . Demand is times the measure of buyers in . The firm earns per buyer under uniform pricing and under outcome-based pricing. The payer's objective is its own expected payoff plus the patients' total expected (risk-neutral) payoff. It covers iff its objective with coverage is at least its objective without. An equilibrium price maximizes the firm's realized profit, with the payer's coverage response, over all .
Let
A drug is high-risk if and low-risk if ; the risk premium is positive exactly for high-risk drugs. Assumption 1 is . Assumption 2 is
with , , and the solution of . It is the region of large payer benefit, in which both systems end in coverage. Finally,
Under Assumptions 1 and 2, let and be equilibrium prices, and write and . Then
and, if and , : every transfer strictly between the two amounts, which runs from the firm to the payer, works.
In attack order:
Proposition 4 says that for a high-risk drug outcome-based pricing raises total firm-plus-payer surplus, even where it hurts the payer. A negotiated side payment therefore always exists that makes both parties prefer it. For a low-risk drug no such payment exists, because the payer's gain is smaller than the firm's loss. The result locates where outcome-based contracts can be self-enforcing and identifies the risk premium as the quantity that decides it. In this model the patients' loss aversion and risk sensitivity act on the comparison only through and .
The paper proves the result with explicit algebra once the equilibrium is pinned down. The formalization adds two things. First, the equilibrium layer is checked, not assumed: the statements quantify over the backward-induction equilibrium prices, with an explicit payer coverage rule and an integral model of demand. The closed forms and the unique optima , become theorems. Second, the formalization makes the small hypotheses explicit (positivity of , non-negativity of , strict versus weak improvement), which the published proof uses without listing. As far as is known, none of these results has a machine-checked proof.
The algebra of Propositions 3 and 4 is short once and with coverage are established. The work is in establishing them. The firm's realized profit is a discontinuous function of the price, because the payer's coverage decision switches at the thresholds , , , , which depend on the regime of . Showing that is the unique global maximizer requires comparing the covered and uncovered profit curves on every piece. It uses Assumption 1, the bound (which places above and above ), and the monotonicity of through the root of . Reading the closed forms off the paper's formulas is not enough: they must be derived from the purchase rule, which itself rests on the prospect-theory inequality . A natural shortcut is to state Proposition 4 at and directly. That deletes the equilibrium content and is not the goal.
All quantities are real numbers in one structure Params with a Standing predicate: , , , , , . Two of these are added to the page's assumptions: ( divides by ) and (used in the proof of Theorem 1).
Powers are Real.rpow on non-negative bases only. The roots (of ), (of ) and (of ) are passed as numbers together with their defining equation on ; uniqueness is a milestone. Demand and patient payoff are a Lebesgue measure and a set integral over the buyers in . Ties follow the paper: an indifferent patient buys, and an indifferent payer covers. "The firm prices at " is read as " is the unique equilibrium price". "Better for both parties" is read as strict improvement, and the paper's closed range of transfers is replaced by the open range, because at its endpoints one party is only indifferent. The payer's side of every comparison is its objective .
A formalization that fixes and by hypothesis, or takes the closed forms as definitions, would make the goal an algebraic identity. The goal here quantifies over all equilibrium prices of the integral model.
A complete development needs elementary real analysis (convexity and monotonicity of , rpow manipulations), Lebesgue measure and integrals over intervals, and piecewise maximization of concave quadratics. The prospect-theory value function and the threshold purchase rule are reusable for other behavioral pricing models. Proofs of any milestone are welcome, as are proofs of the omitted parts of Theorems 1 and 2 (the constrained prices , , , ).
The circular economy movement argues that manufacturers should keep control of their products after use (by leasing instead of selling) and design them so that worn parts can be replaced individually (a modular architecture). Each of the two levers has a long literature in operations management and economics. Leasing versus selling durable goods is studied in models of durable goods with secondary markets (Desai & Purohit 1998; Agrawal, Ferguson, Toktay & Thomas 2012), and modularity in the product-design literature, where its value lies in replacing modules independently. Agrawal, Atasu and Ülkü (Management Science) ask whether the two levers reinforce each other: when is leasing a modular product strictly the most profitable of the four combinations of business model and architecture? Their answer (Proposition 3) is a closed-form partition of the parameter space by cost thresholds, and it shows that the combination is optimal only under limited conditions.
A monopolist offers a durable product made of two modules, each with a useful life of two periods; module 1 is the more durable one. A customer of type , uniform on , values a new product at per period. Under selling, a used module retains a fraction of its value; under leasing, off-lease modules retain , where is the relative return condition (: off-lease products are in worse shape than previously sold ones; : in better shape). Each module costs to produce. The standing assumptions are
In steady state the firm solves one of four quadratic problems, each written in quantities through inverse demand functions derived from customer self-selection and secondary-market clearing:
The optimal profits are the attained maxima of these problems. The paper's thresholds are explicit functions of :
together with , , and the square-root expressions , of the Appendix.
With ties between architectures broken towards the integral one (footnote 13 of the paper):
In each region the chosen option's optimal profit strictly exceeds the others, except at exact ties of the model. These are for , for , , and at further ties between leasing and selling. The goal states these as equalities or weak inequalities and restores strictness for .
The result gives a complete description of the firm's joint choice in a standard durable-goods model with a secondary market, and it qualifies a common claim. Leasing a modular product is strictly optimal only at low production cost. For modularity can even push a leasing firm to selling (Proposition 2), and for the firm never sells. The thresholds feed the paper's later environmental and consumer-surplus comparisons.
The paper's proofs are pencil-and-paper KKT computations reported in compressed form, and nothing in the paper is machine-checked. A formalization would certify the four closed-form optima, every threshold comparison, and the case split of Proposition 3. It would also settle two printing errors found while preparing this mission (see below), one of which changes the statement of Lemma 2 and Proposition 3.
Each firm problem is a strictly concave quadratic program over a polyhedral cone, so existence of the optimum is routine. The difficulty is everything after that. The optimum changes face as moves: LM alone has four KKT cases, and each must be shown to be optimal exactly on its cost interval. The profit comparisons then reduce to sign conditions on rational functions of four parameters. Some involve the square roots in and , which are only meaningful for and are defined as roots of quadratics in , so the comparisons must be placed relative to them. The ordering is an inequality between such expressions on the whole parameter region. It is not a symbolic identity, and checking it at sample points proves nothing.
IsGreatest (profit '' feasible) v, never a supremum without attainment. Statements about the optimizer ("the UN segment exists", "") quantify over every optimal decision.Real.sqrt for , , , . and are used only for , where their radicands are nonnegative.Manufacturers of products with fixed shelf lives must decide both how much to send from a warehouse to a store and which age cohorts to send. A shipment can reduce expiry at the warehouse while changing the age mix seen by shoppers at the store. In the two-echelon system studied by Akkaş and Honhon, the store does not control which items each shopper takes: some shoppers select older items first and the remainder select newer items first. The resulting waste at the warehouse and store can move in different directions when the manufacturer changes a shipment. The paper uses this setting to ask whether ship oldest first (SOF), a simple age-selection rule, minimizes waste over an infinite horizon. Akkaş and Honhon, SSRN manuscript.
The paper reports an inventory-age audit of a consumer packaged goods supplier and then studies the shipment decision analytically. Its Theorem 1 separates warehouse waste from the sum of warehouse and store waste. The former has a specified SOF policy that ships in full; the latter has an SOF age-selection rule but allows the shipped quantity to vary with the state. This mission formalizes those two claims, with a correction to one printed clause described below. Akkaş and Honhon, §3 and Theorem 1.
A unit remains saleable for periods, where . At the start of a period the warehouse holds units of age , and the store holds units of that age, for . Both age-zero entries are zero before replenishment. A plant then delivers fresh units so the warehouse's total post-replenishment stock reaches the exogenous order-up-to level . Thus its age-zero stock is . The manufacturer sends units of age from the warehouse to the store, subject to warehouse availability and the store's shelf capacity . In particular, and . Akkaş and Honhon, §4.1, pp. 10–13, and §4.2, p. 15.
The period's shopper population is . A fraction selects inventory first in, first out (FIFO), meaning older units first; the remaining shoppers select it last in, first out (LIFO), meaning newer units first. The discrete FIFO population is . If is the store stock after delivery, the paper's age-specific demand is
Here . Only units of age expire at the end of the period. Warehouse waste is , store waste is , and total waste is . The remaining units advance one age before the next period. An SOF shipment uses a younger unit only when every older available unit has been shipped. An SOF shipment in full fills the remaining store space or ships the entire available warehouse stock. Akkaş and Honhon, §4.1, pp. 11–12, and §4.2.1, p. 15.
Let and denote the upper and lower limits of expected Cesàro averages of warehouse waste. The first sentence of Theorem 1 is the mission's sole milestone:
The full goal also asserts that one stationary, feasible SOF policy minimizes total waste from every feasible initial state:
The policy chooses its shipping quantity from the current state; the theorem does not prescribe shipping in full for this second objective. These are waste objectives, independent of the paper's separate revenue, labor, and expiration-cost parameters. Akkaş and Honhon, Theorem 1, p. 15.
The warehouse result identifies a fixed, implementable shipment rule for minimizing waste at that location across the paper's whole FIFO/LIFO range. The total-waste result says that optimal age selection can remain SOF even when the quantity decision must respond to the store inventory and shopper behavior. Together they distinguish the two decisions in a setting where moving an expiring unit out of the warehouse can merely move the expiry to the store. The paper later uses its waste comparison in the analysis of profit policies under additional cost assumptions. Akkaş and Honhon, Appendix A.2–A.3.
The theorem is a published paper result, but this mission starts with open Lean statements rather than a machine-checked proof. A complete development would provide a reusable formal model of age-structured two-echelon inventory, stochastic shopper depletion, feasible shipment policies, and long-run waste criteria. The general controlled-process and Cesàro-average definitions can also support other finite inventory models.
An age-selection decision changes the stock carried into future periods, and a quantity decision changes the next warehouse replenishment. A comparison of immediate waste therefore does not by itself compare long-run averages. In particular, simply reordering each shipment to send older units first while keeping its quantity fixed can increase later warehouse waste for some policies; it cannot serve as an unrestricted policy-level argument. The store's FIFO/LIFO mixture introduces another intertemporal effect because a shipped younger unit can be sold ahead of an older one. Akkaş and Honhon, Appendix A.1, Appendix p. 1.
Lean uses finite age vectors indexed by Fin N, natural-number stocks and shipments, a real constrained to , and an arbitrary probability mass function for shopper population. The standing condition makes the final age cohort defined; and remain allowed. Demand samples are independent and identically distributed across periods, as in the stationary transition model of §4.2. Policies are time-dependent deterministic Markov rules: at period they choose a shipment from the current inventory state. This is the finite-state class used by the paper's dynamic program. The comparison includes every feasible rule in that class, every feasible initial state, and a common stationary SOF witness for total waste; it does not restrict competitors to SOF or full shipments. Standard finite-MDP results explain why stationary deterministic optimal policies suffice among broader history-dependent randomized classes. Puterman, Markov Decision Processes, Theorem 9.1.8.
Costs and expectations live in , and long-run criteria use upper and lower limits of expected Cesàro averages. The paper prints a plain limit without specifying what happens when a policy's average fails to converge. The upper-versus-lower comparison states the stronger optimality claim without relying on that convergence. Lean time starts at zero. Natural-number subtraction implements the paper's positive-part operation, and the post-replenishment stock formula is used only for feasible states. The model follows the printed balance equations when discarding the final-age store stock, despite a tension with the narrative timing of expired-unit pickup.
Three transcription corrections are explicit. The demand formula's sums use , the running index, where the page prints ; the action sum runs through age ; and the waste objectives are minimized despite a printed “max” in §4.2.1. More consequentially, Theorem 1's last clause says shipping is in full under pure FIFO. This is false and is omitted: for , , , , and a Bernoulli shopper population, SOF in full has average total waste while an SOF policy that holds stock back attains . The formal goal neither assumes this clause nor asserts its negation. Its feasible-policy and feasible-initial-state quantifiers rule out vacuous or artificially easy readings.
A complete proof may need finite-state inventory invariants, admissibility of the SOF-in-full rule, comparisons of age profiles over time, and results about average costs of controlled chains. Contributions establishing those reusable facts, or the stated warehouse and total-waste targets, are within scope. The separate profit theorems and numerical studies of the paper are outside this mission.
Online platforms show a reader many short signals about the same question (posts, headlines, tweets), more than the reader can absorb. The reader screens the menu and consumes only a few items. Allon, Drakopoulos and Manshadi (Information Inundation on Platforms and Implications, SSRN 3385627; Operations Research, 2021, doi:10.1287/opre.2021.2119) ask what a purely information-seeking reader picks when the accuracy of each post is unknown. Their answer, Proposition 1, is that she picks the post closest to her current belief, the effect the paper calls screening bias. It is the mechanism behind the paper's later results on slow learning and polarization, and it explains a pattern resembling confirmation bias without assuming any bias in how beliefs are updated. Confirmation bias was documented empirically by Lord, Ross and Lepper (1979) and modelled through source reputation by Gentzkow and Shapiro (2006) and Suen (2004). In those models the bias comes from repeated interaction with strategic sources; here it comes from a single screening decision by a Bayesian reader.
An unknown fact is a real number . A post is a noisy observation
where and the accuracy (a standard deviation) is drawn independently from a publicly known law . The paper assumes throughout (§3, p. 8) that is a probability law whose support lies in an interval with .
A consumer holds a normal belief about , with . From her point of view, a post of accuracy is distributed , so its likelihood is
By Bayes rule (4), her posterior on the accuracy after seeing the post value has density proportional to with respect to ; write for the posterior expectation.
If she reads a post and learns its accuracy (ex-post known accuracy), her belief becomes normal with standard deviation (Belief Updating Equations). Before reading, she scores each post by the expected reduction of her uncertainty. The Screening Equation prints the score as
while the text calls it the expected decrease in posterior variance, . A menu is a finite list of post values, and she picks a post in the argmax of the score.
In Lean the model lives in InfoInundation.Screening.Model: AccuracyLaw G (the standing assumption), psi, likelihood, postExp (the Bayes ratio), nextSd, sdScore, varScore, argmaxMenu, closestPosts, and the auxiliary moments auxMoment/auxExp used in the proof.
For every accuracy law satisfying the standing assumption, every belief with and every menu :
(a) if is not a point mass,
(b) if with , the argmax of both scores is the whole menu.
The proof on pp. 10–11 has no numbered lemmas; the milestones are its labelled steps:
Proposition 1 turns a modelling choice (each reader maximizes expected information) into a behavioural prediction (each reader consumes the post nearest her belief). Every later result of the paper is built on it: the slow-learning theorem, in which the speed of learning decreases with menu size, and the multimodal belief distribution, both come from feeding the closest post back into the belief dynamics. Part (b) is the benchmark: with known equal accuracy there is no screening bias, and learning is fast.
The result is proved in the paper; it has no machine-checked proof. The mission produces one, and with it a small reusable library on posteriors over a Gaussian scale mixture: the predictive density of a normal belief under a known noise scale (milestone 1), a measure-theoretic Bayes rule for the noise scale given one observation (milestone 2), and moment inequalities under exponentially tilted mixing laws (milestones 5–6). The formalization also settles two points that the printed proof leaves open (see Difficulty): which of the two scores the conclusion holds for, and why the conclusion is an equality of sets rather than an inclusion.
The proof covers the variance score. Reducing it to the monotonicity of in is algebra. The monotonicity itself requires differentiating a ratio of -integrals under the integral sign, for an arbitrary law , which in turn needs the boundedness of the support to dominate the integrands.
Three places need more than the printed argument:
Measure ℝ with AccuracyLaw G: a probability measure with for some . "Supp() includes at least two distinct values" is ∀ σ, G ≠ Measure.dirac σ; "Supp() = {σ}" is G = Measure.dirac σ with .Z : Fin K → ℝ; argmax and argmin are Finset (Fin K), so posts of equal value are distinct posts, and "" is Finset.univ.Needed infrastructure: dominated differentiation of parameter-dependent integrals against a finite measure on a bounded set (Mathlib's hasDerivAt_integral_of_dominated_loc_of_deriv_le), the equality case of Cauchy–Schwarz in , Gaussian convolution (gaussianReal_add_gaussianReal_of_indepFun) and conditional expectation via densities for milestone 2. Contributions of a covariance or likelihood-ratio ordering lemma for the standard-deviation conjunct are welcome as supporting theorems.
A new venture rarely knows two things at once: whether its core idea is worth anything, and whether the particular way it has chosen to bring the idea to market — its strategy — will work. A failed pilot, a disappointing A/B test or a lukewarm customer experiment can mean either, and the founder cannot tell which. Work on entrepreneurial experimentation (Kerr, Nanda and Rhodes-Kropf, Journal of Economic Perspectives, 2014, doi:10.1257/jep.28.3.25; Gans, Stern and Wu, Strategic Management Journal, 2019, doi:10.1002/smj.3010) treats testing as the main tool founders have to resolve uncertainty before they commit resources.
Agrawal, Gans and Stern (NBER Working Paper 27379, 2020; published in Management Science, 2021, doi:10.1287/mnsc.2020.3920) give a two-period model in which a single test produces a conflated signal about the idea and the strategy together. Two consequences come out of it. A signal that the strategy is good can still lead the entrepreneur to abandon the venture. And when a mentor can sharpen a test, the better direction to sharpen it depends on the founder's prior beliefs. This mission formalizes the model and its two propositions.
The idea is worth (state ) with prior probability , or (state ). Value is realized only if the strategy used is effective (state , against ineffective ). Every strategy is effective with prior probability , independently of every other strategy and of the idea, and there are several strategies to choose from. Implementing a strategy costs and testing one costs . The standing assumptions are
where means that launching a randomly chosen strategy without testing exactly breaks even.
A test of the selected strategy has precisions and emits one of four signals, , , or :
| w.p. | w.p. , w.p. | |
| w.p. , w.p. | w.p. |
Write and for the posterior probabilities that the idea is high-value and that the tested strategy is effective, given signal . Assumption (A1), that tests are weakly informative, requires
After the signal the entrepreneur picks one of three period-1 actions:
is the best of these three conditional values. The value of testing is
The strategy-biased test is and the idea-biased test is , where is the baseline test.
For baseline precisions , if both precise tests satisfy (A1) and
then
The statement leaves and the baseline precisions free, subject only to the standing assumptions.
Proposition 2 answers the question a mentor faces when it can make a test more precise in one direction only. A test with high makes abandoning a poor idea more efficient. A test with high makes it more efficient to continue the idea with a different strategy. The condition weighs these two benefits, and it shows that the choice is driven by the prior . Proposition 1 shows why: the idea is the same in every test while the strategy can change, so switching strategies after an ambiguous signal is how the entrepreneur learns about the idea. The paper's later sections (differing priors between mentor and entrepreneur, §5.2) start from these two results.
The results are proved in the paper by hand-calculation, and Proposition 2 has no printed proof. No part of the model has been machine-checked before. The formalization produces an explicit, reusable encoding of a two-dimensional Bayesian test with a conflated signal, together with machine-checked versions of the case analysis that Proposition 1 summarizes. It also gives a checked replacement for the printed display: the second line of that display does not follow from the first.
The obvious argument reads the paper's prose, takes and as given, and subtracts. In the formal model these values are optima over three actions, computed from the signal table, and each one needs an argument.
The model lives in the namespace EntrepChoice.TestChoice. Params holds . Standing collects the standing assumptions, with kept as the hypothesis rather than substituted. Test holds , and Test.Valid bounds both in . The states, signals and actions are small inductive types, and sums over them are written out explicitly.
Action values are unnormalized: times the conditional expected payoff. With this choice (testValue) needs no division. (A1) is stated cross-multiplied by . It agrees with the posterior form whenever and is harmless when . The posteriors p1 and e1 are real quotients, equal to on a probability-zero signal.
Several conventions are disclosed readings of the paper:
testValue is the maximum over the three period-1 actions, built from the signal table. It is never defined by the closed form of milestone 6, and neither Standing nor A1 mentions it, so the goal cannot be closed by unfolding a definition.
Contributions are welcome on every milestone. Further results of the paper — testing order under irreversibility (§4.1), heterogeneous strategy priors (§4.2) and the mentor–entrepreneur game with differing priors (§5.2) — are natural follow-on missions on the same definitions.
Farmers who sell the same crop can benefit from better forecasts of the market price, but their production decisions also affect one another through the price. A forecast sent to one farmer may improve that farmer’s decision; a forecast sent to many farmers can make their output responses move together. A planner choosing who receives a common forecast therefore faces a question that differs from asking whether the forecast is accurate. Zhou, Fan, Chen and Tang study this question for a public signal about the uncertain intercept of a Cournot market’s inverse demand curve in Information Provision and Farmer Welfare in Developing Economies (SSRN preprint dated June 27, 2019, §§3–4).
The paper’s base model concerns a publicly funded information service. The planner can send the same signal to any number of farmers without charging them, and its objective is the sum of farmers’ expected profits. The target here is the paper’s Proposition 2, which says that the planner should inform either exactly one farmer or none, according to the sign of an explicit polynomial in the model’s signal precisions and number of farmers. The statement is about equilibrium production choices and the resulting profits, rather than about forecast quality alone (Zhou et al., pp. 11, 14).
There are farmers producing the same good with deterministic yield. Farmer chooses a quantity and pays . The total harvest is , and the inverse demand at sale is , where is market potential, measures price sensitivity, and is a centered Gaussian demand shock. Farmer earns . The quantities in this formalization are real valued, as required by the paper’s affine equilibrium formula; this interpretation is explained below (Zhou et al., p. 8, (1); p. 10, (2)–(3)).
Each farmer sees a private signal . The are independent centered Gaussian noises of common precision ; the shock has precision . Thus their variances are and . A planner also observes a public signal , where the independent Gaussian noise has precision and variance . The planner chooses an informed set of farmers who may see ; every farmer sees only its own , and an uninformed farmer cannot use . Write , so is an integer from zero through (Zhou et al., pp. 8–9).
A farmer’s strategy is a measurable function of the information available to that farmer. The realized quantity must be square-integrable under the joint Gaussian law. A Bayesian Nash equilibrium is a profile of such strategies in which no farmer can increase ex-ante expected profit by changing only its own admissible strategy. Write for the sum of the expected profits of all farmers at a profile . Proposition 1 gives a linear equilibrium and its almost-sure uniqueness. Lemma 2 gives the ex-ante profit of each informed and uninformed farmer at that equilibrium (Zhou et al., pp. 12, 14, 34).
The goal is the equilibrium welfare conclusion of Proposition 2. Let be the explicit polynomial displayed in that proposition, with also fixed by the model. For every informed set, an equilibrium exists. When , every one-farmer informed set strictly outperforms all sets of another size. When , the empty informed set is optimal; for it strictly outperforms every nonempty set:
At , informing zero and one farmer gives the same welfare, so the second case asserts that zero is an optimal choice rather than the unique choice. The goal compares for every Bayesian Nash equilibrium of each informed set, allowing any subset of the prescribed size (Zhou et al., p. 14, Proposition 2; p. 36).
The milestone statements follow the claims used for that result: Lemma 1’s two Gaussian posterior identities; Proposition 1’s equilibrium existence and almost-sure uniqueness; Lemma 2’s profit formulas and advantage for informed farmers; and the Appendix A claims that welfare declines after two recipients, one recipient beats two, and the sign of is controlled by (Zhou et al., pp. 10, 12, 14, 35–36). Here is the paper’s closed-form welfare expression for the linear equilibrium, extended from integer to real only for the paper’s continuous analysis.
The result identifies the welfare-optimal reach of a common forecast in a competitive production market. Under the stated model, informing more farmers does not necessarily raise their aggregate expected profit. The threshold decides whether the planner should send the signal to one farmer or withhold it. Proposition 1 and Lemma 2 are needed to connect that policy claim to farmers’ actual equilibrium decisions, rather than to a free-standing polynomial comparison (Zhou et al., pp. 12–14).
The paper proves the result mathematically. This mission asks for a machine-checked development of the Gaussian signal model, the equilibrium result, the profit identities, and the final optimization statement. The Gaussian posterior and square-integrable game infrastructure can be reused in other information provision models. The proposal statements compile, but their proofs are open; no machine-checked proof of these mission claims is asserted here.
The planner can compare policies only after accounting for how all farmers change production when the public signal is shared. Informed farmers use both their private observation and the common signal, while uninformed farmers use only their private observation; the same signal changes both the informed farmers’ expected profit and the Cournot price faced by everyone. The linear equilibrium formula alone does not justify restricting all possible strategies to linear ones. The proof must establish that it is an equilibrium against every admissible deviation and that any equilibrium gives the same realized quantities almost surely. The integer policy choice must then be related to the paper’s real extension without allowing noninteger informed sets (Zhou et al., pp. 32–36).
Lean represents the uncertainty by a product of independent Gaussian measures for , the private noises, and the public noise. The variances are the reciprocals of the positive precisions , , and . Informed sets are finite subsets of Fin n, including the empty and full sets. The observation map gives to a member of and to a farmer outside , so neither type sees another farmer’s private signal. Strategies are measurable functions with square-integrable realized quantities, and both equilibria and deviations satisfy that condition. Welfare is the sum of integrals of realized Cournot profit. The goal quantifies over all equilibria and does not replace their welfare by the closed-form function .
The base game assumes , , , and positive ; no sign condition is imposed on . The paper mentions as an unavailable-private-signal limiting case, but a Gaussian noise with variance is undefined there, so that separate regime is outside this mission. The positive public precision likewise excludes the degenerate case. Equations (2)–(3) print , but the claimed affine equilibrium takes negative values with positive Gaussian probability; the formalization uses unrestricted real quantities, which is the game solved by the paper’s displayed first-order calculations. All of these choices are explicit in the statements and should be checked against the source’s intended reading (Zhou et al., pp. 8–10, 12).
The coefficient definitions , the linear profile, the two type-specific expected profits, and are fixed to the source displays. The useful contributions are proofs of the posterior identities, unrestricted equilibrium existence and uniqueness, expected-profit identities, and the welfare inequalities. Neither an arbitrarily chosen equilibrium nor an affine-only strategy class would establish the target.
A buyer may be liable for social responsibility violations among suppliers that remain in its production network. Auditing can prevent a later penalty, but the buyer must pay for each audit and then choose what to do with a supplier that fails. Dropping a supplier can also remove other firms that depend on it, changing the buyer's eventual production profit. Zhang, Aydin, and Parker study this decision in a three-tier supply network and establish a structural rule for an optimal auditing policy in Theorem 3. The rule tells the buyer how dropping and rectification can be ordered without specifying which supplier to audit first.
There is one buyer in tier 0 and two possible tier-1 firms, and . The tier-2 suppliers are divided into three disjoint sets: , whose members supply only ; , whose members supply only ; and , whose members supply both. A network is , where is the set of tier-1 firms still present. Its supplier set contains those tier-1 firms and the members of the three tier-2 sets. The set of dependents of supplier includes itself. For a tier-1 firm, it includes its exclusive tier-2 suppliers. For a tier-2 supplier, it also includes a tier-1 firm if that supplier is the firm's sole remaining tier-2 source.
An auditing state records the current network and its finite set of unaudited suppliers, . The state is terminal when . The operator vets an unaudited supplier without changing the network. The operator drops and . If a tier-1 firm is dropped, its formerly shared tier-2 suppliers become exclusive to the other tier-1 firm. These transitions are the paper's footnotes 3 and 4 on page 10.
At a state, the buyer can proceed to production (), audit and rectify an unaudited supplier (), or audit and drop one if it fails (). An auditing policy chooses an admissible action at every state. Let be the audit cost, the rectification cost, the chance that a supplier is noncompliant, the chance that an uncorrected violation is exposed, and the penalty for an exposed violation. If the buyer proceeds to production, it receives production profit less the expected penalty .
The optimal value is the maximum of the values of the admissible actions at , using the finite recursion (1)–(5) of §3.2. An optimal policy chooses a maximizing action at every state. The appendix also defines the value of a fixed policy and the restricted value when only and are available.
The main target is Theorem 3, page 19: some optimal policy first audits and drops any number of suppliers, perhaps none, and then enters a second subphase. In that second subphase it either rectifies all remaining unaudited suppliers, in any order, or proceeds directly to production. The choice is governed by the comparison
The inequalities are non-strict: both choices are permitted at equality. The statement applies at every state of the auditing process. Once the policy rectifies a supplier, it rectifies another at the successor state whenever unaudited suppliers remain; no later audit-and-drop action follows. Every available rectification action is optimal during this subphase.
Two appendix results are the milestones. Proposition D.1, OA-11 says that, for each starting state, a buyer can postpone rectification actions until after dropping actions without lowering its value at that state. Proposition D.2, OA-13 identifies the optimal value and actions in the restricted rectify-or-produce problem. With , its value formula is
Theorem 3 reduces the form of policies that need consideration: rectification need not be interleaved with later dropping, and the final choice between rectification and accepting exposure risk depends on one comparison of per-supplier costs. It does not resolve which suppliers to audit and drop, or when to leave that first subphase. Those decisions can still depend on the network and audit outcomes, as §5.1 explains.
The paper proves the structural result and its two appendix propositions. This mission asks for machine-checked proofs of those known statements, together with a reusable finite representation of network dependents, transitions, and Bellman values. The present draft statements compile with proof placeholders; they are not machine-checked proofs of the claims. The definitions also permit later work on other auditing rules over the same state space.
An audit-and-drop action can change the network and therefore production profit. Comparing it with an audit-and-rectify action is more involved than comparing their immediate costs: a dropped supplier can remove its dependents, and those losses affect all later decisions. The obvious choice of rectifying whenever ignores the possibility that a later drop removes the rectified supplier anyway. The structural theorem must account for both successor states of an audit and still produce one policy that is optimal at every state.
Tier-2 suppliers carry labels in an arbitrary type, while every individual network and unaudited set is finite. The tier-2 components of a network are pairwise disjoint. The Lean parameters explicitly require , , and . The paper derives from independent supplier outcomes; the formalization uses that derived formula, and its Bellman recursions already take the audit outcomes' expectations. The profit is any real-valued function of the current network. This is a disclosed generalization of the Cournot profit used earlier in the paper: §6.1 says the two-subphase result does not depend on the mode of competition, and (D.27) uses only that vetting leaves the network unchanged.
The value functions are defined by recursion on the number of unaudited suppliers. Their maxima are taken over exactly the admissible finite action set, and optimality is checked at every state. Transition functions are total, but the theorems use them only for unaudited suppliers. The action-value functions return zero for inadmissible supplier actions; the fixed-policy recursion returns the production value there. These values have no role for admissible policies. The formulation excludes an unattained policy supremum, a policy that is optimal only at a chosen initial state, or a special production-profit function. Contributions that establish the appendix propositions, the main structural theorem, or useful lemmas about the finite transitions and recursions fit this scope.