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?
In inverse optimization, an observer sees decisions made by an expert who solves an optimization problem, and wants to recover the expert's unknown objective. Besbes, Fonseca and Lobel study a contextual version: in each period a feasible set and a context function are revealed, a learner must act before seeing the expert's choice, and then observes the expert's optimal action. The learner pays the expert's cost of its own action. This models, for example, a platform imitating a dispatcher's routing decisions or a recommender learning a user's trade-offs, where only optimal choices, not costs, are ever observed (Besbes, Fonseca, Lobel, arXiv:2106.14015).
For the one-period (offline) problem the paper shows that the circumcenter policy, which acts as if the unknown cost were the center of the smallest revolution cone containing the set of costs still consistent with the data, is minimax optimal (Theorem 1). The natural online policy is to apply it greedily in every period. This mission formalizes the paper's Theorem 2, which shows that this greedy policy can fail badly: its worst-case regret can grow linearly in the horizon, even when the initial uncertainty is small in a precise geometric sense.
Costs live in and actions in . The true cost lies on the unit sphere . An action set is a nonempty compact subset of of diameter at most ; a context function is a -Lipschitz map . The forward problem with cost has solution set
The angle between nonzero vectors is , set to if either vector is . The uncertainty angle of a set is
and a circumcenter is a unit vector attaining this infimum. A set is pointed when , i.e. it fits inside an open half-space cone.
Online protocol. In periods nature reveals and , the learner picks , and then an optimal expert action is revealed. Starting from a closed set , the knowledge set is
the regret is , and the worst-case regret is its supremum over and admissible instances. The greedy circumcenter policy chooses .
There is a closed, nonempty, pointed such that
Concretely: there are and such that for every horizon some and admissible admit a greedy run, and every greedy run (any circumcenter, any tie-break) has regret at least . The constant is left existential, as the page claims only .
The result separates offline from online learning in this model. Theorem 1 makes the circumcenter the best one-shot guess, yet Theorem 2 shows that one-shot optimality says nothing about information collection: a greedy learner can keep choosing actions that are wrong by a fixed margin while the revealed expert actions cut away only slivers of the knowledge set. This is the reason the paper introduces its EllipsoidalCones algorithm, which acts greedily on an enlarged ellipsoidal-cone superset and attains logarithmic regret for pointed initial sets. Theorem 2 is the lower bound that makes that design necessary.
On the formal side, the paper's proof is complete but compressed; it asserts the circumcenter of a three-generator spherical polygon "using Definition 2" and leaves the induction's geometric inclusions to the reader. A machine-checked version fixes the normalization of the circumcenter and the quantitative condition behind "", and gives a reusable formal treatment of uncertainty angles and circumcenters, which the paper's other results (Theorem 1, Theorem 3, Lemma 10) all use. No result of the paper has a formal statement or proof on Prove2Me yet.
The arithmetic of Step 3 is elementary once the knowledge sets are known. The difficulty is in Steps 1 and 2. Identifying the circumcenter of requires a minimax argument over the whole sphere: one must show that no other unit vector has a smaller maximal angle to the three extreme rays, and that the minimizer is unique, which rests on Lemma 2. The greedy policy is defined through this minimizer, so without uniqueness nothing can be said about its actions. Step 2 then needs an exact description of each knowledge set: showing that the new half-space makes the previous one redundant inside requires the sign information carried by the other constraints. A naive bound on the regret that ignores the knowledge-set dynamics fails, because a priori the policy might learn after a few periods.
Vectors are EuclideanSpace ℝ (Fin d), so norms, diameters and Lipschitz constants are Euclidean. The angle uses the paper's convention ; Mathlib's InnerProductGeometry.angle is not used. Action sets are required to be nonempty (otherwise no action exists). Periods are -based in Lean: Lean period is the paper's period , and Lean's knowledge set at is the paper's . The construction and the goal are in dimension , as in the proof; the goal holds for every action dimension .
The worst-case regret is never written as a real supremum, whose junk values would decide the statement. The lower bound is stated by exhibiting the instance. A run of the greedy policy is a predicate quantifying over every circumcenter choice and every minimizer, and nature's sequences are arbitrary. Two pins relative to the page: the printed circumcenter is normalized as in Step 3, and Step 3 assumes , which the page's "" needs (the goal uses ).
Two trivializations are ruled out. Without pointedness the claim holds for with antipodal costs, so is part of the goal. A bound over all runs would hold vacuously if no run existed, so the goal also asserts that a greedy run exists.
A complete development needs spherical geometry of polyhedral cones (extreme rays, angles to a cone), continuity of the uncertainty-angle objective for Lemma 2, and elementary trigonometry. The Geometry and Online definitions are shared with the other missions of this series and are reusable for any work on inverse optimization or learning from revealed preferences. Proofs of any milestone are welcome, as are alternative arguments for Lemma 2.
Remote driving, or tele-driving, lets a human operator in a control center drive a vehicle over a wireless link. A ride-hailing platform that adopts it decouples drivers from vehicles: a driver is attached to a vehicle only while that vehicle carries or fetches a customer, and is released the moment the trip ends. Since an idle vehicle needs no driver, the platform can run a fleet of vehicles with drivers. The operational question is how much service is lost by having fewer drivers than vehicles.
Benjaafar, Wang and Yang study this question with a loss queue in which the service rate depends on the number of idle vehicles, capturing the fact that pickups take longer when fewer vehicles are free (SSRN 4130757; published in Management Science, 2024, doi:10.1287/mnsc.2022.01687). The state-dependent rate builds on the spatial capacity model of Besbes, Castro and Lobel (doi:10.1287/opre.2021.2112). Their main finite-system results describe how the service level changes with the number of drivers in three regimes of vehicle supply. This mission formalizes the third regime, where vehicles are ample. The source is the authors' 2023 SSRN working paper; all labels and page numbers below refer to it.
A fleet of vehicles is operated by remote drivers. Customers request trips according to a Poisson process with rate . A request that arrives when all drivers are busy is lost. When customers are in service, each one completes at rate , so the total completion rate is . The rate is defined for real . Let
The number of customers in service is a birth–death chain on . Its stationary law is
and the service level is the long-run fraction of demand served, .
The paper's standing assumptions on the rate are:
The supply-rich regime is the case , that is, : even with every vehicle busy, the system clears work faster than it arrives. In this regime there is a unique with , and exactly when .
In the supply-rich regime, is strictly increasing in . For every with ,
The first part of Theorem 1.C says that, when vehicles are ample, every driver removed costs some service. The second part says the cost is small once exceeds by a margin. The bound is increasing and concave in , so a platform can run noticeably fewer drivers than vehicles at a controlled loss of service. The paper's numerical study (Figure 7) reports reductions of 35–60% in the number of drivers at a service loss below 0.01. The same objects carry over to the paper's asymptotic Theorem 2.C, where the driver-to-vehicle ratio needed in a large supply-rich market tends to .
The result is proved on paper and has no machine-checked proof. The work this mission adds is formal:
is a ratio whose numerator and denominator both change with . For the drivers beyond , monotonicity is immediate, since each additional factor shrinks the numerator while the denominator grows. Below , and the numerator grows, so that argument fails, and the comparison has to use the shape of on . The shape of (Lemma 3) has to be derived from concavity and monotonicity of alone: the assumptions give no smoothness, although the paper's proof differentiates twice. The page argues the two ranges separately, so the step across also has to be covered. The lower bound needs care at the integer part of : the sum in the denominator is taken from , which is at least 1 only because .
Needed infrastructure: finite products and sums over Finset.Icc, StrictConvexOn/StrictConcaveOn on intervals, and the intermediate value theorem for a function that is continuous on . The model file is shared, up to namespace, with four companion missions on the same paper. Proofs of the general facts used here are reusable beyond this mission and are welcome as separate contributions: the product of a positive increasing linear function and a positive antitone concave function is concave, and the reciprocal of a positive strictly concave function is strictly convex.
Low interest rates are meant to stimulate investment, yet periods of monetary easing have coincided with weak corporate investment and large debt-financed share buybacks and dividends. Acharya and Plantin (SSRN 3484935; Management Science, 2025, doi:10.1287/mnsc.2022.01440) explain this with a moral-hazard channel: when the market rate falls below the rate at which shareholders discount the future, firms borrow against future output to pay out cash today (a leveraged payout). The payout lowers the shareholders' retained stake and with it their incentive to make the firm productive.
The paper then asks how a central bank should set the interest rate after a temporary productivity shock when wages cannot fall. Cutting the rate raises investment but degrades productive efficiency through leveraged payouts. Proposition 12 answers the question by the size of the shock: small shocks should be met by leaving the rate unchanged ("leaning against the wind", in the sense of Stein, 2012), and only large shocks may justify a cut.
An economy consists of a discount rate , an effort-cost parameter (not the circle constant), a capital-good technology and a consumption-good technology . Both satisfy the Inada conditions: , , , ; is twice continuously differentiable on with , and is continuously differentiable with strictly decreasing. A unit mass of workers supplies one unit of labour; goes to the capital-good sector and to the consumption-good sector. The laissez-faire steady state solves
At date 0 one cohort of workers is hit by a shock : its technology is . Its first-best labour solves . The date-0 wage is rigid at .
The central bank chooses the date-0 rate . With , entrepreneurs exert effort and hire labour with
The rate at which is the lowest feasible rate. The planner maximizes the date-0 surplus
An optimal rate , with labour , maximizes over every feasible rate.
There is such that
The threshold is pinned from both sides: the first clause alone holds for close to 1, the second alone for .
Proposition 12 is the paper's policy prescription. Together with Proposition 11 (with unregulated leverage the optimal date-0 rate is at most and investment falls short of the first-best) it says that the second-best response to a shock under a rigid wage is non-monotone in the shock size: a central bank that cuts rates for every shock overreacts to small ones.
The result is proved in the paper, in Appendix B, and has no machine-checked proof. The paper's argument is a sketch at three points: Step 1 appeals to "a standard continuity argument", Step 2 to the envelope theorem (66), which presumes a unique differentiable optimum, and the existence of an optimum is taken for granted. A formal proof settles these points and makes the role of explicit. The printed statement also carries a slip (it reads where is meant), which the formalization corrects and records.
The surplus need not be concave in , so first-order conditions do not identify the optimum, and the optimum must be compared globally across the feasible rates . Near both the efficiency gain and the scale term vanish, so the sign of near is a second-order matter: the gap is of order , and the argument breaks down if . The naive argument " is continuous in , so persists near " fails without a uniform estimate, because the optimizer need not depend continuously on . A tie between an interior optimum and may occur at .
The Lean development fixes one economy E : Economy (fields R, π, f, g, lstar, wstar with (20)); the shock and the first-best labour (IsFirstBestLabor E ρ lρ) are separate parameters, so that varies with everything else held fixed. Effort is effort E r, labour demand the relation IsLaborDemand E r l (which includes ), and optimality IsOptimalRate E ρ ru lu is global: against every rate and every feasible labour demand at . Derivatives are deriv, used only where the Inada conditions give differentiability.
Conventions and deviations from the page:
A trivializing formalization is ruled out: optimality is never local, , and are tied to their defining equations, the existence of an optimal rate for is asserted rather than assumed, and the clauses for and are stated together, so that neither nor near 1 satisfies the goal for free.
A complete proof needs the inverse function theorem for , compactness of the feasible rates , the mean value theorem for at , and a uniform second-order estimate near . The continuity and differentiability of the labour response, and the existence of an optimal rate, are reusable for the companion mission on Proposition 11. Proofs of any milestone, and alternative arguments for Step 1 that avoid the envelope theorem, are welcome.
A metric space is plastic if every nonexpansive bijection of it onto itself is an isometry. Every totally bounded metric space is plastic (Freudenthal–Hurewicz 1936; the term is from Naimpally–Piotrowski–Wingler 2006), and Cascales, Kadets, Orihuela and Wingler (2016) asked whether the closed unit ball of every real Banach space is plastic. The answer is known to be yes for strictly convex spaces (CKOW 2016), for ℓ₁ and ℓ₁-sums of strictly convex spaces (Kadets–Zavarzina 2016, 2018), for finite ℓ∞-sums of strictly convex spaces (Haller–Leo–Zavarzina 2022 for two summands; Kurik 2025 under an extra hypothesis), and for c and for c₀ under continuity of the inverse (Leo 2022), among others; it is open for L¹[0,1] and C[0,1].
A recurring step in these proofs is to show that the map preserves the unit sphere and then that a sphere-preserving map is linear. The published versions of the second step assume homogeneity on rays, or oddness, in addition to sphere preservation (CKOW 2016, Lemma 2.5; Zavarzina 2018, Corollary 2.6; Kadets–Zavarzina 2018, Lemma 2.9). This mission formalizes a version that needs only sphere preservation, together with a strengthening in which surjectivity onto the ball is replaced by coverage of the target sphere. The results come from an unpublished research project on the plasticity problem.
and are real Banach spaces, and .
A map is nonexpansive if for all .
In Lean a map of balls is a function F : X → Y on the whole space, constrained on the ball by Set.MapsTo, Set.SurjOn and LipschitzOnWith 1; its values outside play no role.
The goal and its milestones, from the most special tool to the strongest statement:
In U10 and U16, and are nonzero.
The result. U10 reduces the plasticity problem in every real Banach space to sphere preservation, and U16 to coverage of the target sphere by the image of the sphere; the reductions hold between two different spaces, which matters because the plasticity problem is equivalent to its two-space form (Kurik 2025, Theorem 3.1). They also show that sphere preservation, preservation of every norm, and being an isometry are equivalent for nonexpansive surjections of unit balls.
Formalizing it. The proofs exist only in the project's own notes and have been checked by AI referees and partly by the author; a machine-checked proof is the independent confirmation sought. Mathlib has no theory of nonexpansive or averaged maps, so the development will contribute uniform asymptotic regularity of averaged nonexpansive maps (Borzdyński–Wiśnicki; Goebel–Kirk 1990, Theorem 9.4), U16 needs the Bishop–Phelps theorem, which Mathlib also lacks, and the quantitative form of A01 needs the sharp rate of Cominetti, Soto and Vaisman for averaged maps (arXiv:1206.4195, Theorem 1); it is not needed for U10 or U16.
No injectivity, oddness, homogeneity, smoothness or continuity of an inverse is assumed, so none of the standard routes to linearity applies: Mazur–Ulam needs an isometry, and the published sphere-preservation lemmas need homogeneity on rays. In U16 the map need not even be onto the ball.
Real scalars; arbitrary (not necessarily separable) Banach spaces, with CompleteSpace and, in U10 and U16, Nontrivial.
The conclusion of U10 and U16 is a LinearIsometryEquiv agreeing with F on the closed unit ball, so it includes surjectivity of the linear map.
A01 concludes Set.EqOn H id on the closed unit ball.
Statements are not to be weakened by adding injectivity, continuity of an inverse, or finite dimension.
Published inputs (Goebel–Kirk, Bishop–Phelps, Banach's fixed-point theorem from Mathlib) may be added as separate cards and imported by proof sketches.
Large online retailers such as Amazon, Walmart and JD.com run a retailer-led marketplace: they sell products on their own account and, on the same storefront, host independent third-party sellers whose sales they tax. How the platform charges those sellers is a live question for competition authorities and for the platforms themselves. Real marketplaces mostly use ad valorem fees (a percentage of the seller's revenue, the "referral fee"), sometimes together with per-item charges. Hervas-Drane and Shelegia (Management Science, 2025) build a model of such a marketplace in which the platform chooses its fee, steers part of the demand, and decides which products to sell itself under a capacity constraint. In their Appendix B.3 they ask whether a per-unit fee would serve the platform better than the ad valorem fee, and answer that it would not: provided the per-unit fee is not a subsidy, the platform sets it to zero (Lemma B.1). The comparison echoes the classical public-finance question of ad valorem versus specific taxation under imperfect competition (Suits and Musgrave, 1953).
There is a unit mass of products, indexed by their value to consumers, distributed by a probability measure (the CDF of the paper) on , where is the common marginal cost of supplying a unit. Each product is its own market, with a unit mass of unit-demand consumers and one potential third-party seller . The monopolist :
The game has three stages: announces ; each decides whether to enter, then chooses which products to sell; then prices are set. In a product sold by alone (SBT) she charges and earns . In a product sold by both (SBMT), serves the steered consumers at and charges
so earns . A product sold by alone (SBM) earns him . Sellers enter the products of the marketplace set , that is when .
An allocation is a measurable set of products with . 's profit adds over , over and over , and his profit at fees is
For every maximiser of over with ,
The goal asserts nothing about existence of a maximiser or about the value of ; it constrains every maximiser.
The result. Lemma B.1 justifies restricting the platform's instrument to an ad valorem fee, which is how the paper's main analysis (entry modes, the positive optimal fee, fee regulation) proceeds. It also isolates a mechanism: a per-unit fee raises the seller's effective marginal cost and so the price she must charge, while an ad valorem fee with the same entry threshold extracts more from high-value products. The paper notes on p. 19 that once subsidies are allowed the conclusion reverses; that is a different optimisation and not part of this mission.
Formalizing it. The result is proved on paper in a short argument; it has no machine-checked proof. A formal proof must make precise what the paper leaves implicit: that is a supremum over all allocations, re-optimised after a fee change, that the profit gain from the fee switch is strictly positive and survives the supremum, and which degenerate corners (a foreclosed marketplace, full capacity with full steering) must be excluded. The model file is shared in form with the series' two other missions, which formalize the paper's entry-mode theorem (Proposition 2) and the positivity of the optimal ad valorem fee (Lemma 2).
The milestone algebra is elementary. The difficulty is in passing from a pointwise gain to the value function. The fee switch raises 's revenue on every marketplace product above for a fixed allocation; is a supremum over allocations, so a pointwise strict gain does not by itself give a strict gain of the supremum. When the gain is bounded below uniformly over allocations, through the positive mass of . When the SBMT gain vanishes, and an allocation that covers almost all marketplace products gains nothing; ruling out that the supremum is approached by such allocations requires comparing with a different fee pair, and uses that has a density and full support. The naive reading, "keep 's allocation fixed and compare", only gives a lower bound on the new value and is not itself a proof of optimality failure.
Lean conventions, all in the namespace RetailerMarketplace.UnitFee:
μ : Measure ℝ with IsProbabilityMeasure μ, μ (Set.Iio c) = 0, μ ≪ volume (a density), Integrable (fun v => v) μ (finite mean, never stated in the paper but needed for profits to be finite), and full support on , ∀ a b, c ≤ a → a < b → 0 < μ (Set.Ioo a b) (the reading of in the paper's display (3)).0 < c is a standing hypothesis (the paper's and " such that " presuppose it); is Assumption 1; .vT and the switched fee appear only under and .PiM is sSup of the profits of all measurable allocations of mass at most ; under integrability the set is nonempty and bounded above, so this is a genuine supremum.A formalization that fixes 's allocation in the definition of , restricts allocations to intervals, takes the supremum over a set that may be unbounded, or replaces "every maximiser has " by "some pair beats " would trivialize or change the statement, and is ruled out.
A complete development needs set integrals over the marketplace set, the bathtub-type comparison of allocations, and order properties of sSup on ℝ. The model file and the milestone lemmas are reusable for any fee-design question in the same model. Proofs of the milestones, of the goal, and of intermediate lemmas about PiM (monotonicity in the fees, strict improvement under the fee switch) are welcome.
Many network goods are bought in more than one variety at once. Gamers own both a PlayStation and an Xbox, households subscribe to several streaming services, and users keep accounts on competing social networks. A consumer who multihomes pays twice but enjoys the exclusive content of both products and the network of both user bases. Much of the literature on competition with network effects, starting with Katz and Shapiro (1985) and Farrell and Saloner (1985), assumes that every consumer buys exactly one product. In the paper's own single-homing benchmark (a Hotelling duopoly with network effects), equilibrium prices and profits are strictly decreasing in the strength of the network effect.
Foros, Kind and Stähler (SNF Working Paper 16/21, 2021; published in Management Science, 2025, doi:10.1287/mnsc.2022.00613) let consumers choose endogenously between buying one good and buying both. Without network effects, multihoming makes prices strategically independent (Kim and Serfes, 2006; Anderson, Foros and Kind, 2017), since a consumer's purchase of one good does not depend on the price of the other. Once some consumers multihome and network effects are present, the comparison flips for a range of parameters: network effects make prices strategic complements and can raise both prices and profits. This mission formalizes the paper's Proposition 2, which says exactly when network effects raise the equilibrium price and the equilibrium profit, compared with a market without them.
Two firms sit at the ends of a Hotelling line of unit length, on which a unit mass of consumers is spread uniformly. A consumer at who buys good pays a mismatch cost , with , and . Good has exclusive features worth , and buying it yields a network benefit , where is the strength of the network effect and the expected number of buyers of good . Throughout, (Assumption 1 (i) of the paper). Marginal costs are zero.
When some consumers buy both goods and expectations are fulfilled (), the demand for good at prices is the multihoming demand
Maximizing over gives the reaction function , (15).
This mission treats symmetric firms, . The symmetric fixed point of (15) is the price , and the profit is :
Some consumers multihome and some singlehome exactly when lies in the partial-multihoming range , with
The comparison benchmark "without network effects" is the same model at , where and . The two thresholds of the result are
For , and :
Milestones 4–6 together give , so both thresholds lie inside the partial-multihoming range and every branch of the goal is attained.
Proposition 2 is the paper's answer to whether network effects help or hurt competing firms once consumers can buy both products. In the single-homing benchmark they always hurt. With partial multihoming, network effects raise prices when exclusive content is scarce () and raise profits on the wider range ; in between, on , prices fall but larger sales more than compensate. The thresholds indicate when a firm benefits from stronger network effects, a question the paper's conclusion raises for technology choice.
The result is proved in the paper by hand algebra. This mission produces machine-checked statements of every display of the proof in Appendix A1, first half, in the paper's exact closed forms. Nothing in this model has been formalized before.
The price comparison is a sign check on a rational function. The profit comparison is not: is a quadratic in whose positive root involves , and placing that root relative to and requires comparisons such as . Squaring is valid only once both sides are known to be nonnegative, a fact the paper uses without stating, and the comparisons degenerate to equalities at , so every strict inequality depends on . A naive approach that clears denominators without tracking their signs, or that squares without checking signs, proves nothing.
All parameters are real numbers; , , are explicit arguments. The standing assumptions are explicit hypotheses: , (Assumption 1 (i)), and , strengthened to wherever a strict comparison with the case without network effects is made. The overlapping features cancel from every object and are not a parameter. Assumption 1 (ii)–(iii) (market coverage, positive market shares) is not needed by any statement and is not added.
The model's demand is (14), the multihoming demand under fulfilled expectations; its derivation from consumer choice, and the full pricing game with its single-homing regime and deviations, are not formalized. The profit is defined as price times demand (14), not as the closed form (26), which is a milestone. "Assume partial multihoming" is the parameter range . Proposition 4, the paper's equilibrium characterization, is not posed, because it is false as printed (a profitable deviation exists inside its stated range). Milestone 3 adds , since the quadratic in also has a negative root. The paper's milestone sentences give one direction ("lower if ", "larger if "); the companion directions that Proposition 2 asserts are posed too.
The thresholds are the printed closed forms with Real.sqrt: is never defined as "the root of ", which would make the profit threshold true by definition, and is the literal . Every denominator is positive under , and those hypotheses are kept so that no conclusion relies on Lean's division by zero or on the square root of a negative number.
Needed: real-field algebra, Real.sqrt monotonicity and squaring lemmas, and sign analysis of quadratics. No measure theory or game-theoretic library is needed. Contributions of any milestone, in any order, are welcome.
Affirmative action policies are usually designed reductively: one adjustment for women, another for a racial minority, a third for applicants from low-income families. An applicant who belongs to several categories gets the combined adjustments. A long literature in sociology and law, beginning with Crenshaw's account of intersectionality (1989), argues that people at the intersection of several disadvantaged categories (for instance Black women) can stay underrepresented even when every single category is proportionally represented. Carvalho, Pradelski and Williams, Intersectionality: Affirmative Action with Multidimensional Identities (Management Science, 2025), give this debate a decision-theoretic model. They ask whether any policy that treats identity dimensions independently can achieve proportional representation of every intersectional group.
Their first main result answers that question for a general class of score adjustments and for generic score distributions. This mission formalizes that result, Theorem 1, together with the lemmas its proof uses.
A decision maker admits a share of a unit-mass pool of applicants. Each applicant has a score in an interval and an identity , with . Category is the set of identities with . Write and for the vectors of zeros and ones and for the -th basis vector. The identity equals when the sum is computed coordinatewise in the integers.
The population is a probability measure on , with marginal masses . The space consists of those whose conditional score laws are continuous (atomless) and have full support on . carries the relative weak topology, the topology of weak convergence of probability measures.
A policy family is a set of strictly increasing bijections that is rich (for all some has ) and commutative (). Additive shifts on are an example. A policy assigns to each identity a map . Given a threshold , an applicant of group is accepted when , subject to the capacity constraint
The accepted share of is , the fraction of the accepted who belong to . The outcome is representative if for every (Definition 2). A policy is nonintersectional if implies , and intersectional otherwise (Definition 1). Nonintersectional policies are the reductive ones: is the composition of the maps over the categories that belongs to.
A property is generic in if it holds on a dense open subset of . Theorem 1 states: there is a dense open such that for every ,
"Yields a representative outcome" means that some threshold satisfies the capacity constraint at level and gives for every . Nothing about is fixed beyond richness and commutativity, and nothing about beyond membership in .
The result. Theorem 1 separates two classes of policy. The reductive class, which covers the way most affirmative action programmes are written, cannot generically deliver proportional representation of intersectional groups, however its category-wise adjustments are tuned. A policy that adjusts each intersectional group separately can. The negative part holds for every rich commutative family, not only for additive or multiplicative adjustments, so the impossibility does not come from a particular functional form. The later results of the paper build on this one. They measure how badly reductive policies fail, give the nongeneric conditions under which they succeed (Proposition 3, which is the subject of the companion mission), and treat imperfectly intersectional policies.
Formalizing it. The theorem is proved in the paper; to our knowledge no machine-checked version exists. A formalization has to make several things precise:
The paper's proof of Lemma 2 also concludes with a formula valid only for the additive family (p. 23), so a complete formal proof would supply the missing argument for a general .
Part (b) and the necessary conditions behind part (a) follow from the definitions. The hard step is genericity (Lemma 2). Openness requires the quantiles to depend continuously on in the weak topology. It also requires the map to be continuous, where each is itself determined by and . The obvious argument writes this map as an explicit formula, , and that formula holds only for additive shifts. For a general rich commutative family, continuity of the transport map must come from the structure of as a group of homeomorphisms of an interval acting freely and transitively. Density requires perturbing the law of group while keeping the perturbation inside . This is where enters: for , and there is nothing to perturb independently.
The Lean development fixes the following conventions.
Fin n → Bool, and is checked coordinatewise on Bool.toNat.ProbabilityMeasures on , whose Mathlib topology is that of weak convergence. is the subtype of measures for which every group of positive mass has no atoms and positive mass on every nonempty open subinterval of .Several trivializing formalizations are ruled out:
A complete development needs:
The first two are reusable well beyond this mission. Contributions to any milestone are welcome, and proofs of the quantile-continuity facts as standalone lemmas are especially useful.
Online platforms run experiments on subjects that arrive one at a time: a user opens an app, a customer reaches a checkout page, a patient enters a trial. Each subject must be assigned to control or treatment at once, before the next one arrives, and the quality of the final estimate depends on how well the two groups resemble each other in their observed covariates. Classical sequential randomization such as Efron's biased coin (Efron 1971) balances the group sizes; Zhao and Zhou (arXiv:2201.12936, Management Science 2025) instead measure imbalance by an online matching cost and ask how small it can be made against an adversarial sequence of covariates.
Their pigeonhole design partitions the covariate space into cells and balances the two groups inside each cell. With one continuous covariate the paper shows (Lemma 3 and Corollary 1) that uniform cells achieve an expected cost of order , against for complete randomization (Lemma 2). This mission concerns the matching lower bound, Lemma 4: no choice of pigeonholes does better than .
A horizon of subjects, with even, arrives at times . Subject carries a covariate , and the whole sequence is fixed in advance by an oblivious adversary. An assignment puts each subject in the control group or the treated group .
The discrepancy of the split (display (1), p. 11) is the cost of a minimum-weight perfect matching between the two groups:
A pigeonhole design (Definition 3, p. 16) takes a partition of into pigeonholes. When subject arrives:
The design's expected discrepancy on is the average over these fair coins.
An interval partition is given by breakpoints , ; its pigeonholes are , and the cell lengths are .
There are an absolute constant and a threshold such that for every even and every interval partition of , some arrival sequence gives
The partition is arbitrary and the hard sequence is chosen after it; and do not depend on or on the partition.
Milestones 5 and 6 (with ) together give the goal.
Lemma 4 makes the upper bound of Lemma 3 meaningful as an optimality statement: among all pigeonhole designs on one continuous covariate, uniform cells are optimal up to the factor . It also locates the source of the rate in a tension between two kinds of randomness. Long cells let fair coins inside a cell create imbalance across the cell's length. Many cells leave one unmatched subject per cell, and these must be matched across cells. The rate cannot be improved by tuning the partition alone; doing better requires designs outside the pigeonhole class.
The paper's proof is a short sketch, and no part of it has been machine-checked. A formal proof would supply an explicit hard instance for every interval partition, including the rounding of the counts to even integers and the instance for the many-cell case, which the paper leaves unspecified. Lemma EC.2 is a classical result (Blyth 1980) that also has no formal proof in Mathlib.
The algebra of milestones 3 and 4 is elementary. The difficulty lies in the two cases.
In the few-cell case, the per-cell bound of milestone 2 must be computed from the design's actual run. That requires showing that on the alternating instance the first member of each pair always meets a tie in its cell, and that the global cap never alters an assignment. The matching cost must then be bounded below. On the line the optimal matching is determined by the order of the points, so a cell's internal imbalance cannot be cancelled by subjects of other cells, and this needs proof. The ideal counts are not even integers, and the rounding must not destroy the bound.
The many-cell case is the least specified step. The paper's sketch (an odd number of subjects per cell, then a coupling with complete randomization) does not say where the unmatched subjects lie. As printed, it does not handle a partition that mixes one long interval with many short ones; such a partition must be handled by a combination of the two constructions. Lemma EC.2 needs a sharp local estimate of the binomial distribution: the error term is , which is finer than what a plain central limit theorem gives.
Many accounting frauds have come to light through whistleblowers rather than through audits, and regulators now run programs to encourage tips: since the Dodd–Frank Act of 2010 the U.S. Securities and Exchange Commission pays awards for original information that leads to a successful enforcement action. Empirically, whistleblower involvement is associated with better enforcement outcomes (Call, Martin, Sharp & Wilde, 2018), and employees are a leading source of fraud detection (Dyck, Morse & Zingales, 2010). A natural conjecture is that more whistleblowing raises the chance that an audit failure is caught, and so pushes auditors to work harder.
Nan, Tang & Ye (Management Science, 2025) show in a small game that this conjecture can fail. Their main result, Proposition 2, characterizes exactly when increasing whistleblowing intensity lowers equilibrium audit quality. This mission formalizes that result together with the equilibrium it is about.
A firm is good () with probability and bad () otherwise.
where the posterior is computed by Bayes' rule from the probabilities above. 4. Auditor's program. She pays damages when an audit failure is caught, and minimizes
An equilibrium at intensity is a triple of mutual best responses in which the enforcer's posteriors are computed at the actual . The paper assumes and . Write for the enforcer's incentive and for the auditor's incentive.
In Lean, a Model carries with these restrictions. The posteriors are postW1, postW0; the best-response predicates are IsEnforcerBR and IsAuditorBR; the equilibrium is IsEquilibrium M τ a e1 e0. An equilibrium path A (IsEquilibriumPath M A) assigns to every an equilibrium audit quality .
Fix and , and let
There is a threshold , depending only on and positive when , such that for every model with these and , and every equilibrium path ,
The milestones follow the paper's equilibrium analysis and its proof of Proposition 2:
Proposition 2 separates two effects of intensity. The direct effect is that a tip triggers high investigative effort more often, which raises detection and audit quality. The indirect effect, the silence effect, is that with more intense whistleblowing silence becomes reassuring, so the enforcer investigates less without a tip. The result says the indirect effect dominates exactly when the enforcer's incentive is above an explicit threshold and the auditor's incentive is below a threshold. The paper builds its welfare analysis on it: the planner's optimal intensity (Lemma 2, Proposition 3) and the reward-design extension of §4.
The theorem is proved in the paper (Appendix, pp. 31–34), and Proposition 1 is stated without a printed proof. As far as is known, none of it has been machine-checked. A formal proof would check the computer-algebra steps the paper summarizes as "it is simple to verify" or "after some algebra manipulation". It would also make precise two points the printed proof leaves loose. First, the derivative of in fails to exist where the equilibrium crosses the kink of . Second, the printed comparison "" is reversed: is what holds and what the argument needs.
The equilibrium audit quality has no closed form; it is the root of the gap function , which involves a and rational functions of . The obvious attempt, differentiating the closed-form equations (7)–(9) in , gives an expression whose sign is not visible. Its sign depends on , and on which branch of the the equilibrium lies.
The paper splits by branch. On , the sign of is controlled by a single-crossing property in and by the limit at , which yields . Turning this into a threshold on requires the comparative static of in . Each of these steps is a polynomial inequality in four or five variables over a box. They are routine to check numerically, but proving them requires explicit sign certificates.
Model. The intensity is a hypothesis of each statement, not a field.deriv is not used for this, because it returns at a kink. By Proposition 1 the path is unique on .Contributions that are welcome include sign certificates for the polynomial inequalities of p. 33, an implicit-function argument for the derivative of the equilibrium path off the kink and a proof of Proposition 1, for which the paper prints none.
Remote driving, or tele-driving, separates the driver from the vehicle: a human sitting in a control centre drives a car over a network link and can switch to another car as soon as a trip ends. Commercial pilots of this model exist for car delivery and ride-hailing, and it gives a platform a new design choice. A conventional ride-hailing fleet has one driver per car. A tele-driven fleet can run more cars than drivers.
Benjaafar, Wang and Yang model this choice as a queueing system and ask how the service level depends on the number of drivers when the number of vehicles is fixed (SSRN 4130757; published in Management Science, 2024, doi:10.1287/mnsc.2022.01687). Idle vehicles still matter even when nobody is driving them: they are spread over the service region, so the car nearest a new request is closer, and trips (pick-up plus ride) finish faster. A driver count below the vehicle count therefore trades fewer servers for shorter service times. This mission formalizes the paper's first main result, Theorem 1.A, which says when that trade can strictly improve service. The mission follows the 2023 SSRN working paper (version of 1 June 2023) and its numbering.
A platform has vehicles and remote drivers. Trip requests arrive as a Poisson process of rate . A request that finds all drivers busy is lost. While customers are in service, each trip ends at the exponential rate , a function of a real . The paper's standing assumptions on this rate are:
The number of customers in service is a birth–death chain with birth rate and death rate , truncated at . With
its stationary law is for . The service level, the long-run fraction of requests served, is
The paper restricts throughout to and . It splits fleet sizes into three regimes by thresholds . In the supply-limited regime , demand exceeds the trip-completion rate in every state: for all .
For , if
then there is a threshold such that is strictly increasing in for and strictly decreasing for , with . If (5) fails, is non-decreasing in on .
Theorem 1.A says that removing drivers from a fleet can strictly raise the fraction of demand served, and Condition (5) says exactly when. The condition compares the average trip-completion rate with the completion rate when every vehicle is occupied. In a standard multi-server loss system, where , the condition never holds and more servers always help. The result makes the optimal driver count a well-posed line search over a unimodal function, and the companion Theorems 1.B and 1.C of the paper (intermediate and supply-rich regimes) rest on the same recursion.
The paper's proofs are short but leave gaps a formal proof must close. To our knowledge no part of the paper has been machine-checked. The mission produces a complete formal statement of the model and of the theorem, under the paper's own assumptions, together with the lemmas the published argument passes through. Milestones 2–4 hold in every regime, so they also serve the proof of Theorem 1.B.
Two steps resist the obvious argument. First, the blocking probability is not a monotone function of anything simple: each driver count truncates the birth–death chain at a different state, so the comparison between and drivers is a comparison of two different stationary laws. Second, the published argument for the first step of the dichotomy appeals to " by Assumption 2", which Assumption 2 does not imply. A correct proof must handle the case where the blocking probability increases already from one driver to two. Strict convexity of must also be proved without derivatives, because the formal rate is only assumed concave, not differentiable.
All objects live in the namespace TeleDriving.ScarceFleet. The rate is a function mu : ℕ → ℝ → ℝ, meaningful for real . , the products , and are explicit definitions following (1)–(3). The committed conventions are:
The threshold is bounded, , and no hypothesis on the shape of or is assumed. A threshold or an assumed monotonicity would make the theorem trivial. The dichotomy milestone carries no regime hypothesis, because the argument of App. C.1 does not use one.
Useful infrastructure, reusable beyond this mission, includes: mediant inequalities for with ; the fact that the product of a positive linear function and a positive, antitone, strictly concave function is strictly concave; and the induction pattern that turns a one-step recursion test into global unimodality. Proofs of any milestone, alternative arguments, and proofs that dispense with the regime hypothesis are all welcome.
The European Union's General Data Protection Regulation (GDPR, in force since 2018) shifted control over personal data from firms to consumers: data may be collected and processed only with the consumer's consent, and consent may be given for some uses and withheld for others. Online retailers use consumer data in two opposite ways. Saved shopping carts, stored addresses and location sharing make shopping more convenient for the consumer; the same data can also be monetized against the consumer, through targeted advertising, data sales or other exploitation. Whether giving consumers control over these uses helps them, and what it costs firms and society, is a question for regulators and for operations managers of e-commerce platforms alike.
F. Xu, X. Wang and F. Zhang, Consumer Privacy in Online Retail Supply Chains (Management Science, forthcoming), build a stylized model in which both uses of data appear and the consumers' disclosure decisions are taken under rational expectations. This mission formalizes the paper's single-firm result: when one vertically integrated e-commerce firm sells directly to consumers, the GDPR always raises the firm's profit and social welfare, but it raises consumer surplus only when the product's valuation is below an explicit threshold. A companion mission treats the supplier–retailer chain of the same paper, where the GDPR can hurt all three parties.
A unit mass of consumers values one product at . A consumer's inconvenience cost is uniform on . The data quality is , and monetizing data at intensity costs the firm with . Write
The firm first decides whether to collect data (), then sets a price . Production is free. A buyer who hides her data gets . A buyer who discloses gets : the data scale her inconvenience down by the factor , and the firm extracts from her. Without collection only hiding is available. A consumer buys iff her best buying utility is nonnegative.
Two data policies are compared.
The firm's profit is . Consumer surplus is the integral over of each consumer's realized utility (zero for non-buyers), and social welfare is profit plus consumer surplus. A subgame-perfect equilibrium (SPE) is a profile with an REE response after every , an optimal price over after each , and an optimal .
Let . SPEs exist under both policies, and for every SPE of the mode and every SPE of the mode,
The theorem separates two effects of the GDPR on consumers. The direct privacy effect removes the exploitation loss of every discloser. The indirect pricing effect works the other way: without the exploitation revenue the firm no longer discounts the price to attract disclosers, and once the market under the GDPR is fully covered the firm raises the price sharply. The threshold says exactly where the second effect overtakes the first. The result that profit and welfare rise regardless of shows that in a single-firm market the GDPR is never welfare-reducing; the supply-chain mission shows that this conclusion fails once a supplier sets a wholesale price, which is the paper's main policy message.
The paper's proofs (e-companion, Appendix C, pp. ec21–ec24) work with closed forms and leave several steps to "it can be verified". A formal proof checks the reduction from the game to those closed forms: existence and uniqueness of the REE at every price including the saturated range, global optimality of the prices over all of , and the collection decision against the full no-collection subgame. To our knowledge no part of this paper has been machine-checked.
The obvious argument plugs the printed formula into the profit (3) and maximizes. That formula solves the REE condition only while the market is not saturated; on the saturated range the REE intensity is the constant , and the profit is a different function of . The firm's problem is therefore a maximization of a piecewise function with a kink at full coverage, and the price comparison has to cover prices above (no sales) and the subgame without collection.
The consumer-surplus comparison involves two piecewise quadratics with different breakpoints, , and their single crossing at lies in the middle region where one mode is saturated and the other is not. Strictness of the profit and welfare comparisons needs the identity and its relatives.
All objects are real numbers; , and are hypotheses of every statement. The paper does not state ; at nothing is sold, every outcome is , and every strict claim fails, so is a disclosed standing assumption.
Sets of consumers are measured by Lebesgue measure on ((volume S).toReal); consumer surplus is the interval integral . Indifferent consumers buy and disclose (a null set). The REE uses an IsMaxOn condition over and the disclosing quantity defined from utilities; neither nor is hard-coded. The firm's profit is defined from the REE response, not from the paper's (3). A strategy profile specifies a price for both collection decisions and an REE response at every with ; the comparisons in the goal are between on-path outcomes of such profiles.
The goal is not a comparison of printed closed forms: those are milestones 6–7. It asserts existence of an SPE in each mode, so "every equilibrium" is not vacuous; no price range is restricted and no off-path action is omitted.
Display (2) is stated in its corrected two-branch form for ; Lemma 1 is stated for , with the REE intensity at . The paper's Table 1 (p. 12) misprints the purchase condition of disclosers and is not used.
A complete development needs volumes of intervals, the REE fixed point, maximization of concave piecewise quadratics over , and square-root threshold algebra. No probability or limits are involved. The consumer-stage definitions are shared verbatim with the supply-chain mission and may later be merged. Proofs of any milestone, and of auxiliary lemmas such as , are welcome.
Large online retailers such as Amazon run two businesses on one storefront. They sell products themselves, and they host a marketplace on which third-party sellers sell, paying the platform a percentage of their revenue. A retailer that also runs the marketplace can decide which products to sell itself, and it controls which offer most consumers see. Competition authorities have asked whether this dual role lets the platform appropriate third-party sellers' business, and empirical work (Zhu and Liu, 2018) finds that Amazon enters only a small, high-performing subset of marketplace products.
Hervas-Drane and Shelegia (Retailer-Led Marketplaces, Management Science, 2025) give a model in which these choices can be computed. Its main result, Proposition 2, says which products the platform sells itself when its assortment is limited. This mission formalizes that proposition together with the pricing and entry results it rests on.
There is a unit mass of products. Each product is an independent market indexed by its consumers' valuation . Valuations are distributed according to a probability measure on with CDF . Every unit costs to supply. Each market has a unit mass of unit-demand consumers, who buy at a price only if .
The monopolist retailer sets an ad valorem fee on the third-party seller's revenue. He can steer a share of consumers (the inattentive ones) to the seller of his choice; the remaining buy from the cheapest offer, with ties going to . He has capacity : he can supply at most a fraction of all products.
The game has three stages. In Stage 1 sets . In Stage 2 each product's third-party seller decides whether to enter, and then chooses which products to enter. In Stage 3, in each market both present firms price sequentially: quotes first, then quotes and steers. The solution concept is subgame perfect equilibrium.
Proposition 1 solves Stage 3. A product supplied by alone (SBM) earns him . A product supplied by alone (SBT) earns her and earns him the fee . When both supply it (SBMT), charges
and earns . Lemma 1 says enters exactly the products , the marketplace products. An allocation of is any measurable set of products with . His total profit is the SBM profit on below , plus the SBMT profit on above , plus the fee on marketplace products outside .
Assume (Assumption 1) and . Let and
Then:
Proposition 2 is the step that the rest of the paper builds on. Display (4) writes the monopolist's profit as a function of the fee by plugging in the thresholds , , , of Proposition 2. The optimal fee (Lemma 2, Proposition 3) and the policy comparisons of §6 (a pure-retailer response, fee regulation, steering bans) are all statements about that function. The two modes are also the paper's empirical prediction. A platform with little capacity, effective steering and a high fee competes only in the top marketplace products. With more capacity it also takes products no third party sells.
The paper proves Proposition 2 in Appendix A. The proof is an informal capacity-allocation argument. No machine-checked version exists. A formal proof has to turn the argument about entering the products of highest marginal profitability first into a statement about all measurable allocations of mass at most . It must also prove uniqueness up to null sets, and handle the corners , and that the prose passes over.
The obvious argument ranks products by the marginal profitability of entry and fills capacity from the top. Two facts make this harder than it looks. First, the ranking is not monotone in . Below the gain is ; above it is , which starts again from at . So the optimal set is an upper level set of a piecewise function, and in Mode II it has two components. Second, the claim is about every measurable set of mass at most , not about thresholds. Optimality needs an exchange argument against arbitrary sets, and uniqueness needs the level sets of the gain to be -null. Locating the thresholds also needs continuity and strict monotonicity of , which come from the density and the full-support hypothesis.
Proposition 1 has its own subtlety. At the monopolist is indifferent between matching 's price and charging . 's best price exists only if 's strategy breaks this tie in 's favour, so the equilibrium has to be stated for strategies defined at every price of .
Products form a probability measure μ : Measure ℝ. The standing hypotheses are:
Integrable (fun v => v) μ, which the paper never states but which is needed for profits to be finite;The foreclosed corner () is not covered. Marketplace products are encoded as . Optimal allocations quantify over all measurable sets of mass at most , and uniqueness is up to -null sets. Restricting allocations to intervals or to unions of two intervals would assume the conclusion, and the formalization does not do it.
In Proposition 1, 's strategy is a function of 's price that is a best response at every price, and 's price is optimal against it. Uniqueness of the SBMT outcome is stated only for and , where it holds. Lemma 1's duopoly clause likewise needs .
Two definition files carry the model:
Model: , the marketplace set, the Proposition 1 payoffs, , , , allocations and profit;PricingGame: the three pricing games and their equilibria.The bathtub-type lemma behind Proposition 2 is reusable beyond this mission: among measurable sets of mass at most , an upper level set of a weight maximizes its integral. Contributions of that lemma, of the milestones, and of alternative proofs are welcome.
During the COVID-19 pandemic most U.S. payers began reimbursing a telehealth consultation at the same rate as the corresponding office visit, a policy called pay parity. Many states have since made it permanent, on the stated ground that it improves patients' access to care. In acute care (primary and urgent care) a telehealth visit sometimes cannot resolve the problem and the patient must also come to the office: a duplicate visit. Duplicate visits are paid as well, and they consume office capacity.
Çakıcı and Mills (MSOM 2024; this mission follows the SSRN working-paper version of August 19, 2024) model a provider who splits capacity between an office and a telehealth channel, and patients who choose a channel strategically. Their main finding for the setting in which demand exceeds capacity is that pay parity can make the provider's revenue-maximizing choice and the access-maximizing choice disagree: for a moderate duplicate-visit probability the provider prefers telehealth while patients are better served by an office-only practice. This mission formalizes that result and the equilibrium analysis on which it rests.
A provider serves at total rate and devotes the fraction of its capacity, the telehealth commitment, to telehealth. Episodes of care arrive at rate . Each patient balks (value ), visits the office, or uses telehealth; a telehealth visit needs a duplicate office visit with probability . A resolved episode is worth ; waiting costs per unit of sojourn time; the co-payments are and ; an office visit costs an extra inconvenience . With the proportions choosing the office and telehealth, the expected sojourn times are
and the expected utilities are (office) and (telehealth). A patient equilibrium is a split in which every action used is a best response.
The paper assumes , , and, with , that . In the large-market setting some patients balk at every . There the equilibrium is of one of four types, by region of : balk/office on , balk/office/telehealth on , balk/telehealth on , all-balk on , with explicit thresholds and explicit proportions . The patient access rate and the provider's revenue rate under telehealth reimbursement (office revenue ) are
The commitment that maximizes telehealth usage in the balk/telehealth region is .
Fix all parameters except and , with . There are thresholds such that, for every admissible , pay-parity revenue is maximized over at when and at when ; access is maximized at when and at when ; and for
The thresholds are existential; no closed form is fixed, so the statement survives any later computation of them.
In attack order: Lemma 2 (order of ); Theorems 1–3 (where each equilibrium type occurs) and Lemma 3 (); Theorem 4 (shape of in ); Corollaries 1–2 (the maximizers of and are or ); Proposition 3 (the two thresholds). Two further items are not milestones: the uniqueness of the large-market equilibrium proportions, and Proposition 5 (the reimbursement aligns the two objectives).
The result is the paper's argument against pay parity in acute care: when duplicate visits are neither rare nor frequent, paying telehealth at parity induces the provider to adopt it although fewer patients are then seen. Proposition 5 shows the misalignment disappears under the less-than-parity reimbursement , which pays the same per patient seen through either channel. The thresholds and are what turn this into a policy statement about measurable duplicate-visit rates.
The paper proves these results by hand. None of them has a machine-checked proof, and nothing about strategic channel choice with duplicate service exists on Prove2Me. Formalizing them checks a case analysis with four regions, two square-root closed forms and an intermediate-value argument in . The formalization has already exposed two places where the printed statements need a hypothesis (see Formalization scope).
Each step is elementary; the difficulty is bookkeeping. The equilibrium characterization requires solving the indifference conditions in each region and choosing the root of a quadratic that gives stable queues. The shape results require continuity of and across region boundaries and concavity of a function of the form . The obvious comparison of the closed-form values at and at does not suffice on its own: the closed-form value at is the revenue only when lies in the balk/telehealth region, which fails for some admissible parameters. Whether that failure matters for the maximization is the central question.
All objects are real-valued closed forms in the namespace TelehealthParity.Access. The definition Setting holds the parameters (the arrival rate is lam, since λ is a Lean keyword), , the region-wise proportions, , , the large-market condition and the predicate Admissible p q. The definition Equilibrium holds the sojourn times, utilities and the equilibrium predicate. Conventions:
Admissible p q collects , assumption (6), Lemma 2's ordering condition, the large market, and . The last is not printed; the proof of Lemma 2 presumes it, and Lemma 2 fails without it.IsMaxOn over ; "linear" is affine.Excluded trivializations. , and are closed forms, not suprema or argmaxes. The goal states the strict misalignment and the full threshold characterization, not a comparison with one point. A sorry-free sanity check shows that the hypotheses hold on an admissible instance in the misaligned range (, , , , , ).
Welcome contributions are proofs of any milestone. The real-analysis lemmas (concavity of , maximization of piecewise functions that are continuous across region boundaries) are reusable beyond this mission.
Large technology firms often buy small startups mainly to hire their staff, a practice known as acquihiring. Antitrust authorities review acquisitions that may reduce competition in product markets, but an acquihire can instead reduce competition in the labour market: a firm that buys the employer of a scarce worker no longer has to outbid that employer for her. Bar-Isaac, Johnson and Nocke study this effect in a three-player model: a startup, its essential employee, and a potential acquirer (CRC TR 224 Discussion Paper No. 500, 2024; published in Management Science, 2025, doi:10.1287/mnsc.2024.04604).
In the paper's baseline model (Proposition 1) the acquirer, whenever it hires the employee, does so by buying the startup, and the employee always prefers direct wage competition. This mission formalizes §6, where the employee's private benefit from staying at the startup is her private information. That uncertainty softens wage competition, so acquihiring is no longer always chosen, and the paper derives the exact threshold at which the acquirer switches.
An employee produces value if she works for the acquirer and if she works for the startup. At the startup she also enjoys a private benefit , which only she observes and which is uniformly distributed on . She has an outside option worth , and wages are unrestricted real numbers. The standing assumptions of §6 are
The acquirer chooses between two modes.
A pair is an equilibrium of this wage game when each offer is a best response to the other over all real wages.
The quantities named in the statements are Lemma 5's wages
the indifferent type , and the threshold
Under the standing assumptions, , is a direct-hiring equilibrium, and
In addition, every type of employee is strictly better off under direct hiring than under acquihiring.
The proposition separates two effects that coincide in the baseline model. Without private information, wage competition is Bertrand-like: the winning firm must match the losing firm's full willingness to pay, so buying the competitor is always cheaper. With a privately known benefit, competition between the two employers resembles product differentiation, and each offers less than the employee's productive value. Direct hiring then becomes profitable when is close to , and acquihiring is chosen only when exceeds . Corollary 4 compares this threshold with the efficiency threshold and finds a band of parameters in which acquihiring occurs although it lowers total surplus. That band is the paper's case for labour-market scrutiny of acquisitions.
The results are proved on paper, by first-order conditions and a quadratic comparison. None of them has a machine-checked proof, and the platform has no prior formalization of wage competition, monopsony or acquisitions. The mission adds an explicit Bayesian wage game with expected profits written as integrals over the type distribution, with global best responses rather than first-order conditions. The objects are small enough to be reused for other two-firm wage-posting models with a uniformly distributed taste shock.
The algebra of Proposition 5 is a quadratic inequality in . The work is in Lemma 5. The page solves first-order conditions inside the region , , where both expected profits are concave quadratics. An equilibrium, however, requires that no deviation pays anywhere on the real line, including offers so low that no type accepts and offers so high that every type accepts. Outside the interior region the profit functions are piecewise (zero below, linear above), and each piece has to be compared with the interior optimum. The expected profits are interval integrals of indicator functions, so evaluating them requires the measure of the set of accepting types. Ties between the two offers occur with probability zero, and the statements are insensitive to how they are broken.
All quantities are real numbers. The parameters , , form a structure, and the five standing inequalities form a predicate that every theorem except the pure-algebra milestone takes as a hypothesis (that milestone needs only ). Expected profits, the poaching probability and direct-hiring welfare are of bounded, piecewise-constant integrands, hence interval integrable. A verification file evaluates the acquirer's profit at Lemma 5's wages to its closed form on one instance, and exhibits instances of both branches of the proposition and of the window in Corollary 4. Ties go to the startup.
Conventions committed to:
The direct-hiring profit is an integral over the type distribution evaluated at wages that are proved to be an equilibrium. It is not a closed-form payoff taken as a definition. Dropping any standing inequality would change Lemma 5 (the poaching probability leaves ) or Proposition 5 (the second root comes back into range). The employee-preference clause is part of the goal, and no equilibrium is claimed unique beyond what the page derives.
Contributions welcome: the interval-integral evaluations of step functions, the global best-response argument for Lemma 5, and the quadratic comparison with .
Technology firms often buy small startups mainly to obtain their staff, a practice known as acquihiring; Chatterji and Patro (2014) identify 98 such deals between 2009 and 2013. Bar-Isaac, Johnson and Nocke (CRC TR 224 Discussion Paper No. 500, 2024, www.crctr224.de; published in Management Science, 2025, doi:10.1287/mnsc.2024.04604) study the labour-market side instead. A firm that wants a startup's essential employee can compete for her in wages, or it can buy her employer and so remove the only rival bidder for her services. Their baseline model, the subject of this mission, isolates that choice. It shows that whenever the acquirer hires the employee, it does so by buying the startup, and that the employee is always worse off as a result.
This mission is the first of a series of three on the paper. The second formalizes the extension with Nash bargaining over the price and possible poaching after a failed bid (Proposition 2). The third formalizes the version in which the employee's private benefit is private information (Proposition 5).
There are three players: a startup , an employee , and a potential acquirer . The employee generates value when working at the startup and when working at the acquirer. At either firm she is paid a wage of at least the floor (written wl in Lean), and at the startup she also enjoys a private benefit . Throughout the paper,
In Lean these four numbers form the structure Params (fields va, vs, b, wl), and the displayed assumption is the predicate Params.Standing.
The acquirer first chooses a mode.
The paper restricts attention to equilibria in undominated strategies: no firm offers or bids more than its willingness to pay (footnote 13). A continuation equilibrium of each mode is a profile (offers, bid, and the accept/decline rules of the employee and of the startup at every possible offer) in which every player best-responds, both on and off the path of play. The total surplus of an outcome is if the employee ends up at the acquirer and if she stays; wages and the price are transfers. An outcome is efficient when its surplus equals .
For every continuation equilibrium of the direct-hiring subgame and every continuation equilibrium of the acquihiring subgame:
where denotes the acquirer's payoff and the employee's payoff under each mode. The goal also states that continuation equilibria exist away from the knife edges (direct hiring) and (acquihiring), so that the universal statements are not vacuous. In words: if the acquirer hires the employee, which happens exactly when , then it does so through acquihiring, and the employee always prefers direct hiring.
The proposition carries the paper's main message in its simplest form. Buying the startup removes wage competition: the acquirer pays the startup its retention profit and then pays the employee only the floor . It never compensates her for the private benefit she loses. As a result, acquihiring occurs whenever , including the range in which it destroys surplus, and the employee loses relative to direct hiring in every case. Formalization adds a fully explicit version of the equilibrium analysis. The paper calls Lemmas 1 and 2 "immediate" and does not spell out the employee's tie-breaking or the off-path behaviour that the equilibrium concept requires. Here each subgame is an explicit predicate on strategy profiles, so a complete proof also has to show that the stated outcomes are the only ones. The results are proved in the paper. No machine-checked proof of them is known, and the platform currently has no formalization of acquisitions or of wage competition between firms.
The algebra is elementary; the work lies in the uniqueness half of Lemma 1. Exhibiting one equilibrium is routine. Showing that every equilibrium has the stated outcome requires ruling out each alternative: a winning offer above the rival's reservation level can be undercut, and a losing firm with surplus left can overbid. Each deviation has to be shown both feasible (at least , which is where the standing assumption enters) and profitable against the employee's rule. A naive treatment that fixes the employee's choice only on the equilibrium path fails, because a firm's deviation could then be "punished" by an employee who chooses the worse offer. A treatment with strict tie-breaking fails too: when the acquirer would want the unattained infimum , and no equilibrium would exist. Lemma 2 needs the same care with the startup's acceptance rule. There, the bid is not unique when .
All quantities are real numbers. The direct-hiring profile DHProfile consists of the two offers and a Bool-valued acceptance rule acceptA x y defined at every pair of offers . The predicate IsDHEquilibrium requires:
The acquihiring profile AHProfile consists of the bid, the startup's acceptance rule at every bid, and the two post-bid wages. The predicate IsAHEquilibrium requires:
The standing assumption ( and ) is a hypothesis of every theorem. Footnote 13 enters only through these caps. The other hypotheses added relative to the page are:
The knife edges and are not covered by the page's case distinctions, and the corresponding clauses stay conditional on strict inequalities. Milestones 3–4 and the employee's preference hold at the knife edges as well and are stated without exclusions.
The payoffs are never defined by their closed forms ( or as definitions would turn Proposition 1 into arithmetic), the standing assumption and the employee-preference clause are never dropped, and the declined bid is never claimed unique.
All definitions live in AcquihiringMonopsony.Baseline.Model. The direct-hiring wage game, an asymmetric Bertrand contest for a single worker with a private benefit at one firm, is reusable for the other missions of this series. Contributions are welcome at every level: proofs of the two lemmas, of the payoff identities, and of the goal from them.
Online marketplaces such as Amazon are both the storefront of third-party sellers and a retailer in their own right. A platform that observes how well a seller's product sells can later launch a competing product in the same space, and empirical work finds that it does so selectively: Zhu and Liu (2018, Strategic Management Journal) report that Amazon is more likely to enter product spaces with high sales and ratings. A seller who anticipates this faces a strategic choice about how much to invest in her product before the platform decides.
Qi, Song and Xiao (Management Science, 2025) model this interaction as a two-stage game and ask how the seller's investment responds to the threat of entry. Their answer depends on whether the seller ultimately benefits from the platform's entry, which can happen through spillovers: the platform's own investment in the product space also raises the value of the seller's product. This mission formalizes the case in which the seller does not want the platform to enter, the protective regime, and the paper's characterization of her optimal effort there (Proposition 3).
The parameters are a degree of spillover , a referral rate (the share of the seller's revenue paid to the platform), a competition intensity , the seller's effort-cost coefficient , and the platform's fixed entry cost . The platform's own cost coefficient is normalized to .
In the first stage the seller's product has base value ; she chooses an effort at cost , raising the value to , and sells a quantity at price , keeping the fraction of revenue. In the second stage the platform, having inferred , decides whether to enter. If it does, it invests in the product space and the two compete in quantities.
The paper reduces the second stage to closed forms. Write for the left side of condition (5),
which says that the seller stays in the market after entry and is assumed throughout. With an explicit polynomial denominator , set (equation (8)). The seller's two-stage profits under non-entry and entry are
The platform enters iff the product value exceeds a threshold , where is a second explicit polynomial in (Proposition 1). Hence the seller's total profit is
The protective regime is ; there for every effort. The benchmark efforts and , equations (9)–(10), maximize and respectively.
In the protective regime, with defined by , there is such that an optimal effort is
and the optimal first-stage quantity is .
The result identifies strategic underinvestment as the seller's response to an unwelcome entrant: for intermediate base values she chooses less effort than her first-best so that the product's value sits exactly at the entry threshold. For low base values no distortion is needed, and for high ones the required distortion costs more than entry does. This explains why a seller's investment may fall short of what her own costs and demand would justify, and it is the starting point of the paper's analysis of non-entry commitments (Proposition 5).
The result is proved in the paper; nothing here is open. No part of it is formalized. A machine-checked version adds a complete check of a proof that compresses several steps into "verifiable" remarks: the positivity of and the sign of under (5), and the single sign change of that defines .
The seller's objective is discontinuous at , so the first-order condition alone does not locate the optimum: the candidates are the two unconstrained maximizers and the cutoff, and which one wins depends on . The step that needs care is the existence of a single switching point : it requires comparing the value of the constrained non-entry problem with the unconstrained entry optimum as a function of , and showing that the comparison changes sign once. The polynomial sign facts behind , namely and on the parameter box under (5), are elementary but involve quartic polynomials in three variables.
All quantities are real numbers. The standing ranges , , are hypotheses, as are condition (5) (assumed by the paper from p. 12 on) and (not stated by the paper, but presupposed by its formula for ; with the threshold degenerates to 0). Only the branch of and for which (5) holds is formalized; the paper's proof also covers the regime where (5) fails, with .
The closed forms (6), (7), the entry gain and are definitions taken from the paper. Their derivation from the second-stage Cournot game (Lemmas 1–2) is the subject of the companion mission On the Platform’s Entry I. The piecewise profit is the printed one, with the tie assigned to non-entry.
Efforts range over all of . This is the paper's implicit domain and it matters: the optimal effort is negative for some parameters (for instance , , and slightly above ), so a version restricted to would be false. "Optimal" means a global maximizer, with ties allowed; at two efforts are optimal and at the middle interval is empty.
Trivializing formalizations are ruled out: is pinned by its defining equation rather than chosen, every hypothesis is satisfiable (at , one has ), and the sign conditions keep from collapsing to a junk value of division or square root.
A complete development needs only real analysis of quadratics and polynomial inequalities on a box; contributions of reusable lemmas on maximizing concave quadratics under a threshold constraint are welcome.
A portfolio manager who observes side information (a covariate , such as a market indicator) before choosing a portfolio wants to control the loss of the asset returns conditional on the observed covariate value . The conditional law of given is unknown and must be learned from historical pairs . When itself was never observed, the empirical conditional law is undefined, and kernel or nearest-neighbour estimates are fragile. Nguyen, Zhang, Wang, Blanchet, Delage and Ye (arXiv:2103.16451v3, Operations Research, 2025) robustify the conditional decision with an optimal transport ambiguity set: the decision maker hedges against every joint law of within transport distance of the empirical law. The resulting objective is a ratio of two linear functionals of , so the standard Wasserstein distributionally robust duality (Blanchet and Murthy, 2019; Gao and Kleywegt, 2023) does not apply directly.
The paper settles every regime of the three parameters (ball radius , fiber radius , minimum fiber mass ). This mission formalizes the simplest regime, , where the answer is negative: the worst case does not depend on the data at all.
The covariate space and the return space are Polish spaces with their Borel -algebras. Two ground costs and combine into the separable cost . The data define the empirical measure .
The optimal transport cost between two probability measures on is
the infimum over couplings with marginals and . The ambiguity set is the ball .
Given a covariate value and a radius , the neighbourhood is , and is the fiber set. For a loss at a fixed decision and a law with positive fiber mass, the conditional expected loss is
The paper's standing Assumption 2.4 requires: (i) and are symmetric, non-negative and continuous, and vanishes exactly on the diagonal; (ii) every has a unique projection onto ; (iii) every boundary point of has points outside at arbitrarily small cost.
With the fiber is . With the fiber-mass constraint is taken as the strict inequality , so that the conditioning event is never null.
For every , every and every loss ,
both sides in .
The proposition shows that conditioning on a single covariate value with an optimal transport ball is uninformative: the worst-case conditional loss equals the robust optimization value for every data set. This is what motivates the rest of the paper: either a minimum fiber mass (Theorem 3.2) or a fiber of positive radius (Section 4) is needed for the data to matter. The paper contrasts this with the type- Wasserstein ball, for which it points to existing results to compute the worst case.
For the platform, the mission sets up the shared model of the series: the separable ground cost, the empirical measure, the fiber, the conditional expectation as an extended-real ratio, and the paper's Assumption 2.4. The ball representation (milestone 1) is used by every other mission of the series; it rests on the existence of optimal couplings on Polish spaces, which Mathlib does not yet have. The result is proved in the paper; no machine-checked proof is known to exist.
The statement is an equality of two suprema over very different index sets, and neither inequality reduces to the other. The natural first idea, that the worst case is attained by a small perturbation of the empirical measure, fails: the empirical measure may put no mass on the fiber , or put its mass there at returns far from where is large, and the value must be reached for every data set. Points of the data sitting exactly at are the delicate case, since the transport budget charges for every displacement of mass. The ball representation (milestone 1) is the hard infrastructure step in its "only if" direction: it needs an optimal coupling, i.e. attainment of the transport infimum on Polish spaces, which is absent from Mathlib.
Samples are indexed by Fin N with . The ground cost is as a -valued function. The transport cost reuses the published RWPI.SqrtLasso.transportCost, an infimum over couplings whose first marginal is and second marginal is ; the paper's "min" is not built into the definition. The radius enters as ENNReal.ofReal ρ, and the goal assumes as on the page (). Expectations use the published ModelRiskOT.Duality.extIntegral, in , so the loss is arbitrary: no measurability, boundedness or integrability. The loss stands for at an arbitrary fixed decision, which is how "for any feasible " is read. The fiber at is ; that it equals follows from Assumption 2.4(i). The boundary in Assumption 2.4(iii) is the topological frontier in .
One hypothesis is added to the paper and disclosed: is not isolated for (for every some has ). This is Assumption 2.4(iii) at when the boundary of is read in an ambient Euclidean space, as the paper's remark on p. 11 does; the proof uses it, and without it the statement fails at an isolated that is also a sample point.
Trivializing encodings are excluded: the supremum ranges only over probability measures in the ball with strictly positive fiber mass, so the conditional expectation is never evaluated at a null fiber; no Bochner integral (which is for a non-integrable loss) is used; cannot enter through ofReal; and the feasible set is exactly intersected with the positive-mass constraint.
Contributions welcome: the existence of optimal couplings for lower semicontinuous costs on Polish spaces (reusable far beyond this mission), the decomposition of couplings with a finitely supported marginal, and the two halves of the goal.
Ride-hailing platforms are expected to add autonomous vehicles (AVs) to fleets that today consist of human drivers. AVs have a cost advantage: a human driver must earn a reservation wage for every hour on the platform, while an AV owner pays a fixed capital cost per calendar hour and a smaller variable cost per operating hour. Whether that advantage reaches riders as lower prices depends on how the market is organized: who owns the AVs, and whether AVs and human drivers are dispatched on the same platform.
Z. Lian and G. van Ryzin study this question in Capturing the Benefits of Autonomous Vehicles in Ride-Hailing: The Role of Market Configuration (Management Science, 2025). This mission formalizes one of their central results: when a single AV supplier (a monopoly) shares a common platform with perfectly elastic human-driver supply, its choice of AV capacity is a newsvendor problem, and the optimal capacity is the pure human-driver fleet size of the scenario at a critical fractile of the demand distribution. The version formalized here is the authors' 2023 SSRN working paper (abstract 3716491, version of 23 August 2023); all theorem and equation numbers refer to it, not to the published article.
Vehicles and demand. Riders' values for a ride-hour are uniform on . In a scenario with potential demand mass , serving the demand rate requires the price , and generates the revenue , where is the trip time. Pickup times depend on the number of open vehicles through with and . Minimizing over gives the minimal fleet needed to serve ,
and the maximal utilization . The function is a strictly increasing bijection of ; its inverse is the largest demand that vehicles can serve.
Human drivers (HVs). In this mission HV supply is perfectly elastic at reservation earnings per hour (the paper's ). A demand rate is a pure-HV equilibrium when revenue covers the minimal HV cost, ; among stable equilibria the paper selects the largest, the maximal stable equilibrium , with fleet size . The market is loose when .
AVs. AVs cost per operating hour and per calendar hour, and (Assumption 1). On a common platform, the paper shows (Proposition 6) that the variable profit per AV at fleet size is
Scenarios and the monopoly problem. Demand has scenarios with masses and probabilities . The monopoly chooses a capacity , then a fleet in each scenario:
Let be the smallest index with . In a loose market,
is an optimal capacity for (5).
The result. Proposition 8 says that, on a common platform with elastic human-driver supply, a monopoly AV supplier never undercuts the human drivers' price: in every scenario it deploys at most the pure-HV fleet size, so riders pay the pure-HV price, and the whole cost advantage is retained by the supplier. Its capacity is set by the classical newsvendor trade-off between the margin of a used AV and the fixed cost of an idle one. With a cheap fixed cost the supplier covers the peak scenario; with an expensive one it covers only the lowest scenario and lets human drivers serve the rest. These conclusions drive the paper's policy comparison of market configurations.
Formalizing it. The result is proved in the paper; nothing here is open. No machine-checked version exists. A complete development requires the analysis of (real powers with exponent ), the identification of the maximal stable equilibrium under the loose-market condition, a monotonicity argument for the AV-only profit along the inverse , and the discrete newsvendor argument over a piecewise-linear concave objective. The last part is reusable for any discrete-scenario capacity problem.
The newsvendor step is elementary once the objective is in the form (20). The work lies in reaching (20) from (5). That requires, in each scenario, showing that the maximum over of is attained at . Below this is linear growth; above it, the profit is a function of , an inverse of a sum of a fractional power and a linear term with no closed form, and its decrease rests on the loose-market condition placing beyond the revenue-maximizing demand . Without the loose-market condition the claim fails: in a thin market the only equilibrium is , and the supplier's AV-only profit need not decrease past it. The continuity of at uses the equilibrium identity , which itself depends on identifying the maximal stable equilibrium.
Fin I (0-based): the paper's scenario is index , is a sum over indices strictly above , and "the smallest " is IsLeast.IsMaxStableEq on given numbers , not a choice function.Retail chains increasingly run their physical stores and online channels as one network. A customer who walks into a store and finds nothing she wants can be shown products stocked in other stores of the chain, to be shipped or picked up later. This raises a basic assortment question: when every store can point its customers to the rest of the network, should the stores still carry the assortment each would choose on its own, or should they coordinate?
Liu, Chen, Liu and Wan (MSOM 2025, DOI 10.1287/msom.2024.0761) compare two ways of showing the network's products. Under simultaneous recommendation (SMR), a customer sees her store's products and the other stores' products at the same time. Under sequential recommendation (SQR), she sees the other stores' products only after declining everything in her own store. This mission formalizes the paper's result for SMR, Theorem 1, together with the lemmas of its proof and two consequences (Theorem 5(a) and Proposition 2). The single-store model it builds on is the multinomial logit (MNL) assortment problem of Talluri and van Ryzin (2004).
A seller operates stores and sells products, indexed , with revenues . Product has attraction value , where is its utility; the no-purchase option has attraction value . A fraction of customers first visits store , and .
An assortment profile lists the set offered by each store. Write for the products offered somewhere. A customer of store who buys product from store suffers a utility discount , with . She buys from the cheapest store that offers , so the effective discount is , and if no store offers .
Under SMR, the customer of store chooses product with the MNL probability
The seller's problem is
The single-store problem is
An assortment is revenue-ordered if it is for some . The paper writes for the smallest revenue-ordered optimal solution of (3).
Offering the single-store optimal assortment in every store is optimal under SMR. The goal asserts optimality, not uniqueness: with ties, other profiles can be optimal too.
Theorem 1 says that under simultaneous recommendation the network adds nothing for the seller: the revenue of independently run stores, , is the best achievable. The paper calls this revenue the benchmark. Every later comparison is made against it. The sequential strategy beats it (Theorem 5(a)), and the paper's structural results on SQR and its ½-approximation are phrased relative to and . Proposition 2 shows that adding an online channel enlarges the optimal assortments of the physical stores.
The results are proved in the paper, partly in an Additional Supplement. As far as is known, none of them has a machine-checked proof. The mission produces a reusable Lean model of multi-store MNL choice with cross-store discounts, the SQR choice probabilities, and checked proofs of the single-store threshold structure with discounted outside products (Propositions A.1 and A.2).
A store's SMR revenue depends on every other store's assortment, through both the denominator and the products of . The objective does not separate across stores, so the obvious idea of optimizing each store on its own does not directly apply. Products of other stores enter at reduced weight , so the standard MNL result for (3) does not cover (A.1).
Proposition A.1's exchange argument has two cases, depending on whether the added product is already available elsewhere. In the second case the gain is weighted by , which vanishes when . Proposition A.2 compares optimal values across two discount vectors whose optimal assortments differ.
Products are Fin n (the paper's product is index ), stores are Fin m, and a profile is a function Fin m → Finset (Fin n). The attraction values are the primitive parameters. The discount factor is the largest over the offering stores, and when none offers . In (A.1) the discounts are encoded by the factors , with for . and are predicates: revenue-ordered (hence nonempty), optimal, and of least cardinality among revenue-ordered optima. "Optimal" means a global maximizer, and comparisons of optimal values are written as "for every there is an with ", with no maximum operator. The SMR and SQR objectives are written from the choice probabilities (1) and (2), exactly as the paper writes them.
The standing assumptions are explicit hypotheses: , , strictly decreasing, , , . Two hypotheses are pinned. The first is : revenues are prices, which the paper uses but never states as a sign condition. The second applies only to the second part of Proposition A.1: , because its "if and only if" fails at ; the existence of a revenue-ordered optimum is stated for every . The goal and Proposition A.2 keep , so zero cross-store discounts are allowed. The Gumbel derivation of (2) (Proposition 1, cited from Gao et al. 2021) is not formalized; (1) and (2) are the model.
The hypothesis on is satisfiable: its existence is the first milestone. A statement that assumed some optimal profile, or that defined through a junk-valued supremum, would be trivial or vacuous, and the formalization avoids both. Contributions are welcome on any milestone. Propositions A.1 and A.2 are reusable for other multi-store and omnichannel MNL problems.
Small third-party sellers on e-commerce marketplaces often lack working capital to buy inventory. Two financing channels compete for them. Under trade credit, the supplier ships now and is paid after sales, bearing the seller's default risk. Under platform financing, the marketplace itself (Amazon Lending, Alibaba's microloans, JD's supply-chain finance) lends the seller the purchase cost at an interest rate it chooses, the supplier is paid upfront, and the platform bears the default risk. A platform that already earns a commission on every sale has a reason to lend that a bank does not: cheaper credit raises orders, and higher orders raise commission income.
R. Huang, G. Lai, X. Wang and W. Xiao study this in Platform Financing vs. Trade Credit for Lending to Third-Party Sellers (Management Science, 2024). Their §5 asks how a platform that can set its loan rate freely would set it. The answer at low demand uncertainty is a clean dichotomy in the production cost: the platform lends at exactly its own capital cost when cost is low, and strictly below its capital cost, subsidizing the loan, when cost is high. This mission formalizes that result, Proposition 8, together with the equilibrium analysis it rests on.
The source is the authors' manuscript on SSRN (abstract 4014045, titled Lending to Third-party Sellers with Platform Loan); every page and label below refers to that manuscript, not to the typeset journal article.
A seller with no capital buys units from a supplier whose unit production cost is , and sells all of them on a platform at the market-clearing price . The market size is uniform on with ; measures demand uncertainty. The platform keeps a share of revenue and passes to the seller. The supplier and the platform both have capital cost equal to the risk-free rate , and selling is profitable in expectation: .
Under platform financing at loan rate , the game has two stages after is fixed:
The seller has limited liability: if revenue falls short of the debt , she hands over all of it. The platform's profit is
A subgame-perfect equilibrium at rate is a price and an order rule such that the rule is a best response for the seller at every price, the supplier's price is optimal against the rule, and ties are broken as in the paper. The paper also defines a threshold rate (p. 15) below which the seller prefers platform financing to trade credit; the platform chooses subject to the participation constraint . Write
Let be the platform's profit in a subgame-perfect equilibrium of the stage game at rate , for an arbitrary choice of equilibrium at each feasible rate. If , then
The result separates two motives for platform lending. At low cost the platform gains nothing by undercutting its own capital cost, so the loan is priced at cost; at high cost the commission earned on the extra units ordered outweighs the interest forgone, so the platform subsidizes. The threshold is explicit and depends only on the mean market size, the commission share and the risk-free rate. Together with Proposition 7 of the same paper (whether the platform gains relative to trade credit), it is the paper's account of why marketplaces lend below market rates.
The proof in the paper is a chain of closed-form computations whose final steps are stated as "it can be verified". A formalization checks that chain end to end: the equilibrium of a limited-liability Stackelberg game with uniform demand, the reduction of the platform's objective to (10), and the sign analysis of . To our knowledge none of these steps has been machine-checked. The model file (uniform expectation, limited-liability payoffs, the equilibrium predicate with tie-breaks) is reusable for the two sister missions on the same paper and for other supply-chain-finance models with a uniform market-clearing price.
The objective is defined through an equilibrium, not a formula. The obvious approach, substituting the closed forms of Proposition 2 into the platform's profit, presupposes that every equilibrium has those closed forms; establishing this means solving the seller's piecewise problem (whose objective changes form where default becomes possible), then the supplier's problem over a piecewise best response, and handling the indifference point . Only then does the problem reduce to the one-variable function (10).
On that function, the low-cost case requires a polynomial inequality on a half-open interval in four parameters, and uniqueness needs strict monotonicity, not just a nonnegative derivative. The high-cost case requires both a single sign change of a cubic on and the existence of a maximizer on a set that is open at , where the profit tends to .
All objects live in the namespace PlatformFinance.EndogRate. Conventions committed to:
Corrections relative to the page: (10) is printed under the heading "the equilibrium profits under trade credit" on p. 35, a slip for platform financing; Proposition 8 states while its proof writes , and the statement follows Proposition 8.
A trivializing formalization is ruled out: the goal is stated about the platform's equilibrium profit, not about the closed form (10), and the high-cost clause asserts existence of a maximizer so that "every maximizer is below " cannot hold vacuously.
Needed infrastructure: interval integrals of piecewise polynomials, optimization of one-variable piecewise functions, and real-polynomial sign arguments. Proofs of any milestone are welcome, as are alternative proofs of the cubic sign analysis.
Large asset managers now hold significant stakes in many competing firms at once. When the same investor owns shares in rival firms, managers who weigh that investor's interests have an incentive to compete less hard, which raises industry profits at consumers' expense. This "softening of competition" effect is the subject of a large empirical and antitrust literature (see Azar, Schmalz and Tecu, Journal of Finance, 2018, and the review of Schmalz, Antitrust Bulletin, 2021). A natural question is then why common ownership is not complete: if buying stakes in rivals raises profits, why does an investor not buy the firms outright?
Denicolò and Panunzi (ECGI Finance Working Paper 927/2023; Management Science, 2025, doi:10.1287/mnsc.2023.03467) answer this with a corporate-governance cost. Common ownership is acquired from blockholders who monitor management; as a blockholder sells, his residual stake shrinks and so does his incentive to monitor, so managers appropriate more of the profit. The equilibrium level of common ownership trades off softer competition against weaker monitoring. The mission formalizes the paper's comparative statics of that trade-off with respect to the two corporate-governance parameters.
Two symmetric firms each have a blockholder owning a fraction of the shares; dispersed shareholders own the rest. A financial investor buys the same stake from each blockholder, who keeps the residual stake .
Each firm's manager diverts a fraction of the firm's profit unless monitored. A blockholder's monitoring cuts the diversion to at a private cost per unit of profit, with , , . Given , the blockholder chooses to maximize
and an optimal monitoring rule is a maximizer over for every . In the specification studied here the cost is quadratic, with .
Managers maximize their own firm's profit plus a weight on the rival's profit, where the common-ownership weight is
and measures the investor's influence on managers. Equilibrium industry profit is for a function of determined by the product market.
The large shareholders' payoff per unit of profit is
and their joint surplus is . An equilibrium level of common ownership is a stake that maximizes over .
With the quadratic cost, the equilibrium level of common ownership is monotonically decreasing in and monotonically increasing in :
for every equilibrium at each parameter value. The statement fixes no product-market model: it holds for every positive industry-profit function of .
A companion pair covers the §7.1 variant in which the blockholder himself diverts profits at a quadratic deadweight loss : the optimal diversion (46) and Proposition 9, which states that equilibrium common ownership is increasing in .
Both and measure the quality of corporate-governance institutions: lower values mean fewer opportunities to divert profits and cheaper monitoring. Proposition 3 shows that the two act in opposite directions on common ownership. Stronger legal protection of shareholders (lower ) raises common ownership, while cheaper monitoring (lower ) lowers it. The paper uses this to argue that improvements in governance may have contributed to the rise of common ownership, and that policy aimed at governance has consequences for product-market competition. Proposition 2 gives the bound that makes the comparative statics meaningful: the investor never acquires the blockholders' entire stakes.
The results are proved in the paper by a first-order argument on an interior optimum together with a separate argument for jumps between interior and corner equilibria. No machine-checked version exists. A formalization makes the statement precise in two respects the paper leaves implicit: it holds for every equilibrium, including ties between an interior and a corner maximizer, and for every positive industry-profit function, independent of the product-market model. Along the way it records a slip in (A4), where the constant is rather than the printed ; the paper uses only its sign.
The paper's argument differentiates the first-order condition of an interior optimum and treats jumps of the equilibrium separately through the sign of . Implicit differentiation alone does not give the result: the surplus is not concave in (it can have two local maxima, one at ), the equilibrium need not be unique, and it jumps. A proof for every equilibrium therefore has to compare global maximizers at two parameter values directly rather than follow a differentiable selection.
A second difficulty is that the surplus is built from the optimal monitoring rule as a maximizer, not from its closed form: the step from the optimality predicate to the formula (21) must be proved before any algebra on is available. For Proposition 2 with a general cost, the optimal rule is only implicitly defined, and the comparison near involves a first-order gain in monitoring against a second-order loss in industry profit.
All objects are real-valued. Stakes range over and monitoring over ; an optimal monitoring rule is a function constrained only on residual stakes . An equilibrium is a maximizer of the joint surplus on , ties allowed, and monotonicity is weak and asserted for every pair of equilibria. Derivatives are stated with HasDerivAt, except in the sign milestones, where deriv appears only inside strict inequalities.
Standing assumptions, all explicit hypotheses: and (pp. 7–8); ( is a fraction; is a disclosed pin, needed for the part); (footnote 19's form of ); on , one for both parameter values (industry profit does not depend on and ). Proposition 2 assumes twice continuously differentiable with on (the paper says convex but divides by ), and differentiable at with . The companion assumes , which keeps the optimal diversion inside .
The model is the weight (17), the monitoring stage of §3.2.1, and of (13)–(14), and the industry-profit function . Proposition 1 (the bargaining reduction from the investor's offers to the maximization of the joint surplus) and the product-market game itself are not formalized: equilibrium ownership is defined, as in §4.2, as a maximizer of the symmetric surplus, and is arbitrary, so the theorem covers every product-market model of §3.1.3. The paper's derivation of from the product-market conditions is not posed; in milestone 3 that sign is a hypothesis. §4.2's remark on the concavity of the joint payoff is not assumed.
Two trivializing formalizations are ruled out: the surplus is never typed with the closed form of (monitoring is any optimal rule, and milestone 1 is the bridge), and industry profit is required to be positive, since would make every stake an equilibrium.
The development needs only elementary real analysis: one-variable optimization on intervals, derivatives of rational functions, and a comparison of maximizers at two parameter values. A general monotone-selection lemma for functions with strictly increasing differences on an interval would be reusable beyond this mission. Proofs of any milestone, and alternative arguments for the goal that avoid the interior/corner case split, are welcome.
Data brokers sell information about consumers to firms that decide whom to target: a lender deciding whom to offer credit, a retailer deciding whom to mail. Two products dominate this market. A marketing list sells contact information together with an analysis, so that a firm cannot reach the consumer at all without buying. A data append adds information about consumers the firm already knows, so that the firm can act even without buying. Liang Guo's Selling Data to Marketers (Management Science, doi:10.1287/mnsc.2023.01350) studies how a monopoly data seller should design a menu of data products when the buyers' targeting costs are private, and shows that the answer differs sharply between the two products.
This mission formalizes the data-append result in the paper's base model with a binary targeting value: Proposition 3 (p. 13 of the author's manuscript). The companion missions of the series cover marketing lists and the general model with a rotation-ordered family of posterior distributions.
A marketer can take an action at cost . The action yields a value , with with prior probability , so the prior mean is . Not acting yields .
The seller can produce a signal with , where the informativeness is chosen from . The signal probabilities are and , and the posterior means after and are and , computed by Bayes' rule. The standing assumption makes acting worthwhile exactly after the high signal, so a marketer of cost values information at . Serving a marketer with informativeness costs the seller , with and increasing.
Marketers have cost with probability and with probability , privately known. The seller offers a menu of two plans and with fees . Type 's payoff from plan is
With data appends, a marketer who buys nothing can still act on the prior, so its outside option is . The seller maximizes subject to () and (). An optimal menu solves this problem; its informativeness levels are .
The benchmark is the seller's problem when costs are observable: for each type it maximizes over . Any maximizer is an efficient informativeness .
When :
The first claim is an equality of sets: the high-cost informativeness levels of optimal menus are exactly the efficient ones at . The inequalities hold for every optimal menu and every efficient .
The result says that a data seller's distortion depends on the product's form. With marketing lists the low-cost marketers are the high type, their plan is efficient, and the high-cost plan is distorted (Proposition 2, p. 11). With data appends and costs below the prior mean, the outside option falls with faster than the value of information does, so high-cost marketers have the larger willingness to pay. The roles of the types switch, the low-cost plan is distorted, and the direction of the distortion is reversed, giving the paper's "double mirror image" (p. 13). The direction is set by the skewness of the prior through the sign of , not by an assumed single-crossing condition.
The result is proved in the paper, in an appendix argument of a few lines that invokes Topkis's monotonicity theorem. To our knowledge it has no machine-checked proof. Formalizing it makes explicit what the printed proof leaves to the reader: that the constraints dropped in (8) hold at its optimum, that the efficient and optimal informativeness need not be unique, and which regularity of the strict inequalities need.
The obvious argument substitutes the binding constraints, compares first-order conditions, and invokes Topkis's theorem. Three steps of it are not automatic. First, the reduction drops , and the nonnegativity of fees; these must be shown to hold at every maximizer of (8), and holds only because the maximizers of (8) are ordered in the right direction, which is itself a comparative-statics fact. Second, the reduction identifies the optimal menus only if (8) attains its maximum. Third, Topkis's theorem yields only weak inequalities, ; strictness needs the efficient informativeness to be interior and to be differentiable there, which footnote 5 (p. 7) supplies. Without it, both optima can sit at the same corner or .
Everything is stated over in the sub-namespace SellingData.AppendsBinary. The two types form an inductive type CostType with constructors H and L. A Model structure holds , , , , , , weakly increasing on , and the standing assumption for both costs. The posteriors are defined with the divisions of the paper's (2). The outside option is the printed .
Optimality and efficiency are predicates on maximizers, never a chosen maximizer. The optimal menu is defined from the data-append screening problem itself; defining it through (8) would make the first claim of the goal trivial and is ruled out. The goal additionally assumes the part of footnote 5 that the strict inequalities need: continuous on , differentiable on , right derivative at , and as . Convexity and twice differentiability, which the footnote also lists, are not assumed. The milestones carry only what they need: none for the willingness to pay, continuity of for one part of the reduction, and differentiability at the point for the derivative.
A complete development needs Bayes posteriors for a symmetric binary signal, elementary calculus (derivatives, the mean value theorem, extrema on compact intervals), and Topkis's monotonicity theorem, which is on the platform (Theorem 2.8.4) and is referenced by this mission. Proofs of the milestones and of the goal are welcome. Lemmas on the binary-signal posteriors (for instance the identity ) are reusable by the companion mission on marketing lists.
Third-degree price discrimination means charging different prices to identifiable groups of customers. Its welfare effects are a classical question in industrial organization. With linear demands and every market served under uniform pricing, discrimination leaves total output unchanged and lowers total welfare (Pigou 1920). More generally, welfare can rise only if total output rises (Schmalensee 1981; Varian 1985).
Many current markets are two-sided platforms: marketplaces, app stores and payment networks that charge sellers participation fees and differentiate those fees by seller category (for instance, app stores charging games and non-games differently). On such a platform, a seller's presence is worth something to the buyers on the other side. De Cornière, Mantovani and Shekhar (Management Science 71(4), 2025) show that this cross-side benefit overturns the classical conclusion: discriminating between seller types raises seller participation, which attracts more buyers, which raises seller participation further. In their linear model, total welfare rises, and for large enough cross-side benefits every group gains.
A monopoly platform serves a mass one of buyers and two categories of sellers, and , each of mass one.
The platform chooses participation levels, and the fees follow from the inverse demands.
Uniform pricing (). The platform chooses to maximize
At the common fee , type- participation is .
Price discrimination. The platform chooses to maximize
The participant with outside option joins when its net value exceeds . Buyer surplus and type- seller surplus are therefore integrals over from to the participation level of (net value ). Total welfare is .
Assumption 1 (p. 3343) restricts the parameters: (i) ; (ii) .
Two denominators recur: and .
Under , and Assumption 1, both optimization problems have a solution, and for every uniform optimum and every discrimination optimum:
When , all four groups (platform, buyers, low-type sellers and high-type sellers) are strictly better off: a strict Pareto improvement.
The result. Proposition 2 is a counterpoint to the Pigouvian benchmark. In a two-sided market with linear demands, seller-side discrimination can be a strict Pareto improvement, so a blanket presumption against fee differentiation by platforms is not justified on welfare grounds. The comparison also isolates the mechanism. The low-type sellers gain even though the platform could already serve them, and the high types gain only when the buyer-side benefit is large enough. The paper's extensions in §5 (seller-type-dependent buyer benefits, ad valorem fees, competition) start from this baseline.
Formalizing it. The paper proves Proposition 2 by explicit algebra in Appendix A.2. Most of that algebra is printed, but the positivity of is argued only through claims about the roots of a quartic in , which are asserted rather than shown. No part of the argument is machine-checked. A formalization would give:
The model is a small, self-contained template for platform pricing with linear demands, and the same definitions can serve later comparisons (fees, prices, exclusion).
The optimization steps are routine: both objectives are concave quadratics, strictly concave exactly when and , and Assumption 1(i) gives . The integrals have affine integrands. The comparison steps are where the work is.
Two-sided platforms (ride hailing, delivery, freight, cloud capacity) test product changes with user-split experiments: each arriving demand unit is assigned to treatment with probability and to control otherwise. Treated and control units then compete for the same supply, so the outcome of one group depends on the size of the other. This interference biases the standard estimator that compares the value earned by the two groups and rescales by and (Blake and Coey, 2014; Johari, Li, Liskovich and Weintraub, 2022).
Bright, Delarue and Lobel (arXiv:2205.02274v4, 2024; Management Science 2025) model each matching cycle as a linear program and propose a shadow-price estimator that weights the observed demand counts by the marginal values of demand in the experiment's matching problem. This mission formalizes their finite-sample result, Theorem 6: at every market size, the shadow-price estimator is unbiased for the slope of the expected value function at the experiment state. The fluid-limit comparison with the standard estimator (Theorem 4) and the fluid limit of the matching value (Theorem 1) are the subjects of the other two missions of this series.
A matching network has one sink node for each of demand types, one source node for each of supply types, a finite set of intermediate nodes, and arcs that leave a supply or intermediate node and enter a demand or intermediate node. Arc has a value and a capacity . For a density , demand and supply , the matching value is the optimal value of the linear program (2): maximize subject to inflow at at most , outflow at at most , flow balance at intermediate nodes, and . Write and for the -th unit vector.
Rates are a control demand rate , a treatment effect with , and a supply rate . In the partial-treatment market with treated fraction , the demand counts and supply counts are independent. The finite-sample partial-treatment value function is
and the global treatment effect is .
In the experiment with treatment fraction , the platform observes independent control counts , treatment counts and supply counts, and solves the matching problem at . The negative-demand subgradient is and the positive one . The shadow-price estimator is
with the vector at .
For every network, all rates as above, every and every , is differentiable at and
If on , then .
Theorem 6 says the shadow-price estimator measures, in expectation, the derivative of the value function at the experiment state, for every finite market and for every network, with no uniqueness assumption on optimal dual solutions. It is what licenses the estimator outside the fluid limit, where the matching problem is frequently degenerate. Corollary 2 turns it into an explicit bias bound in terms of the curvature of , and the same identity integrated over a uniformly random gives an unbiased estimator of (Theorem 8 of the paper, not part of this mission).
The paper proves Theorem 6 in Appendix C.4.4; none of the statements has been machine-checked. The formalization adds a precise account of the junk cases a proof on paper passes over (infeasible programs at zero demand, the choice of subgradient), a Lean development of Poisson derivative identities that does not exist in Mathlib, and a network-flow LP layer shared with the two sibling missions. Theorem 7 is a discrete-concavity statement about network-flow values that is of independent interest.
The two sides of (14) are expectations under different laws: the right-hand side differentiates an expectation over the total demand in its Poisson means, while the left-hand side is an expectation over the separately observed treatment and control counts of a quantity that depends on both. Differentiating needs control of an infinite Poisson series uniformly in the mean, and differentiability in is a joint statement about all means at once. Computing the left-hand side with the law of the total demand alone loses exactly the information the estimator uses. The finite-sample matching problem is often degenerate, so its optimal duals are not unique; the paper notes that the particular selection is what makes Theorem 6 hold (p. 25), so no argument that treats the duals as interchangeable can work. Theorem 7 is a discrete-concavity statement about network-flow values that needs integrality of the data, and is the hardest combinatorial statement of the mission.
Demand types are Fin nd and supply types Fin ns (Lean index is the paper's type ). A network is a structure with arcs carrying their endpoints by type, values and nonnegative capacities. is the supremum of the objective over the feasible set; for nonnegative arguments the set contains and lies in the box , so it is a maximum. Poisson vectors are products (Measure.pi) of Mathlib's poissonMeasure, and the experiment law is the product of the control, treatment and supply laws; independence across all counts is the paper's standing reading of one Poisson process per type. Derivatives are HasDerivAt, so every differentiability claim is part of a conclusion. Statements follow arXiv:2205.02274v4; its printed slips are corrected as disclosed in each item: (16) carries wherever , Lemma 1's uniqueness presupposition becomes a correspondence of optimal sets, Lemma 4 is stated for arbitrary capacities so that it covers , and (32) drops the redundant conditioning on supply.
Standing hypotheses are , , , , ; Assumptions 1–3 of the paper are not hypotheses of Theorem 6, because its proof uses none of them, and no integrality of capacities is assumed outside Theorem 7. The estimator is (18) applied to and its expectation is taken under the separate laws of control and treatment counts; it is not defined as a derivative, and its expectation is not computed from the law of the total demand. At zero demand, the infeasible value of is multiplied by a vanishing count, so it never affects the estimator.
Useful infrastructure beyond this mission: derivatives of Poisson expectations in the mean, the binomial conditional law of a Poisson split, and value-function facts for capacitated network-flow LPs. Contributions to any milestone are welcome; Lemmas 3 and 5 and (32) are pure probability and independent of the LP layer.
Music streaming platforms collect a subscription fee from each user and have to pass the revenue on to the artists whose content was played. The two rules used in practice are pro-rata (each artist is paid in proportion to their total number of streams, over all users) and user-centric (each user's fee is split among the artists that user played, in proportion to that user's streams). Which rule is fair has been debated by platforms, rights holders and regulators. Bergantiños and Moreno-Ternero (arXiv:2310.11861, Management Science, 2025) study the problem axiomatically, and in their §4 also through cooperative game theory: they associate a transferable-utility game with every streaming problem and ask which revenue allocations no coalition of artists could object to.
This mission formalizes their Theorem 2. It gives an explicit description of the core of that game.
There are artists and a finite set of users, each of whom pays , so is to be shared. A streaming problem records the number of times user played artist . Every user in is assumed to have played at least one artist.
This is a pessimistic estimate of what a group of artists could earn by leaving to found its own platform. Because every list is nonempty, .
The proof goes through two classical objects of cooperative game theory. The Harsanyi dividends are . A sharing system assigns to each nonempty coalition a probability vector supported on . The Harsanyi set is the set of allocations that a sharing system induces. The unanimity game has if and otherwise.
Theorem 2 says that the core-stable allocations of streaming revenue are exactly those that split each user's fee among the artists that user played. The user-centric rule is such a split, so its rewards always lie in the core. The pro-rata rule can fall outside the core: in the paper's Example 1 a coalition of one artist receives less than the fee of the user who played only that artist. This observation underlies the paper's Theorem 3, where core selection together with homogeneity and additivity characterizes the user-centric index. Beyond streaming, the theorem gives an explicit core for a class of games built from users' lists. The museum-pass games of Ginsburg and Zang have the same structure.
The paper's proof combines two cited classical theorems (Harsanyi's unanimity decomposition and Vasil'ev's identification of core and Harsanyi set for games with nonnegative dividends) with bookkeeping specific to streaming. None of these is formalized on the platform except the bare existence of a unanimity decomposition (Young 1985's exists_unanimity_expansion, Proved, referenced here). The mission therefore produces reusable statements of Harsanyi dividends, the Harsanyi set and Vasil'ev's theorem for arbitrary finite TU games, as well as the streaming result itself.
Most of the mission is finite bookkeeping: Möbius inversion over the subset lattice and regrouping sums by users' lists. The central difficulty is the inclusion in Vasil'ev's theorem. One has to show that every core vector can be generated by splitting each dividend among the members of its coalition. This is a feasibility statement for a transportation problem whose supplies are the dividends and whose demands are the core payoffs, with each coalition allowed to ship only to its own members. The core inequalities have to be turned into such a shipment plan, and neither of the obvious candidates does that. Splitting each dividend equally among a coalition's members gives the Shapley value, a single point. Taking extreme points of the core gives the marginal vectors, and writing an arbitrary core point through them is the same feasibility question again. The paper cites the result without proof.
Fin n, numbered from . Users are named by natural numbers. A problem is a finitely supported map t : ℕ →₀ (Fin n → ℕ) with t j i ; the user set is its support. Every user in therefore has a nonempty list, which is the paper's standing assumption (recalled on p. 19). Streams are natural numbers. The empty problem is allowed; there both sides of Theorem 2 are .Fin n → ℝ. The core is the published Supermodularity.Cooperative.Core Finset.univ. Convexity is the published Supermodularity.Cooperative.IsConvexGame. The unanimity game is the published MonotonicSolutions.StrongMono.unanimity.