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?
Diversification is the oldest prescription of decision theory. Bernoulli (1738) used the example of a merchant, Sempronius, who can send his goods on one ship or split them over two ships, and showed that an expected-utility maximizer with concave utility prefers to split. Portfolio choice, insurance and supply-chain sourcing all rest on the same principle: when the risk of loss is known, spreading exposure helps a risk-averse decision maker.
Most real diversification decisions are made without knowing the probability of loss. A common intuition in the ambiguity literature holds that ambiguity aversion, a dislike of not knowing the probabilities, should add a second motive to diversify on top of risk aversion. Epstein (2010) and Klibanoff, Marinacci and Mukerji (2012) debated whether the smooth ambiguity model of Klibanoff, Marinacci and Mukerji (2005) captures a preference for diversification at all.
Berger and Eeckhoudt (iRisk Working Paper 2021-iRisk-02; Management Science 67(3), 2021, doi:10.1287/mnsc.2020.3823) return to Bernoulli's two-ship problem with two experts who disagree about the probability that a ship perishes. They show that ambiguity can lower the value of diversification: under ambiguity neutrality it is below the value for the corresponding known risk (their Proposition 2), and in the smooth model, under constant or increasing absolute ambiguity aversion, it is below the ambiguity-neutral value (their Proposition 4.1). This mission formalizes the second result.
A decision maker has sure wealth and ships cargo of value . A ship perishes with probability . Her utility is . Shipping everything on one ship, or splitting the cargo over two ships that perish independently, gives the expected utilities
The value of diversification under risk is .
Under ambiguity, two experts give probabilities . The decision maker holds the prior , with . Write for the value of diversification according to expert . The ambiguity-neutral decision maker averages the experts' expected utilities, so that
The smooth ambiguity model aggregates them through an ambiguity function and takes the certainty equivalent:
A concave expresses ambiguity aversion. A linear gives back . The coefficient of absolute ambiguity aversion is . The decision maker exhibits DAAA, CAAA or IAAA (decreasing, constant or increasing absolute ambiguity aversion) when is strictly decreasing, constant or strictly increasing.
Let be nondecreasing and concave, and let be , concave, with . Suppose that (i) IAAA holds and , or (ii) CAAA or IAAA holds and . Then
Proposition 4.1 shows that the smooth model does not automatically turn ambiguity aversion into a stronger taste for diversification. Under CAAA, the exponential case used throughout applied work, together with experts who both consider a loss at least as likely as not, the smooth value of diversification never exceeds the ambiguity-neutral one. Together with Proposition 2 this says that, in Bernoulli's own example, ambiguity weakly lowers the incentive to diversify. Applied models that use the smooth criterion to explain hedging or portfolio spreading by ambiguity aversion rely on the opposite comparison. The result marks the conditions on and on the experts' beliefs under which that comparison fails.
The paper's proofs are short, but they compress several steps. Lemma 1 is Pratt's (1964) characterization of decreasing, constant and increasing absolute aversion through certainty equivalents, cited without proof. Case (ii) relies on the sentence "it is easy to show that, under the concavity of , inequality (A.8) is satisfied if ", and (A.6)–(A.8) are stated through an expectation over a random whose law is never specified. A formal proof fixes the exact hypotheses: risk aversion and monotonicity of , the regularity of , and the weak form of the conclusion. The mission also yields a reusable Lean statement of Pratt's comparative-statics lemma for two-point lotteries. As far as is known, none of these results has a machine-checked proof.
The algebra (milestones 1, 3, 5, 6) is routine. Lemma 1 is not: its hypothesis is a pointwise condition on , a local quantity, while its conclusion compares certainty equivalents, which are global quantities involving . Mathlib has no theory of absolute risk aversion or of Pratt's comparison for this to rest on.
The natural first attempt at the goal applies Lemma 1 directly, but this only works when every expert's utility rises by the same amount, which is case (i). In case (ii) the shifts differ, and comparing with the weighted average requires knowing which expert gains more. It also requires that this expert is the one with the higher no-diversification utility, and that is where and the monotonicity of enter.
All quantities are real. The utility and the ambiguity function are functions , so outcomes are allowed and logarithmic utility is outside the model. The two experts are two real parameters with prior weights , exactly as the proofs write them. is Function.invFun φ. Every argument it receives is a -mixture of two values of a continuous, strictly increasing , so it lies in the range of and the inverse is the true one.
The following hypotheses are added to the page and disclosed in each item:
IAAA, CAAA and DAAA are monotonicity of , not a sign condition on . "Decreases the value of diversification" is the weak inequality , the comparison (A.4) of the proof. The strict inequality is false at , at , or for linear .
The values of diversification are defined as differences of expected utilities. The closed forms (A.1), (A.2) are milestones, so they cannot become definitions under which those milestones hold by rfl. IAAA is defined through , never through certainty equivalents, which is the conclusion of Lemma 1. Milestone 7 is a repaired two-expert reading of the (A.8) step, not (A.8) as printed.
Not formalized: Proposition 2, the -maxmin results (Propositions 3.1, 3.2), Proposition 4.2, the converse of Lemma 1 and its version for general random variables, and the numerical examples.
Welcome contributions: proofs of the milestones, a general Pratt comparison theorem for certainty equivalents in Lean, and the omitted companion results.
A medical visit, a hotel stay or a bank onboarding is not one transaction but a service process: a sequence of steps (check-in, waiting, examination, payment), each delivered by the provider and each experienced by the customer. Practitioners design such processes with descriptive tools such as customer-journey maps and service blueprints, which list the steps and their touchpoints but do not say how much effort each step deserves. Two features make this allocation non-obvious. First, customers judge the experience as a whole, and the experiences at different steps are correlated: a long wait colours the examination that follows. Second, effort changes not only the average quality of a step but also its variability, and the direction depends on the step: at a routine step (check-in) more effort makes the outcome more predictable, while at a non-routine step (a diagnostic procedure) it may make it less so.
Bellos and Kavadias (Management Science, 2020) give a model in which the optimal effort per step has a closed form, and characterise when the efforts at two steps move together (are complementary) or in opposite directions (are substitutable) in response to a change in one step's characteristics. The answer depends on the two step types and on one entry of the inverse of the correlation matrix, not on the correlation itself. This mission formalizes that characterisation.
There are steps . The provider chooses an effort at every step and one price .
The paper's analysis assumes that each lies in an explicit interval built from the other parameters, the cofactors of and (the interior condition), and for its comparative statics it sets the technical couplings between distinct steps to zero.
Fix a step . Under the interior condition and without technical coupling, the effort at step satisfies
and for every the effort at step responds to , and in the same directions if and only if
and in the opposite directions otherwise (when ). The derivatives are of the optimizer of the design problem, in one parameter at a time.
The result. Proposition 3 says that a change at one step propagates to every other step through the inverse correlation matrix. An entry is, up to a negative factor, the partial correlation of steps and given all other steps. So two steps whose experiences are positively correlated can still have substitutable efforts once the rest of the process is accounted for, and two uncorrelated steps can have coupled efforts. Pairing a routine with a non-routine step reverses the direction. The paper's later results, on antedependent and autoregressive correlation structures and on the first versus the last step, use this characterisation as their starting point.
Formalizing it. The result is proved on paper. As far as is known, it has no machine-checked proof. Formalizing it means: a verified closed form for the maximizer of a box-constrained concave quadratic with a correlation-matrix Hessian; the identification of the optimizer with that closed form near the base point, so that the optimizer is differentiable there; and the sign analysis. Along the way the formalization corrects two printed slips: the auxiliary quantities and in the proof of Proposition 3 (as printed, the displayed identity for fails), and the printed "Otherwise", which is false when .
The sign algebra at the end is short. The work lies in the step before it: Proposition 3 differentiates the optimizer of a constrained problem, not a formula. To differentiate it one has to show that under the interior condition the optimizer exists, is unique, and coincides with on a neighbourhood of the parameters in each direction of perturbation. This needs strict concavity from positive definiteness of , the identification of the interior condition (stated through cofactors of ) with , and the openness of that condition in the parameters. Differentiating directly and reading off signs proves a statement about the closed form, not Proposition 3.
Steps are Fin n, 0-based. All quantities are real. The utility is defined by its mean-variance expression; no random variables appear. is assumed symmetric, positive definite, with unit diagonal and off-diagonal entries in . The cofactor is Matrix.adjugate P i j. Two hypotheses are added to the page and disclosed: (the model allows , but Proposition 1 divides by ) and (every step is routine or non-routine). Proposition 3 assumes for , the paper's own simplification for §4. A partial derivative is Lean's deriv of the optimal effort along one parameter, the others fixed ( fixed when moves, fixed when moves). The optimal effort is a choice of maximizer of the §3.3 problem, with junk value when none exists.
Stating Proposition 3 for the closed form instead of the optimizer of the design problem would trivialize it, and that formalization is ruled out. Likewise the interior condition is the page's interval on , not the assumption .
The development needs Mathlib's positive definite matrices, adjugates and determinants, strict concavity, and one-variable derivatives. Reusable by-products: strict concavity and the unique maximizer of a concave quadratic with Hessian ; positivity of principal cofactors of a positive definite matrix. Contributions are welcome on any milestone, and alternative proofs of Proposition 1 by convex duality or KKT are welcome too.
Proof-of-work mining allocates a fixed reward among miners whose investments determine their chances of receiving it. The resulting distribution of mining power matters for decentralization: if a few miners control most of the investment, the economic mechanism does not support a diffuse set of participants. Arnosti and Weinberg study this question in a contest model where miners have different unit costs and rewards may rise more than proportionally with investment. Their proportional model has an explicit equilibrium; the economies-of-scale model asks what can still be said about market shares when that explicit characterization is unavailable.
The authors' result is a bound for each miner who invests, measured against the cost of any other miner who invests. It applies even when unit costs are asymmetric. The claim is conditional on a pure equilibrium: for sufficiently strong economies of scale, such an equilibrium need not exist, as the paper observes. The mission concerns the quantitative restriction on every equilibrium that does exist, not an assertion that all parameter choices have one.
There are miners and a prize worth one. Miner chooses a nonnegative investment and pays , where the unit cost is strictly positive. A parameter determines how investment affects rewards. At an investment profile , the market share of miner is
when some miner invests. When every investment is zero, the model assigns every miner share zero. The utility of miner is . The prize value is fixed at one throughout; there is no extra reward parameter.
A pure Nash equilibrium is a nonnegative profile at which no miner can increase its own utility by replacing with another nonnegative investment while all other investments remain fixed. This global comparison matters because, with economies of scale, a local first-order condition alone does not characterize a best response. The paper's phrase “equilibrium in the EoS model” has this pure-strategy meaning. A miner participates when ; at the equilibrium profiles of interest this is equivalent to having positive market share.
The paper states the cost vector in increasing order without loss of generality in its earlier proportional-model section. The share bound is invariant under relabelling, so its formal statement permits any assignment of positive costs to the miners. No pair of miners has to be distinct.
The goal is Theorem 2 of the arXiv preprint. For every pure equilibrium and every pair of participants , including , it states
The bound depends on both the scale exponent and the relative costs. Setting gives the symmetric threshold for each participant. The target therefore retains the exact cost ratio and the paper's quantifier over all participating pairs. It does not require a selected or unique equilibrium.
The milestone list follows the authors' named results and one explicit analytic statement in their proof. Lemma 3 gives the equilibrium identity and a separate inequality that still applies to a nonparticipant. Corollary 4 gives when . In the proof of Proposition 1, the function is decreasing on the open interval ; the milestone states strict decrease, matching the negative derivative shown there. Proposition 1 then says that if , then , with equality exactly when . These are the source's results that support Theorem 2, rather than substitutes with weaker conclusions.
The theorem turns a claim about scale effects into a checkable limit on equilibrium concentration. When costs are equal, every participant has share at least . Thus, as the paper notes, sufficiently strong scale effects limit the number of participants in any pure equilibrium. With unequal costs, the same result gives a pairwise share guarantee that accounts for each miner's cost relative to another participant's. A bound only in terms of would lose that comparison.
The mathematical result is proved in the cited paper. This mission asks for machine-checked Lean proofs of the statement and its source milestones. The definitions and theorem statements here are local drafts; compilation of a statement confirms that Lean can parse it, not that a proof exists. The reusable global pure Nash predicate is imported from an existing formalization. The paper-specific layer consists of the contest success function, utility, equilibrium specialization, and share-shape function. Together they make it possible to compare formal proofs of the same economic claim without silently changing the game.
For , the utility from a unilateral investment change can have a shape that is not captured by a single local optimum test. An argument based solely on setting a derivative to zero can miss a better distant deviation or the boundary action . The first-order relations of Lemma 3 are consequences of global equilibrium, not its definition. The main share bound also compares two miners at once: knowing only a participant's own first-order identity gives an expression involving its own share and investment, while Theorem 2 asks for an exact ratio of two different costs. Proposition 1 supplies the ordering information needed by the authors' argument. At , the model meets the proportional case, so formulas involving must still make sense at zero investment.
Lean indexes miners by Fin n; its zero-based labels correspond to the paper's miners without changing any statement. The model uses real-valued investments and costs, with the strategy constraint , and real exponentiation for . Standing assumptions are , , and for every miner. The model explicitly assigns zero share at the all-zero profile, rather than relying on a convention for division by zero. The imported feasible-strategy Nash predicate is specialized to the set of nonnegative real numbers and therefore quantifies over every nonnegative unilateral deviation. No theorem adds positivity of the aggregate investment as a premise: that property must follow from equilibrium where it is needed.
These choices rule out a trivializing formalization in which equilibrium is defined by Lemma 3's first-order equations or the goal is weakened to the equal-cost case. The exact exponent, the unit prize, and the ratio are part of the target. The real-power convention gives at in Lemma 3's inequality; the theorem's denominator is positive at equilibrium. Formal proofs will need finite-sum and real-power facts, unilateral-deviation reasoning, real analysis for the shape function, and inequalities linking investment, share, and costs. Proofs of the four milestones, alternative proofs of the goal, and reusable game-theoretic lemmas are within scope. The paper's separate proportional-equilibrium characterization and countably infinite-miner model are outside this mission.
A cloud provider buys servers in preset configurations, while its demand for processing and memory grows at different rates. Each server configuration supplies both resources, so adding capacity for one resource also changes the unused capacity of the other. Purchases incur a charge for the servers, a charge for making an expansion, and an ongoing cost for unused capacity. The choice between buying configurations together and staggering their purchases is therefore a cost decision even when demand is known. Arbabian, Chen, and Moinzadeh study this decision for two resources and two server configurations over a finite planning horizon. Their Proposition 1 identifies a threshold in the fixed cost of a joint expansion.
The result was stated in the authors' April 14, 2019 manuscript and published in Manufacturing & Service Operations Management in 2020. This mission uses the manuscript's theorem numbers and pages. The result is a known mathematical claim; the remaining work is to give its definitions and proof in Lean, with the source's policy classes and cost accounting represented explicitly.
There are two capacity attributes, indexed by , and two cluster types, indexed by . A unit of cluster supplies units of attribute . Demand for attribute increases at a nonnegative rate over , and is its growth between and . The provider starts with both attributes at their minimum desired excess capacity, normalized to zero. It must meet demand at every time and return both excess capacities to zero at the end of the horizon. Replenishment takes effect immediately. These are the base-model conventions in §3 of the manuscript.
A capacity expansion cycle begins and ends when both attributes are leveled. In a sequential cycle, one cluster type leads: it is bought one or more times, followed by one purchase of the other type. Each expansion costs . In a simultaneous cycle, both types are bought at each expansion, whose fixed cost is for . Cluster has unit purchase cost , and unused attribute has holding rate . If is the excess capacity after the expansions at time , total holding cost is . Total cost also includes all fixed and purchase costs. Sequential policies may have any positive number of cycles, any positive number of leading expansions within each cycle, and either leading type. For joint policies, the intervals between consecutive joint expansions form a partition of .
The main target is the unique fixed-cost threshold of Proposition 1. Write for the infimum of costs of all feasible sequential policies and for the corresponding simultaneous infimum. The threshold satisfies, for every ,
This makes equality at explicit, in line with the paragraph following Proposition 1. The milestone list records the source's sequential and simultaneous cost identities, the fixed-time holding comparison, the split comparison from the appendix, the two endpoint inequalities, and monotonicity in . Equation (8), which fixes the final sequential expansion time inside a cycle, is another milestone because the authors use its uniqueness in their analysis.
The threshold gives a precise decision rule for the model: a lower relative joint expansion charge favors buying both types together; a higher charge favors staggered purchases. It compares optimized policies, whose cycle boundaries and expansion times may differ, rather than only two schedules held at the same times. The result therefore captures the interaction of the fixed charge and the time spent holding unused capacity. The paper also analyzes specialized one-cycle schedules under exponential demand; those results are separate from this mission's general comparison.
A completed Lean development would make the policy definitions, cost identities, and threshold claim machine checked. It would also provide reusable definitions for finite-horizon bundled capacity expansion, including a time-dependent excess-capacity trajectory and its integral holding cost. The manuscript supplies a mathematical proof, but this proposal's theorem files currently contain open sorry proofs. The mission invites proofs of its listed statements and the analytic facts needed to connect them, including existence of optimal schedules.
The straightforward comparison uses identical expansion times. That comparison identifies a holding-cost difference, but it does not compare the two optimized classes: the least-cost sequential schedule and the least-cost joint schedule may choose different times and different numbers of expansions. The paper's endpoint arguments also rely on strict inequalities for optimal costs. A strict inequality for every fixed schedule does not automatically become strict after taking an infimum. Showing that the relevant optima are attained, or supplying an equivalent uniform argument, is part of the formalization burden. The fixed expansion charge bounds how many expansions a near-optimal policy can afford, but the interval lengths remain continuous variables.
Lean represents the attributes and cluster types by Fin 2, with index 0 corresponding to the paper's 1 and index 1 to its 2. The matrix entry a i j is capacity of attribute per unit of cluster . Times, demand, quantities, and costs are real. Replenishment times are strictly increasing, and a purchase at time contributes to the right-continuous excess capacity at . Policy validity requires no shortage and balance at cycle endpoints. The positive determinant records the nondegenerate, attribute-intensive cluster configurations needed by the paper's division formulas. The optimal costs are real infima over full policy classes, with no attainment built into their definitions. Holding cost is computed from the integral of actual excess capacity; defining it by the displayed closed forms would erase the content of Lemmas 1 and 2.
The theorem assumes continuous demand rates and the strict demand-ratio guard and throughout . The manuscript states Assumption 1 only for chosen leading intervals. Its Proposition 1 needs more: without the guard, taking , , , , , and on then permits one joint expansion at for at most 202 while every feasible sequential policy costs at least 300. Demand continuity supports the cost integrals; the strict guard makes every subinterval satisfy Assumption 1 strictly and keeps the appendix's sequential split feasible. Neither regularity nor this guard is claimed as a printed hypothesis of Proposition 1.
The appendix prints an extra outside the sum in its Case 2 holding-cost difference; the Lean milestone uses , consistent with the preceding integrals. The paper also prints in its last monotonicity sentence, while its fixed-cost parameter is defined on ; the milestone uses the model's interval. Useful contributions include formal integration identities for these finite replenishment schedules, existence and finiteness of the policy optima, and the comparison claims in the milestones.
Firms that hold a large, divisible asset (a commodity inventory, a block of shares, a stock of natural gas) often financed it with debt and must sell it over time to repay that debt. Without debt, the timing problem is classical: Karlin (1962) showed that a non-divisible asset facing independent prices should be sold the first time the price exceeds a reservation price. Debt changes the incentives in two opposite directions. Limited liability caps the shareholders' loss at zero, which rewards gambling on high future prices and delays selling. Bankruptcy also destroys the value of the unsold asset, an indirect bankruptcy cost, which rewards selling early to secure the debt payment. Ahn, Wang and Wu (SSRN 3472345, published in Operations Research 69(4), 2021, doi:10.1287/opre.2019.1961) solve the resulting dynamic program with Markov prices. This mission formalizes their central structural result: the optimal first sale under a single debt payment due before the end of the horizon.
A seller holds an amount of a divisible asset at the beginning of period , with . The selling price follows a Markov process: the law of given is a probability kernel , with finite conditional mean. Write for the expectation given the current price. The discount factor is , the per-period selling capacity is , and unsold asset is worthless after period .
The debt-free value solves, with ,
The debt-free critical price is .
Debt. A schedule , , is due at the end of periods , with maturity . The seller's working capital starts at and grows at rate . In period , a quantity is feasible if and . If no quantity is feasible, the seller is bankrupt and the equity value is . Otherwise
For a single payment (and otherwise), write and , with . The net effect of debt is
It is the value of limited liability net of the bankruptcy cost. The two critical prices are
Assume , a single payment at , a period before any sale (, ), and a price . Then , and:
After the debt-securing sale, the optimal quantities coincide with the debt-free ones. Moreover:
When , all three prices coincide.
In attack order:
Proposition 4 is the paper's headline. Under debt, the first sale follows a control band. Below the seller waits. Between the two critical prices, the seller sells exactly the quantity whose revenue covers the discounted debt; in that band a higher price means a smaller sale. Above the seller sells everything. Part (ii) separates the two economic forces by the sign of one number, . When the bankruptcy cost dominates, part of the asset is sold earlier than without debt. When limited liability dominates, selling is delayed and done all at once. The same structure underlies the paper's later results on threshold debt levels and general installment schedules.
The result is proved on paper but has not been formalized; the platform has no asset-selling, reservation-price or debt-constrained selling model. The mission contributes three things. The first is a finite-horizon Markov-price dynamic program with an explicit bankruptcy branch and limited liability, built on Mathlib's probability kernels. The second is Karlin-type debt-free stopping results for a divisible asset. The third is the full convexity argument behind the control band.
Part (ii) is signed algebra once footnote 4 is known; the work is in part (i). Because of the bankruptcy branch, is neither convex nor concave in general (Lemma 1(iii)). So the first-order reasoning that settles the debt-free problem, a linear objective in , does not carry over. Two facts reduce the optimum to three candidate quantities. The first is convexity of in below the debt-covering region, proved by backward induction together with the debt level. The second is linearity above that region. The induction must carry the debt level as a variable.
Every value function is integrated against a kernel. Before any identity between expectations can be used, and must be shown measurable and integrable, and both are suprema over a continuum of quantities. The strict inequality of footnote 4 is a separate induction: at every positive price.
Everything lives in the namespace AssetDebt.ControlBand.
Representation.
κ t p is the law of given , a Mathlib Kernel ℝ ℝ.Added hypotheses.
Excluded trivializations. is never defined by its closed forms (A.6), (A.8) or (A.9), which would make the goal an unfolding exercise. The critical prices are not existentially quantified: a price-dependent existential could be witnessed by thresholds read off the optimal action itself.
Infrastructure. A complete development needs measurability of suprema of kernel integrals, sup-shift lemmas for bounded intervals, and the backward-induction convexity argument. The debt-free results (Proposition 1) and the sup and measurability lemmas apply to other finite-horizon selling and stopping models. Contributions are welcome on any milestone, in particular on the measurability layer.
A seller can disclose privately known product quality, but credible disclosure costs money. In a market with competing sellers, disclosure changes both what consumers believe about a silent seller and how aggressively the sellers can price. Zhang and Li study this interaction when consumers are loss averse about quality: learning that a product falls below an expected standard hurts more than learning that it exceeds the standard helps. Their duopoly result says that stronger consumer loss aversion makes firms disclose more often and raises each firm's profit before quality is known, even though disclosure itself remains costly. The model and result appear in the SSRN preprint, §§3.1–3.3 and Proposition 2.
The paper first gives a monopoly benchmark and then analyzes two firms facing the same consumers. The duopoly question is distinct because a firm's disclosure affects the gap between its own product's perceived value and its rival's. The paper's Proposition 2 is a comparative statement about the equilibrium of this disclosure game, not a claim about a distribution chosen for a numerical example. The formalization targets the general quality distribution used in the paper.
Two symmetric firms, A and B, each have one product and a privately known quality . Their qualities are independent draws from a common cumulative distribution with a continuous, strictly positive density and . A firm may pay a common disclosure cost to reveal its quality truthfully. Otherwise, consumers infer quality from nondisclosure. With a common disclosure threshold , firms reveal quality above and remain silent at or below it. The inferred quality of a silent firm is the conditional mean .
When a product's quality is disclosed, a consumer values it at , where is its price. When quality is hidden, the consumer experiences a gain or loss relative to . With gain sensitivity and loss sensitivity , equation (1) gives utility
The degree of consumer loss aversion is . The paper assumes and also discusses the loss neutral benchmark . It uses two functions of the quality distribution,
They express the belief as and the expected gross utility of a silent product as , by equation (2). After disclosure decisions, firms set prices against homogeneous consumers. Under the paper's participation condition, the Bertrand outcome awards the firm with the higher gross consumer value the difference between the two values as revenue; the lower valued firm earns zero. Disclosure cost is then subtracted from the revealing firm's revenue. A symmetric equilibrium threshold means that both firms use the same and each firm's disclosure choice is a best response at every quality.
Fix and compare at fixed , with . For the corresponding symmetric best response thresholds , Proposition 2 asks for both strict comparisons:
Here is either firm's ex ante profit, averaged over its own quality before the draw. The result does not prescribe a numerical disclosure threshold or profit. The preprint's Proposition 2, p. 18, states the two directional claims; its proof on p. A7 gives strict signs.
The milestones preserve the paper's intermediate statements: the nondisclosure belief and expected utility, growth of , the two disclosure profits, the equilibrium equation (6) and its unique root in Claim 3, the ex ante profit identity (7), and the derivative of the integral . In particular, the game defined above determines the threshold and profit; equations (6) and (7) are claims to establish about those objects.
The result identifies a setting in which a consumer preference that lowers the perceived value of undisclosed goods can benefit competing firms. A stronger aversion to disappointed quality expectations changes firms' disclosure decisions and, through those decisions, the price differences available in competition. Proposition 2 gives a statement about each firm's expected profit, while the paper separately discusses cases in which an individual firm's realized profit can rise or fall. These distinctions are explicit in the preprint's §3.3, pp. 15–18.
The economic result is established in the paper; this mission seeks a machine checked Lean proof of its symmetric equilibrium claim and the paper's supporting identities. The statements here compile as open targets, and no proof is asserted to have been formalized. The work also develops reusable interval integral facts for conditional means and costed disclosure games with a general continuous quality density.
The central difficulty is the link between the original disclosure game and the integral expressions used in the paper's comparative statics. The profit of disclosing depends on the rival's random quality and its disclosure decision. The profit of silence depends on a belief formed from the same threshold that firms choose. A formula about a root of equation (6) alone does not establish that the root is a best response threshold in this game. Likewise, the compact profit expression (7) must agree with the profit obtained by integrating the game's conditional Bertrand margins and paying disclosure cost.
The general density also matters. A calculation for the uniform distribution in the paper's numerical footnote does not cover the paper's proposition. Establishing strictness requires keeping the positive density, the monotonicity assumption on , and the consumer participation domain visible throughout the development.
Lean represents and as real valued functions relevant on , together with a proposition asserting that is continuous and positive there, that on the interval, and that . Every expectation against is an interval integral against . The firms' independent, identical draws are encoded by using that same density separately for own and rival quality; no probability space is introduced. The standing assumption that is increasing is expressed as strict monotonicity on . The threshold lies in that interval, so division by cannot create a boundary statement about an undefined conditional mean.
Lean's utility function is gross of price. Its pricing layer represents the paper's homogeneous consumer Bertrand outcome by . The symmetric equilibrium predicate requires the silent product's gross utility to be nonnegative, and the strategic payoff identities carry the same condition. This is the bound in footnote 3 of §3.3, p. 15. The comparison fixes and increases ; it includes to cover the paper's loss neutral benchmark. The model's positive and assumptions are explicit in the economic statements. The milestone for exposes positivity on the full positive interval, beyond the page's explicit .
The symmetric equilibrium is defined by best responses in disclosure and the participation condition, with consumers using the conditional belief and firms receiving Bertrand revenue less disclosure cost. Neither the equilibrium threshold nor ex ante profit is defined by the simplified equation it is supposed to satisfy. Claim 3 gives a unique root of the threshold equation; an admissible root must also satisfy participation to represent an equilibrium. The paper's Claim 2 about the absence of asymmetric equilibria is outside this mission: Proposition 2 is framed for the symmetric equilibrium, and the printed argument for Claim 2 has an unresolved monotonicity step. Contributions to the model identities, equilibrium characterization, integral calculus, and goal proof are all within scope.
Suppliers often let buyers pay after delivery. If the buyer defaults, the supplier loses the credit sale revenue and may also face a financing cost from the resulting cash shortfall. Trade credit insurance transfers part of this loss to an insurer, but the insurer may possess information about the buyer that the supplier cannot observe. The insurer can use that information by canceling coverage before shipment. Yang, Bakshi, and Chen study how this option changes both the insurer's incentive to gather information and the supplier's decision to ship. Their Proposition 3 identifies a regime in which a simple cancelable contract recovers the entire value available to a centralized decision maker. Yang, Bakshi, and Chen (2021)
The question matters for contract design because a policy's deductible and refund affect different decisions. A deductible changes the supplier's loss if the buyer defaults. A refund changes the insurer's cost of canceling coverage. With a sufficiently attractive alternative sales channel, these terms can induce the insurer to reveal adverse credit information through cancelation while leaving the supplier fully covered when she ships. This mission states that claim precisely for the three-signal model in the authors' accepted manuscript. Accepted manuscript, §§3 and 6
A supplier receives an order for one unit at credit price . She may ship on credit or sell through an outside channel for . When the buyer defaults, the supplier receives no payment from the buyer. Her financing cost depends on end-of-period net cash flow :
Here is a cash flow threshold and is the marginal cost of falling short. At the time of contracting, the buyer's default probability is . An insurer can pay cost to monitor the buyer and observe one of three signals . Signal occurs with probability and has conditional default probability , where and . The paper assumes the outside channel is initially less attractive than the credit sale: . Accepted manuscript, §3 and Table 1
A cancelable contract is . The supplier pays premium ; if she ships while covered and the buyer defaults, the insurer pays the credit price minus deductible . Before shipment, the insurer can instead cancel coverage and refund . After this decision, the supplier chooses whether to ship. The contract must satisfy and . The insurer's monitoring decision compares its expected total cost with three alternatives: keep coverage without monitoring, cancel without monitoring, and decline the contract. The supplier's payoff includes her premium, any refund, default losses, and financing costs. Accepted manuscript, §§3 and 6, and Lemma B.1
The first-best payoff is the maximum available to a financially unconstrained planner who controls monitoring and, if monitoring occurs, can choose whether to ship at each signal. The paper's Proposition 1 identifies it as
The quantity is the value of using the signal to avoid credit shipments for which the outside sale is better. The supplier receives the full value of TCI when her payoff under a contract equals . Accepted manuscript, Proposition 1 and its proof
Proposition 1 gives the difference between the first-best and the no-insurance payoff:
This benchmark makes the phrase “full value” testable against a separate maximization over planner policies, rather than against a formula chosen to fit the contract. Accepted manuscript, Proposition 1, p. 11
The goal is Proposition 3. Under Assumptions 1 and 2, the paper's efficient-monitoring regime , and , it identifies
The insurer monitors and cancels at signals 2 and 3; the supplier ships only at signal 1. Her payoff equals , and no other admissible cancelable contract gives her more. Milestones establish the monitoring conditions, the first-best formula, feasibility and resulting decisions, attainment of the payoff, and the upper bound over other contracts. Accepted manuscript, Proposition 3, p. 18, and proof, pp. xi–xii
Proposition 3 identifies a regime where cancelation transmits the insurer's private credit information into the supplier's shipment choice. It gives exact contract terms, the induced actions at each signal, and a payoff that meets the centralized benchmark. The result thus pins down when the option to cancel coverage eliminates the loss from the two parties controlling different decisions. Yang, Bakshi, and Chen (2021), §6.2
The result is proved in the paper. The remaining formalization work is to prove the Lean statements, beginning with the finite three-signal model and ending with the optimality inequality over every admissible cancelable contract. A local prior-art search found no published declaration with this model and these conclusions. The finite contract and policy definitions can also support formal statements about the paper's other regimes, provided their distinct assumptions and timing rules are introduced explicitly.
The contract sits on several decision boundaries. In particular, the insurer's cost of monitoring can equal the refund, so replacing a weak incentive comparison by a strict one would discard the proposed contract. The supplier can be indifferent about shipping at signal 2 after coverage is canceled when . The paper's displayed threshold rule and its Proposition 3 proof make different tie choices there. The formal goal follows the proof's choice and records it in the model.
A second difficulty is showing global optimality. Computing the proposed contract's payoff alone does not compare it with contracts that generate different cancelation or shipping patterns. The upper-bound milestone covers all admissible cancelable contracts, while the first-best is defined from the planner's actual choices. The threshold cannot define shipping at the proposed contract, because its denominator is zero there. Accepted manuscript, equations (1), (6)–(9), and proof of Proposition 3
Lean uses real-valued prices, costs, probabilities, and payoffs, and a finite signal type with three members. Lean indices correspond to the paper's signals . The prior is defined by Table 1's weighted average . Standing hypotheses state nonnegative signal probabilities summing to one, ordered default probabilities in , , , and positive monitoring cost. The explicit additions and make financing cost nonnegative and meaningful. Assumption 1, Assumption 2, and remain separate hypotheses.
Decisions are defined by payoff comparisons. Shipping under coverage uses the weak inequality in (1); cancelation and shipping after cancelation use the strict tie choices in the proof of Proposition 3, equations (64)–(66). The first-best is a maximum over no-monitoring choices and all shipping policies after monitoring. Optimality compares the supplier's payoff with every valid cancelable contract that induces monitoring and actual cancelation at some signal. Defining the first-best as the desired formula, restricting competitors to contracts with the proposed policy, or using division by a zero threshold denominator would empty the intended claim.
The development needs finite sums, real inequalities, maxima, and a representation of sequential contract decisions. Contributions proving the monitoring characterization, planner value, feasibility, payoff identity, and global upper bound are within scope. The model's finite signal and contract interfaces may be reused in further results of the paper.
A firm that needs outside money to start a project knows more about the project than its investors do, and it can usually choose how much of that knowledge to reveal before raising funds: which audits to commission, which metrics to report, how informative an analyst's report will be. The security-design literature studies the security side of this problem, meaning what claim to sell given the information the investors have (Innes, 1990; Nachman and Noe, RFS 1994). The Bayesian persuasion literature (Kamenica and Gentzkow, Bayesian Persuasion, AER 2011) studies the information side, meaning what to reveal when a sender can commit to a signal in advance.
M. Szydlowski, Optimal Financing and Disclosure (Management Science 2021; working paper of March 2017), puts the two together. An entrepreneur who cannot finance a project on the prior alone commits to a disclosure policy so as to maximize her expected payoff, subject to the investors' competitive pricing. The main answer is simple and testable: the optimal policy is a pass/fail test, and the passing standard is set exactly where investors break even. This mission formalizes that answer and the chain of lemmas the paper's appendix uses to reach it.
The project pays . The investment cost is . The entrepreneur sells a security with payoff to competitive investors. is continuous, , and both and the residual are weakly increasing (equity, debt and options all qualify). The common prior over has a continuous density with support .
A posterior is a probability measure on . At posterior the security sells for (1), and the project is financed iff (2). If it is financed, the entrepreneur receives the residual, a private benefit , and a share of the excess cash, so her payoff (3) is
A disclosure policy induces a distribution over posteriors. By Kamenica and Gentzkow's equivalence, the feasible are exactly the Bayes-plausible ones, those whose mean posterior is the prior, (5). The entrepreneur's problem (6) is to maximize over Bayes-plausible . The threshold policy with cutoff reveals only whether . With probability it produces the posterior on , and otherwise the posterior on ; this is (17).
Throughout, the project cannot be financed without disclosure: (§4).
There is a threshold at which the financing constraint (20) binds,
such that the threshold policy with cutoff is Bayes plausible and attains the maximum of over every Bayes-plausible . The hypothesis is added, as explained under Formalization scope.
Proposition 1 gives disclosure a concrete shape: certify whether cash flows clear a bar, and say nothing more. The bar is the lowest one at which investors still break even, so the entrepreneur maximizes the probability of financing. The paper's later results build on it: the choice of the optimal security (Proposition 4), extensions to general utility (Proposition 5), and comparative statics of the threshold in the security's information sensitivity (Propositions 2–3).
The result is proved on paper but has not been machine-checked. A formalization adds three things. It checks a proof whose central step goes through an infinite-dimensional linear-programming duality (Levinson, 1966). It pins down hypotheses the printed statement omits, notably . And it provides a reusable Lean account of Bayesian persuasion over a continuum of states, with distributions over posteriors as measures on the space of measures.
The obvious argument is a bang-bang argument. Fix the probability of financing, put as much high-posterior mass as possible on the best states, then optimize over . Each step hides a gap. The reduction to two posteriors (Lemma 1) needs barycentres of a measure on the space of measures. The fixed- problem is a linear program over densities with a pointwise cap , so finite-dimensional LP duality does not apply. The paper uses an infinite-dimensional duality theorem plus a compactness lemma under an extra equicontinuity restriction (32).
Monotonicity of the value in is where the printed argument fails in general. The marginal contribution can be negative near the cutoff when . In that case a slack threshold beats the binding one, and the binding threshold is not optimal. A second trap is that the binding root of (20) need not be unique: for debt, every cutoff above the face value can solve (20) with equality. " solves (20)" therefore cannot by itself be the content of the theorem.
The state space is , and and are read only on . The prior is Lebesgue measure on with density . Support is encoded as positive prior mass on every nondegenerate subinterval. Posteriors are arbitrary measures on , and a distribution over posteriors is a measure on the space of measures with Mathlib's Giry σ-algebra. Bayes plausibility is: is a probability measure, almost every posterior is a probability measure, and 's monadic join is the prior. Posterior expectations are integrals over , written through positive and negative parts so that they are measurable in the posterior. As a result is never a junk value. Ties in the financing rule go to financing (). "Increasing" means weakly increasing. The fixed- problems range over integrable densities with pointwise, which encodes . The equicontinuity restriction (32) is dropped; it serves only the compactness Lemma 2, which is not formalized.
Two hypotheses are added, each disclosed in the items that carry it:
The goal quantifies over all Bayes-plausible distributions over posteriors, and its threshold is pinned by optimality, not only by solving (20). A version restricted to threshold or two-point policies, or one whose is any root of (20), would be a different and weaker theorem. Optimality is stated as "an optimal policy", since the optimum is not unique.
Not formalized: Lemma 2 (compactness); the continuity and differentiability parts of Lemma 5; the second case of Proposition 8 (); and the paper's later Propositions 2–6, 9 and 10. The general definitions of Bayes plausibility and of the reveal-a-cell policy are stated for an arbitrary measurable state space and are reusable for other persuasion missions. Contributions are welcome on any milestone. A barycentre construction for measures on the space of measures (Lemma 1) and a bathtub principle for densities under a pointwise cap (Proposition 7) are of independent use.
Wind and solar generation have near-zero marginal cost. In a wholesale electricity market where prices are set by the marginal producer, adding such capacity displaces expensive conventional generation and lowers the spot price: the merit-order effect. Regulators and system planners rely on this effect when projecting the price impact of renewable expansion, and empirical studies of European markets report it.
Most electricity, however, is not traded only in the spot market. Producers and retailers hedge in forward markets before demand and wind output are known, and forward trading changes how producers with market power behave in the spot market (Allaz and Vila, 1993). Peura and Bunn (Management Science, 2021) ask what happens to the merit-order effect once this channel is included. Their answer is that, when wind output is variable and positively skewed, additional wind capacity eventually raises the expected spot price and the forward price. This mission formalizes that statement, Proposition 2 of the paper, together with the equilibrium characterization it rests on.
There are two conventional producers with constant marginal cost , a set of price-taking wind producers with total capacity and zero cost, price-taking retailers who resell at a fixed retail price , and an elastic industrial demand , where is the spot price.
Two random quantities are drawn on a probability space: the total retail demand , bounded, and the wind yield , so that available wind output is . They are independent and both have positive variance. Write for the mean, variance and third central moment of , and for those of . The coefficient of variation of the yield is and its normalized skewness is .
Trading has two stages.
With and , the spot equilibrium is and (Lemma 1). The forward-spot equilibrium is and for explicit expressions in the parameters, the moments, and (Theorem 1).
If
then an equilibrium exists at every capacity , and there are thresholds and such that along every equilibrium selection
The value of comes from the paper's proof; the proposition itself only asserts that some works.
The result. Proposition 2 isolates a mechanism by which two pro-competitive forces, low-cost capacity and forward trading, can combine to raise prices. Variable and skewed wind output increases the risk that a producer is caught with a large forward position when wind is high and the spot price is low. Producers therefore sell less forward, which by Lemma 1 lowers their spot output and raises the spot price. For large enough capacity this forward effect outweighs the merit-order effect. The condition for the reversal involves only and .
Formalizing it. The result is proved in the paper but has no machine-checked proof. In a formal development the equilibrium has to be defined through the participants' optimization problems, not through the closed forms. Theorem 1 then has to show that this optimization-defined equilibrium exists, is unique, and equals the closed form. The polynomial coefficients have to be checked: the printed has a misplaced parenthesis, and the printed is off by a factor of . Both are corrected and disclosed in the milestone statements. Neither affects the conclusion.
The goal combines three layers. The probabilistic layer computes means, variances and covariances of products of independent bounded random variables. These computations produce the third central moments and justify replacing the utility of each participant by an explicit quadratic in its own position. The game-theoretic layer has to show that each first-order condition gives a global optimum, which needs strict concavity, and that the producers' best responses, each computed against a clearing price that itself depends on the deviation, meet at a unique point. The analytic layer studies the rational function of , whose derivative's numerator is a quartic with coefficients that are themselves polynomials in eleven quantities.
A tempting shortcut is to define the equilibrium by its closed form, which reduces the goal to a sign argument on a polynomial. That shortcut removes Theorem 1 entirely and is excluded here. A second tempting reading treats the forward price as fixed when a producer deviates. That makes producers price takers in the forward market, which is a different game whose equilibrium is not .
The market parameters are a structure with fields a, c, pR, lam (, a Lean keyword) and NR : ℕ; the retailers are indexed by Fin NR. The demand and the yield are real functions on a probability space , and the capacity is a separate real argument, so the joint law stays fixed as varies. The standing assumptions, a hypothesis of every model theorem, are: and are measurable and independent; is bounded and at every sample point; ; ; and . The last two come from the paper's statement that demand and supply are uncertain in the forward market. Third moments are central. The footnoted conditions and are not assumed, since the goal holds without them.
The spot inverse demand is the interior branch of the paper's , used for all and all realizations, with quantities ranging over the reals. This is what Assumption 1 (no blackouts or curtailment) licenses and what the paper's proof differentiates. The statement is therefore about the model with linear inverse demand. At realistic parameter values the turning point can lie where Assumption 1 fails for some realizations, so its economic reading inside the no-curtailment region is the paper's interpretation, not part of the theorem.
The forward-spot equilibrium is a predicate built from optimization alone: retailer optimality over all real positions, clearing, and each producer's optimality against every deviation evaluated at that deviation's own clearing price. The closed forms (13)–(16) and the quartic's coefficients live in a separate definition file used only in milestone conclusions. The goal imports only the model. The goal also contains an existence conjunct, so the statement about equilibrium selections is not vacuous.
A complete development needs moment calculus for bounded independent random variables (variance and covariance of products, third central moments), maximization of concave quadratics, and single-crossing arguments for real polynomials. The moment computations and the mean-variance optimization of an affine position are reusable beyond this mission. Contributions are welcome at every milestone, including partial results.
Networks of autonomous sensors — machines on a factory floor, vehicles, devices in the Internet of Things — each measure a common environment with their own noise and can improve their estimates by asking other sensors for theirs. Communication capacity is limited, so each sensor must decide whom to ask, and the answer it receives is useful only to the extent that it understands how the other sensor turns measurements into estimates. Saghafian, Tomlin and Biller (SSRN 3124417, version of October 16, 2020; published in Manufacturing & Service Operations Management, 2021) model this as a dynamic target-selection problem and ask which communication network forms in the long run. Their abstract leads with the answer: each sensor eventually settles on a constant target set, which is sample-path dependent. With known, pairwise distinct qualities this target set is a single sensor (Proposition 4, p. 21). This mission formalizes that result.
There are sensors . Sensor has a quality : its measurement of the state has noise variance . Sensor starts with initial familiarities with each other sensor , the precisions of its initial Gaussian beliefs about 's inference parameters. A sample path is the sequence of realized states, an arbitrary sequence of reals.
The familiarity function of with in period is a function . It starts at
In period , after is revealed, sensor targets the sensor of least signal variance
with ties broken toward the lower index (footnote 11). Writing if and otherwise, the familiarity grows by the stickiness factor:
The long-run contacts of along are (Definition 2)
In Lean these are Instance (q, v, w), psi1, sigma2, stick, lowArgmin, the joint recursion fam/target, count and longRunContacts in IoTFusion.KnownQuality.
If the qualities are asymmetric ( for , Definition 3), then for every sample path
No hypothesis on the state process is involved: the statement holds path by path.
Supporting items: for (long_run_contacts_nonempty); each sensor eventually targets one fixed sensor (eventually_constant_target, the wording of p. 5); and the rank-one precision identity (EC.66).
Proposition 4 says that, with known and distinct qualities, the long-run communication network is a functional graph — every sensor has out-degree one — although which graph forms depends on the realized states, and a sensor's eventual partner need not be the highest-quality sensor available. The paper builds on it its description of the long-run network as a random directed graph (Propositions 5–6) and its managerial discussion of early-period "momentum" in familiarity.
The result is proved in the paper; nothing in it is machine-checked. The work here is a formal proof of the deterministic core, including the existence half , which the printed proof (p. ec22) does not give: it shows only .
Every statement is elementary in isolation; the difficulty is that the target sequence is defined by a feedback loop. The target of period depends on familiarities, which depend on all earlier targets, which depend on earlier states. Statements about "infinitely often" therefore cannot be reduced to the behavior of any single function of fixed in advance.
The tempting argument "the highest-quality sensor eventually wins" is false: a sensor that becomes familiar early with a lower-quality partner can keep choosing it forever, so no fixed candidate for the unique contact exists. The uniqueness argument must instead compare two putative long-run contacts with each other, using a familiarity threshold that does not depend on the familiarity with the worse one (Lemma 2), and the existence half needs a separate counting argument over the finitely many possible targets.
Fin n (0-based) with on the existence statements; for there is no other sensor and .fam P i s k is .Filter.Tendsto … atTop atTop; is Set.ncard; asymmetry is Function.Injective q.Set.ncard bookkeeping would be reusable.Firms increasingly delegate the generation of new concepts (product designs, advertising campaigns, engineering prototypes) to outside providers such as design agencies and engineering consultancies. The client cannot dictate how hard the provider works; it can only decide when to stop asking for new solutions. Two practices are common. Under a flexible stopping policy the client keeps the right to stop or continue after each submitted solution. Under a committed stopping policy the client commits in advance to stop, and pay, as soon as a feasible solution arrives. Classical search theory says that keeping options open is never harmful, so flexibility should dominate. Yet committed contracts are widespread in practice.
Rahmani and Ramachandran (2021) explain this by two features that the classical benchmarks omit: a deadline on the number of rounds, and a provider who adjusts its effort from round to round in response to the client's policy. In two benchmark settings, an unlimited number of rounds or a fixed provider effort, flexibility (weakly) dominates (their Lemmas 1 and 2). With a deadline and strategic effort, commitment can be strictly better, and the paper characterizes exactly when.
A client delegates a project of rounds to a provider. In each round in which the client asks for a solution, the provider chooses an effort , at cost or , and submits a solution of quality . The client pays an evaluation cost for each submitted solution. When the project stops with a feasible solution (), the client implements the best solution received and pays the provider a fixed payment ; if no feasible solution is found by the deadline, nothing is paid.
Quality under effort has distribution function
where is the provider's capability: with probability the solution is infeasible (), and otherwise it has density on . The expected quality is . The standing assumptions are
Under the committed policy, the project stops after round 1 if . Under the flexible policy, after a feasible the client compares with the expected value of a second round and stops when stopping is at least as good. The provider anticipates this and chooses its efforts by backward induction: round-2 efforts , (after a feasible first solution), (after an infeasible one), then round-1 efforts , . Write and for the client's equilibrium expected profits under the two policies.
Fix satisfying the standing assumptions and a payment . There exist thresholds and such that for all and ,
Commitment is strictly better exactly for an intermediate range of evaluation costs, and never when the payment is below . The thresholds are left existential, as in the paper.
Proposition 4 reverses the conventional wisdom that retaining decision rights cannot hurt the decision maker. The mechanism is strategic: flexible stopping lowers the provider's expected reward for a good first solution, because the client may continue the search instead of accepting it, and so it weakens the provider's first-round effort (Proposition 3). When the payment is in , commitment induces high first-round effort that flexibility does not, and whether this outweighs the option value of a second round depends on the evaluation cost. The result gives contract designers in innovation procurement a concrete criterion in terms of evaluation cost, capability and payment.
The paper's proofs are in an online appendix. No machine-checked version of any result in this model exists. The mission produces a formal model of a dynamic principal–agent stopping game with an atom-plus-density quality law, a verified threshold structure for the client's stopping rule, and the full equilibrium effort characterization, all of which carry over to related delegation and contest models.
The goal compares two equilibrium profits, each determined by a nested backward induction in which the provider's round-1 effort depends on the client's stop rule, which in turn depends on the provider's round-2 effort. The obvious approach, comparing the two policies at the same efforts, proves only Lemma 2 and points the wrong way. The comparison must instead track which of the effort regimes of Proposition 3 each policy induces, as a function of and . The profits are piecewise in (the stopping threshold is zero for large ), and the claim that the strict-improvement set in is a single open interval requires a monotonicity argument across these pieces, uniformly in . The case must be shown to give no improvement at all.
The Lean development models exactly the two-round game (), the case the paper analyzes in §4. Effort levels form a two-element inductive type; parameters form a record, with and separate arguments. The standing assumption is written cross-multiplied; is the reading that costs are non-negative. The paper's Stieltjes integrals are Bochner integrals of against the density over the open ray ; the atom at appears in the separate terms, so no payment is charged on infeasible solutions. Ties are broken as on the page: the provider takes high effort, and the flexible client stops. The paper's restriction to payments "neither too high nor too small" (Lemma A-1 of its online appendix) is not available; every statement is posed for all , for which it remains true. Evaluation costs satisfy .
The model defines no stopping threshold and no effort in closed form: the stopping threshold is a theorem (Proposition 2), is computed from the provider's objective, and the goal compares profits at the efforts the model computes, not at efforts supplied as arguments. A formalization that defined , fixed , or compared the policies at exogenous efforts would make the milestones trivial or prove a different theorem, and is ruled out.
A complete development needs integrals of polynomial-times-exponential functions on rays, the closed forms of the round-2 values, and finite case analysis over effort profiles. Contributions to the comparative statics (Propositions 2 (c), 3 (c)) are welcome independently of the goal.
Not formalized: Proposition 4 (b) (its half fails under the main-text model, e.g. at , , , , , , ); Lemma 1 (infinite horizon); Proposition 1 (general finite ); Proposition 5 (dependent solutions); Propositions 6–8 (endogenous payments); the numerical study.
Online retail platforms such as Amazon, Alibaba's Tmall and JD.com host thousands of third-party sellers and observe every customer interaction with each of them. From these interactions the platform learns about market demand far better than any single seller can, and it sells or gives away part of that knowledge through analytics tools (Alibaba's Business Advisor is the example in the source paper). The platform earns a commission on every seller's revenue, so it cares about the sellers' total profit, and it has to decide what each seller is told.
The classic literature on information sharing in oligopoly points the other way. Gal-Or (1985) showed that Cournot competitors facing a common demand shock never voluntarily pool their private demand signals: shared information makes their strategies more correlated, and the resulting competition destroys more value than the better forecasts create. Li (2002) and others refined the conditions. Liu, Zhang and Zhang (Manufacturing & Service Operations Management, 2023; SSRN 3258109) change who decides: the signals belong to the platform, which chooses what each seller learns in order to maximize its commission. Their headline result for the unconstrained ("asymmetric full sharing") format is that the platform shares everything it knows, without any added noise, but only with a limited number of sellers, and that number is determined by the substitution between products alone.
There are sellers of substitutable products. Given quantities , seller 's price is
where is a common demand shock with prior variance . The platform observes, for each seller , a signal with , , independent of everything else.
A noise matrix with entries in is the platform's sharing strategy. Seller receives the noisy copy , independent, for every with ; is truthful sharing and means is withheld from seller . Seller 's information is the -algebra generated by what he receives.
Each seller chooses a quantity measurable with respect to his information to maximize his expected profit , where is the platform's commission rate. A Bayesian equilibrium under is a profile of such strategies from which no seller gains by deviating. The platform's expected profit is , and it chooses before the signals are realized.
Under Asymmetric Full Sharing (AFS) each seller receives all signals with one common noise level (for all ), and the levels may differ across sellers. The benchmark is no sharing, for all , with platform profit .
Let . Among all AFS noise matrices in and all equilibria, an optimal strategy is to share truthfully with sellers and nothing with the others, where
The platform and every seller do weakly better than without sharing, and every optimal truthful group has size or .
The result separates two levers of information design, precision and audience, and shows that in this linear-Gaussian Cournot setting only the audience matters: the platform never degrades a signal, it only chooses how many sellers see it. The optimal audience size depends only on the substitution parameter once the market is large, and equals one seller when products are perfect substitutes. This reverses the Gal-Or no-sharing result by changing who decides, and it explains why a commission-earning platform may rationally treat its sellers asymmetrically, which is the tension the paper's later sections on fairness and privacy constraints study.
The paper's proofs are in an online appendix. No part of this model has a machine-checked proof. The mission produces a reusable Lean layer for Bayesian games with designed Gaussian signals: information -algebras generated by noisy copies of shared signals, Bayesian Nash equilibrium over square-integrable strategies, and its characterization by first-order conditions in conditional expectations. Mathlib has Gaussian measures, conditional expectation and independence, but not the projection formula for jointly Gaussian vectors that eq. (5) needs.
The closed forms are routine once one assumes that equilibria are linear in the received average signal. The difficulty lies in what that assumption skips. First, eq. (5) is a statement about conditional expectation with respect to a -algebra generated by correlated Gaussian variables; it needs the Gaussian conditioning (projection) theorem, not a computation with densities. Second, the goal quantifies over all equilibria, so existence and uniqueness of the equilibrium must be proved for every noise matrix, including those with infinite entries; the paper solves the first-order condition and never discusses uniqueness. Third, Proposition 1 is an optimization over : the platform's profit is not concave in the noise levels, and the endpoint property for one seller (with the others fixed at arbitrary levels) is the step that rules out partial sharing. Restricting attention to truthful groups from the outset assumes away exactly this step.
All declarations live in the namespace RetailInfoShare.AFS, with one definitions file RetailInfoShare.AFS.Model. Conventions:
gaussianReal 0 σ), as eq. (3) of the paper requires.ℝ≥0∞; a signal with never enters the receiving seller's information -algebra.Fin N, so the paper's sellers are indices .Out of scope: the AIS half of Proposition 1, Proposition 3 and Lemma 2 (privacy-constrained sharing), the symmetric formats of §5, the pricing mechanism of §6, and the appendix extensions. Contributions of general infrastructure are welcome: the Gaussian conditioning theorem in Mathlib form, and existence and uniqueness of equilibria in linear-quadratic Bayesian games with Gaussian information.
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).
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.
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.