Algorithmic Game Theory

Completed

Economics Operations Research Optimization·Captain: mikedeng1

Improving Access to Rare Disease Treatments: Subsidy, Pricing, and Payment Schemes I: With Manufacturer Pricing, Subsidize Only the Manufacturer; Outcome-Based Pay Raises the Price iff B < k − 1/8Research Paper

Motivation

Treatments for rare diseases can require substantial research and development spending while reaching a small patient population. A public subsidy can cover part of the manufacturer's development cost, part of the patient's price, or both. Which recipient should receive the subsidy depends on how the manufacturer responds. A further design choice is whether the manufacturer is paid when a drug is sold or only when treatment succeeds. Olsder, Martagan, and Tang formulate these choices as a sequential game between the government, a manufacturer, and patients in their SSRN working paper, §§3–4. This mission concerns their results for the case in which the manufacturer sets the price.

The paper reports that a manufacturer subsidy alone is optimal under either payment scheme and that the relative prices under the two schemes change with the government budget. The price comparison is useful because a payment contract intended to protect patients can change the price set by the manufacturer. The mission uses the working paper dated 2019-11-13. Its page and equation numbers are those of that version, which precedes the published article.

Setting

The government first chooses two subsidy shares: $\alpha\in[0,1)$ covers the fraction $\alpha$ of research cost and $\beta\in[0,1)$ covers the fraction $\beta$ of the unit price paid on a patient's behalf. The manufacturer then chooses a nonnegative unit price $p$ and a positive target efficacy $e$ . Research cost is $ke^2$ , with $k>0$ , so the manufacturer's effective cost is $(1-\alpha)ke^2$ . The government has a budget $B>0$ . The market size is one, and patient valuations are uniform on $[0,1]$ ; these conventions are given in §3.1–§3.2.

In Setting (1A) the manufacturer receives the price for every sale. Its profit is $\pi_A=p(1-(1-\beta)p/e)-(1-\alpha)ke^2$ . At price and efficacy $(p,e)$ , patient welfare is $W_A=(e-(1-\beta)p)^2/(2e)$ , while government spending is $M_A=\alpha ke^2+\beta p(1-(1-\beta)p/e)$ . These are the paper's equations (2), (3), and (5). In Setting (1B) payment occurs only if treatment succeeds. The corresponding expressions are $\pi_B=ep(1-(1-\beta)p)-(1-\alpha)ke^2$ , $W_B=e(1-(1-\beta)p)^2/2$ , and $M_B=\alpha ke^2+e\beta p(1-(1-\beta)p)$ , from equations (7), (8), and (10) of the same source.

For each scheme, a manufacturer best response is a pair $(p,e)$ maximizing that scheme's profit over all $p\ge0$ , $e>0$ . A government policy is optimal when it has a best response at which spending does not exceed $B$ , and its patient welfare is at least the welfare of every feasible policy evaluated at every manufacturer best response. This expresses the government's leader role and the manufacturer's follower role in the game's sequence of events, rather than assigning the closed forms of §§4.1–4.2 to either player by definition.

Formalization targets

Government policy under each payment scheme

Proposition 1 of the working paper, p. 12, gives the unique optimal policy under sales-based payment. The paragraph after (16) on p. 13 says the same policy is optimal under outcome-based payment:

(\alpha,\beta)=(\alpha^*,0),\qquad \alpha^*=\frac{1+128Bk-\sqrt{256Bk+1}}{128Bk}.

The budget binds at this policy. In both settings the optimal patient welfare and the manufacturer's profit equal $2B/(\sqrt{256Bk+1}-1)$ . These policy claims, the two best-response formulas, and the two welfare and spending reductions form the six milestones.

Price comparison

Corollary 1 on p. 13 compares the manufacturer's optimal price in the two payment schemes. If $p_A$ and $p_B$ denote prices at optimal policies and best responses, the goal is the three-way statement

B<k-\tfrac18\Rightarrow p_A<p_B,\qquad B=k-\tfrac18\Rightarrow p_A=p_B,\qquad B>k-\tfrac18\Rightarrow p_A>p_B.

The printed second clause uses $B\ge k-1/8$ and says “higher”; equality of the two prices at the threshold is a boundary slip. The formal target records equality separately and preserves the strict high-budget comparison.

Significance

The policy result identifies which subsidy reaches patients most effectively within this model: when the manufacturer sets the price, the government uses its entire budget on the manufacturer's development cost, regardless of whether payment is per sale or contingent on treatment success. The price result adds a distinct comparison. Equal optimal subsidies and equal patient welfare do not imply equal prices; the sign of the price difference depends on $B$ relative to $k-1/8$ . This distinction appears explicitly in the paper's discussion following Corollary 1, pp. 13–14.

The working paper proves these results mathematically. The mission's remaining work is to give machine-checked proofs for the game definitions, both best-response results, both welfare and spending reductions, the unique optimum, and the final price comparison. It does not assert that those proofs have already been formalized. The definitions of attained best response and government optimality can also support later analyses of different subsidy or payment rules.

Difficulty

The government cannot compare the two schemes by holding the manufacturer's choices fixed. The manufacturer optimizes both price and efficacy after observing the subsidy policy, and the two profit functions have different price terms. Even after determining each manufacturer's response, identical formulas for government welfare and spending do not themselves establish an attained and unique optimum on the continuous half-open policy region $[0,1)^2$ . The price comparison then concerns the actual best-response prices at that optimum, including the threshold where the two prices coincide. These dependencies explain why the reduced expressions alone cannot serve as the definition of the game.

Formalization scope

Lean represents all parameters, policies, prices, efficacies, profit, welfare, and spending in $\mathbb R$ . The policy predicate requires $\alpha,\beta\in[0,1)$ . Every theorem assumes $k>0$ ; the budget results also assume $B>0$ . These positivity conditions make the paper's denominators meaningful and state its implicit economic regime. Prices chosen by the manufacturer satisfy $p\ge0$ . Its efficacy choice satisfies $e>0$ and has no imposed upper bound of one: equations (3) and (8) maximize over $e$ , and in the high-budget part of Corollary 1 their optimizer can exceed one. This is a convention of the paper's algebraic model, even though efficacy is introduced as a probability.

The demand expressions used in the paper's equations are left unclipped. At the stated best responses, they lie in the relevant nonnegative range. Best responses are represented as sets of all maximizers, and the goal compares every response at every optimal policy. Government optimality requires a feasible best response and comparison with every feasible competing policy and response, so neither existence nor uniqueness is obtained from an empty set. In particular, the reduced welfare and budget formulas (13) and (16) are milestone conclusions, not definitions of government choice. Reusable contributions include real optimization arguments for joint price and efficacy maximization and for attained welfare maxima over subsidy policies.

Selected references

W. Olsder, T. Martagan, and C. S. Tang, Improving Access to Rare Disease Treatments: Optimal Subsidies, Pricing, and Payment, SSRN working paper 3481150, version of 2019-11-13, §§3–4, pp. 8–14. SSRN.
W. Olsder, T. Martagan, and C. S. Tang, Improving Access to Rare Disease Treatments: Subsidy, Pricing, and Payment Schemes, Management Science, 2023. DOI: 10.1287/mnsc.2022.4634.

8 thms2 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Infinite-Dimensional Fisher Markets and Tractable Fair Division 2: For Linear Valuations on [0,1] the Feasible Utility Set Is a Projection of Linear and Parabolic ConstraintsResearch Paper

Motivation

A Fisher market divides a supply of goods among buyers with different values and budgets. In many fair division models, the goods form a continuum: pieces of time, land, or a divisible resource can be allocated in arbitrarily small amounts. A direct description of all possible buyer utilities then appears to require one allocation function for every buyer. Gao and Kroer show that when values vary linearly along an interval, the same utility set has a finite description using linear constraints and a parabolic cone. This makes the utility possibilities visible to convex optimization methods even though the underlying allocation space is infinite dimensional. Gao and Kroer, §§2 and 4.

The result is a characterization of a set, rather than a claim about one selected market equilibrium. It includes every feasible utility vector, including vectors below the Pareto frontier and cases in which adjacent buyers have identical valuations. The article proves the characterization as Theorem 4 and extends it to arbitrary subintervals and piecewise linear valuations in Theorems 5 and 6. Gao and Kroer, Theorems 4–6.

Setting

There are $n$ buyers and one unit interval of items, $\Theta=[0,1]$ , with Lebesgue measure. Buyer $i$ values item $\theta$ at $v_i(\theta)=c_i\theta+d_i$ . An allocation assigns a nonnegative, essentially bounded share $x_i(\theta)$ to each buyer, with $\sum_i x_i(\theta)\le 1$ almost everywhere. Its utility vector has coordinates $u_i=\int_0^1v_i(\theta)x_i(\theta)\,d\theta$ . The feasible utility set $U(v,[0,1])$ contains all vectors obtained this way, including utilities from allocations that leave some supply unused. Gao and Kroer, (1), p. 8.

The goal assumes normalized valuations, $c_i/2+d_i=1$ , and intercepts $2\ge d_1\ge\cdots\ge d_n\ge0$ . These bounds ensure that each valuation is nonnegative on the item interval. The ordering can contain ties. For each adjacent pair of buyers, the result introduces four real auxiliary variables $(z_i,w_i,s_i,t_i)$ . The pair $(s_i,t_i)$ lies in the parabolic cone $\mathcal C=\{(s,t):s^2\le t\}$ , and a $2\times2$ matrix $G_i$ maps it to $(z_i,w_i)$ . Gao and Kroer, Theorem 4, pp. 15–16.

For the supporting welfare statement, the item space is instead a compact subset of Euclidean space. A buyer's valuation is integrable and nonnegative, prices are integrable and nonnegative, and a market equilibrium gives each buyer a utility maximizing bundle within budget while clearing all positively priced supply. A Pareto optimal allocation admits no feasible allocation that weakly improves every buyer and strictly improves one. These notions are used in Lemma 6 and the path to the interval result. Gao and Kroer, §§2 and 4.1.

Formalization targets

The main target is the full equivalence of Theorem 4:

u\in U(v,[0,1])\quad\Longleftrightarrow\quad u\ge0\text{ and there exist }z,w,s,t\text{ satisfying Theorem 4's linear and parabolic constraints.}

The constraints include $u_1\le z_1$ , $u_i\le z_i+w_{i-1}$ for interior buyers, $u_n\le1+w_{n-1}$ , $G_i(s_i,t_i)=(z_i,w_i)$ , $s_i^2\le t_i$ , $0\le z_i\le1$ , $-1\le w_i\le0$ , and $z_i+w_i\ge0$ for each adjacent pair. The representation quantifies over real auxiliary variables; it does not assume a market equilibrium or a partition into intervals. Gao and Kroer, Theorem 4, pp. 15–16.

The milestones are the paper's continuum second welfare theorem (Lemma 6), the ordered interval structure of equilibrium under Assumption 1 (Lemma 5), the ordered interval domination of feasible utilities (Lemma 7), the breakpoint description in the proof of Theorem 4, and the two buyer region identity in that proof. Theorem 5 is a companion target: it identifies utilities on $[l,h]$ with scaled, permuted utilities for normalized valuations on $[0,1]$ . Gao and Kroer, pp. 14–19 and a10–a13.

Significance

Theorem 4 turns an infinite dimensional feasibility question into membership in a projection of a finite convex set. This lets the interval utility set enter a conic optimization model without choosing a discretization of the item space. Theorem 5 transfers that description to other intervals, and the paper uses these results for piecewise linear fair division. Gao and Kroer, §§4.2–4.3.

The mathematical results are proved in the article. The formalization work here records the precise objects and open Lean theorem statements; machine checked proofs of these new statements remain to be supplied. The generic allocation, demand, equilibrium, and feasible utility definitions can also support later results about continuum Fisher markets and Eisenberg–Gale optimality.

Difficulty

A feasible utility vector may come from a fractional allocation that varies arbitrarily along the interval. The geometric statement, however, describes it with only one adjacent pair of auxiliary variables per buyer boundary. The link must preserve the entire feasible set, including vectors below the Pareto frontier and valuations with equal intercepts. A characterization proved only for equilibrium utilities, or only for distinct valuations, would miss those vectors. Lemma 6 also works over general compact Euclidean item spaces, so its assertion cannot be reduced to the interval case. Gao and Kroer, Lemmas 5–7 and Theorem 4.

Formalization scope

Lean represents allocations and valuations as real functions modulo almost everywhere equality in the statements, rather than as quotient $L^p$ elements. Bundles must belong to $L^\infty$ and prices and valuations to $L^1$ ; their integral pairings are then meaningful. The feasible utility set is defined from allocations and Lebesgue measure restricted to the relevant interval. Buyers are indexed from zero in Lean and from one in the paper. Natural number indices for the auxiliary sequences follow the same shift. The goal requires $n\ge2$ because its first and last adjacent pair constraints do not exist for smaller $n$ ; Lemmas 5 and 7 require $n\ge1$ for their endpoint lists.

The goal includes ties among intercepts. The printed further claim that all feasible auxiliary $s_i,t_i$ lie in $[0,1]$ fails with a tie, so its companion statement assumes the relevant adjacent intercepts are strictly ordered. Theorem 5 reads the valuation as $c_i\theta+d_i$ : that agrees with its normalization and interval integral, while the displayed $c_i\theta/2+d_i$ on p. 18 is inconsistent with those formulas. These readings are recorded with concrete checks in the moderation notes. Gao and Kroer, Theorems 4–5, pp. 16 and 18.

A complete proof will need reusable measure theoretic facts about allocations, interval integrals of linear functions, Pareto optimal utilities, and the image of the parabolic cone under a linear map. Contributions to those foundations and to the listed theorem statements are within scope. The target cannot be met by assuming a breakpoint partition or an equilibrium for the utility vector: it must characterize $U(v,[0,1])$ directly.

Selected references

Yuan Gao and Christian Kroer, Infinite-Dimensional Fisher Markets and Tractable Fair Division, Operations Research, 2023. arXiv:2010.03025v5.

9 thms2 active usersReviewed

Completed

Dynamical Systems Economics·Captain: mikedeng1

Network Externalities and Market Dominance: Under In/Out Demand the Impulse Selects the Introspective Equilibrium by Its Position Relative to the Middle EquilibriumResearch Paper

Motivation

Markets with network externalities can support several levels of adoption at the same price. A consumer's willingness to buy may rise when many other consumers buy, while the ordinary price effect still works in the opposite direction. A price and an aggregate demand curve can therefore identify several self-consistent quantities without identifying which one consumers reach. In Network Externalities and Market Dominance, Akerlof, Holden and Rayo study this selection problem before analyzing firms' pricing decisions (accepted manuscript, §2.1).

The paper uses an introspective equilibrium: consumers begin with an impulse about firm 1's sales and repeatedly revise consumption in response to the previous level. The resulting limit gives a selection rule tied to an observable starting condition rather than to an arbitrary choice among fixed points. The mission formalizes Proposition 1 of the accepted manuscript, dated September 16, 2022. Its source is the repository manuscript; the numbering and printed pages here refer to that artifact, not the journal typesetting (Akerlof, Holden and Rayo, Proposition 1, p. 10).

Setting

There is a unit mass of consumers, each with unit demand. Write $p=p_1-p_2$ for firm 1's relative price, and let $Q\in[0,1]$ be its current total sales. The aggregate demand $D(p,Q)\in[0,1]$ is the quantity that would be demanded at price $p$ if consumers believed sales were $Q$ . With one firm, the paper sets the second firm's price and quantity to zero, so the same two-argument demand map applies. With two firms, $p$ is the difference of their prices. An equilibrium quantity is a feasible fixed point,

Q=D(p,Q).

The inverse demand curve $P$ gives a price at which a given quantity is self-consistent: $D(P(Q),Q)=Q$ for $Q\in[0,1]$ . The market assumptions say demand is continuous in price and feasible quantity, decreases with price, and increases with believed quantity. The formal market records weak monotonicity together with strict price comparisons at an inverse-demand point on the nonsaturated part of the range. These comparisons give the signs used in the paper's footnote 12 (§2, p. 5; footnote 12, p. 10).

An In/Out curve has two quantity thresholds $0<Q_L<Q_H<1$ . The curve $P$ is strictly decreasing and convex on $[0,Q_L]$ , strictly increasing on $[Q_L,Q_H]$ , and strictly decreasing and concave on $[Q_H,1]$ ; convexity and concavity here are weak. Define $p_{\min}=P(Q_L)$ and $p_{\max}=P(Q_H)$ . The endpoint conditions are $p_{\max}<P(0)$ and $P(1)<p_{\min}$ . At a price between the thresholds, the intersections of $P(Q)=p$ with the three branches are $Q^{\mathrm{out}}(p)$ , $Q^{\mathrm{mid}}(p)$ , and $Q^{\mathrm{in}}(p)$ . At either threshold price, two adjacent branch labels can name the same quantity (footnote 7, p. 6; §2.1, p. 8).

The consumers' impulse $I_0$ lies in $[0,1]$ . Level- $k$ consumption is the actual iteration $I_k=D(p,I_{k-1})$ , or $I_k=D(p,\cdot)^{\circ k}(I_0)$ with $I_0$ at level zero. An introspective equilibrium $Q_1^*$ is the limit of this sequence as $k\to\infty$ (Definition 1, p. 9).

Formalization targets

Equilibrium structure

For $p_{\min}<p<p_{\max}$ , the three branch quantities are distinct and exhaust the feasible equilibrium quantities. At $p=p_{\min}$ or $p=p_{\max}$ , two distinct quantities remain. The milestone from §2.1 also records uniqueness within each branch. Footnote 12 records where $D(p,Q)$ lies above or below $Q$ between these intersections (§2.1, p. 8; footnote 12, p. 10).

Selection rule

The goal is the full two-part Proposition 1. When $p_{\min}\le p\le p_{\max}$ , the branch equilibria exist and

Q_1^*(p)= \begin{cases} Q^{\mathrm{in}}(p),&I_0>Q^{\mathrm{mid}}(p),\\ Q^{\mathrm{mid}}(p),&I_0=Q^{\mathrm{mid}}(p),\\ Q^{\mathrm{out}}(p),&I_0<Q^{\mathrm{mid}}(p). \end{cases}

When $p>p_{\max}$ or $p<p_{\min}$ , exactly one feasible quantity solves $Q=D(p,Q)$ , and $I_k$ converges to it for every $I_0\in[0,1]$ . The proof's convergence and uniqueness passages are separate milestones, so the goal retains both claims without taking either as an extra assumption (Proposition 1 and proof, p. 10).

Significance

Proposition 1 ties a market's adoption outcome to the initial impulse. In the multiple-equilibrium price range, the middle equilibrium separates impulses that select the low and high quantities; outside that range, the selected quantity is independent of the impulse. This makes the refinement usable when the subsequent economic analysis asks how a price or a change in expectations can move the market between dominant firms (§2.1–§3).

The paper proves the result in ordinary mathematics. The remaining work here is a machine-checked proof of its precise selection statement and of the source passages that support it. The definition layer also supplies a reusable interface for continuous aggregate demand and inverse demand on a bounded quantity interval. There is no claim that this paper's later pricing-game propositions have already been formalized.

Difficulty

The inverse-demand picture shows three crossings, but a picture alone does not establish that every branch crossing exists or that no additional feasible fixed point is present. At a threshold, two branch labels meet, so a claim that always demands three distinct quantities would be false. Outside the threshold interval, the paper's reference to a unique intersection of $P(Q)=p$ fails at prices beyond $P(0)$ or $P(1)$ : the equilibrium can instead be a saturated fixed point at $0$ or $1$ . The formal statements must cover those prices with $D(p,Q)=Q$ (Proposition 1 and proof, p. 10).

The convergence claim concerns a specific recursive sequence from every allowed impulse. Fixed-point existence by itself does not identify that limit or its dependence on the impulse. The market assumptions also require care at the saturation endpoints: strict decrease in price on the whole real line would conflict with nonnegative demand at $Q=0$ , while merely weak decrease permits extra fixed points that would defeat the selection claim.

Formalization scope

Lean represents prices and quantities by real numbers and restricts feasible quantities and impulses to $[0,1]$ . A Market stores $D$ , $P$ , continuity of $D$ on real prices and feasible quantities, range bounds, weak monotonicity in quantity and price, the inverse-demand identity, and the strict nonsaturation signs from footnote 12. The paper says demand is strictly increasing in quantity below $1$ ; the formal interface uses weak increase because its own saturated consumer model can have a constant zero-demand segment. The strict price signs make explicit the stronger reading of “decreasing” needed at inverse-demand points. Both choices are disclosed in the setting item. The polynomial and clamped-demand example in the local verification file witnesses that the assumptions are consistent.

IsInOut retains every monotonicity, convexity, concavity, threshold-order, and endpoint condition of footnote 7, even when a clause is unused in a proof. The branch quantities are predicates that include their intervals and the equation $P(Q)=p$ ; the goal asserts their existence before quantifying over them. IsIntrospectiveEq uses Function.iterate and Tendsto for the prescribed $I_k$ , so it cannot be satisfied by selecting an unrelated fixed point or sequence. Outside the threshold interval, uniqueness is over feasible fixed points of $D$ , including $0$ and $1$ . The assumptions apply to the aggregate map for either one or two firms; consumer types, their distribution, the micro-foundations, the firms' pricing game, profits, the WIN constraint, Corollary 1, and later sections are outside this mission.

A complete development needs continuity and intermediate-value results, monotonicity and convexity of real functions on intervals, and convergence of bounded sequences of real numbers. The market and level- $k$ definitions can be reused by later work on equilibrium selection. Contributions may prove the listed milestones, supply independent proofs of Proposition 1, or build the interval-dynamics lemmas they require, while retaining the statement's full price and impulse domains.

Selected references

R. Akerlof, R. Holden and L. Rayo, Network Externalities and Market Dominance, author's accepted manuscript, WRAP 178238, dated September 16, 2022; published in Management Science (2024). Accepted manuscript; DOI.

7 thms2 active usersReviewed

Economics Operations Research Optimization·Captain: mikedeng1

Personalized Pricing and Distribution Strategies II: With Personalized Pricing by the Manufacturer, Dual Distribution Is Optimal Iff β > β_PZ(α), and β_PU(α) > β_PP(α)Research Paper

Motivation

A manufacturer can sell directly to consumers and also supply an independent retailer. The retailer reaches consumers for whom its distribution service is more valuable, but its presence can also force the manufacturer to lower direct-channel prices. Jullien, Reisinger and Rey study when the additional sales justify dual distribution under different abilities to personalize retail prices (Jullien, Reisinger and Rey, 2023). This mission isolates their Proposition 4: the manufacturer can personalize its own prices, and the retailer may either personalize or charge one uniform price. The source used here is the authors' March 2022 manuscript; the formal claims follow its Proposition 4 and Online Appendix A.

The question matters for vertical channel design because a retailer's reach and the competition it creates pull industry profit in different directions. The manufacturer and retailer negotiate a wholesale contract before retail pricing. A fixed fee can divide their combined profit, so the distribution decision depends on whether both channels together earn more than the manufacturer's direct channel alone. The model makes that comparison exact for a continuum of consumers rather than treating the retailer's contribution as a general benefit (Jullien, Reisinger and Rey, 2023).

Setting

Consumers have types $x\in[0,X]$ , with one unit of consumer mass per unit of $x$ . A monopoly manufacturer A offers a direct channel, and retailer B offers a differentiated service. Their consumer values are $u_A(x)=\max\{1-x,0\}$ and $u_B(x)=\max\{v-sx,0\}$ . The market parameters satisfy $0<s<v<1$ and $X\ge v/s$ . Thus both valuations fall as the consumer index rises, B's valuation falls more slowly, and the market extends beyond the last consumer with positive value for B. The two values cross at $\hat x=(1-v)/(1-s)$ , with common value $\hat u=(v-s)/(1-s)$ .

The channel contributions measure valuation advantages. A's contribution is $\alpha=\int_0^{\hat x}(u_A(x)-u_B(x))\,dx$ ; B's is $\beta=\int_{\hat x}^{X}(u_B(x)-u_A(x))\,dx$ . They are defined by the integrals. The closed forms in the Online Appendix, $\alpha=(1-v)^2/[2(1-s)]$ and $\beta=(v-s)^2/[2s(1-s)]$ , are milestone results, not substitutions into the definitions.

The manufacturer can instead use mono distribution, selling only through A and charging each consumer the full direct-channel value. Its profit is $\Pi_P^m=\int_0^X u_A(x)\,dx=1/2$ . Under dual distribution, a two-part tariff has wholesale price $w\ge0$ and a fixed fee. The fee allocates the proceeds between firms; industry profit is the total price paid by consumers. Dual distribution is selected only when its industry profit strictly exceeds $\Pi_P^m$ , as specified in the manuscript's footnote 17.

Two retail continuations are relevant. In PP, both firms personalize prices, and the manuscript selects the Bertrand equilibrium where the lower-valued offering prices at its opportunity cost. In PU, B first announces one price $p_B$ , and A then tailors its prices to consumer types. B chooses a globally profit-maximizing price after allowing for A's response. These rules determine each consumer's payment and hence industry profit; they are represented directly in the Lean definitions.

Formalization targets

The central target is Proposition 4. It asserts the existence of functions $\beta_{PP}$ and $\beta_{PU}$ of $\alpha$ alone, valid uniformly across all admissible $(v,s,X)$ , with

\text{dual distribution in PP}\iff\beta>\beta_{PP}(\alpha),\qquad \text{dual distribution in PU}\iff\beta>\beta_{PU}(\alpha),\qquad \beta_{PP}(\alpha)<\beta_{PU}(\alpha).

The valuation-space milestones identify the underlying cutoffs $\tilde v(s)=s(2+\sqrt{1-s})/(1+s)$ in PP and $\check v(s)=s[2+\sqrt{(1-s)(2+5s+s^2)/(1+2s)}]/(1+s)$ in PU. They say dual distribution is strictly better exactly when $v$ exceeds the respective cutoff. Other milestones give the mono benchmark, the formulas for $\alpha$ and $\beta$ , the existence of the two contribution thresholds, and the strict ordering $\tilde v(s)<\check v(s)$ (Jullien, Reisinger and Rey, 2023, Proposition 4 and Online Appendix A).

Significance

Proposition 4 turns a distribution choice involving wholesale and retail prices into a comparison of two channel contributions. It identifies precisely how large B's contribution must be to make a second channel profitable, and it says that B's ability to personalize prices lowers that required contribution. A price policy restriction on B therefore changes the region of market parameters in which the retailer is brought into the channel. The strict threshold statement also distinguishes an actual gain from a tie with mono distribution.

The result is proved in the authors' manuscript, with detailed arguments in Online Appendix A. This mission asks for a machine-checked version of the market definitions, its integral and cutoff identities, and the passage from $(v,s)$ to $(\alpha,\beta)$ . The proposed Lean theorem files contain open proof obligations; compilation of their statements does not supply those proofs. A completed development would give reusable formal definitions of the consumer outcomes and a checked statement of the channel comparison.

Difficulty

The industry profit changes formula as the wholesale price changes which consumers can be served by B. In PP, the profit derivative has different expressions on either side of $w=v-s$ , and the curvature of one region changes with $s$ . In PU, B's uniform price can leave some consumers buying directly from A both before and after B's customer interval. A single interior first-order calculation therefore does not settle the global distribution choice. The contribution thresholds add another step: each cutoff in $(v,s)$ must correspond to a threshold depending only on $\alpha$ , and the two resulting thresholds must retain a strict order along every admissible iso- $\alpha$ curve (Jullien, Reisinger and Rey, 2023, Online Appendix A).

Formalization scope

Lean uses real numbers for $v,s,X,w,p_B$ , interval integrals against Lebesgue measure for profits and contributions, and the Lebesgue volume of B's buyer set for its PU demand. The standing assumptions are exactly $0<s<v<1$ and $v/s\le X$ . Retail prices in B's maximization range over all real numbers; wholesale prices satisfy $w\ge0$ . The continuation fixes an assignment of indifferent consumers. Positive-valuation tie boundaries have measure zero; at $w=0$ , an interval of zero-valuation consumers pays zero in PP. Consumers with $u_B(x)=0$ are assigned to A in PU and are excluded from B's demand. If several uniform prices maximize B's profit, a strict industry gain at one maximizing price suffices in the dual-distribution predicate.

The setting defines industry profits from consumer payments and defines dual distribution by a strict profit comparison. It never defines them from $\tilde v$ , $\check v$ , or the desired threshold functions. The real-valued integrals are well behaved here because the consumer interval is bounded and the integrands are piecewise affine. The cutoff expressions use positive denominators under the standing assumptions. The PU price maximum is global; neither a stationary point nor the first market configuration is built into the definition.

A complete proof needs interval integration of piecewise affine functions, global optimization across the PP and PU price regions, and a comparison of the induced contribution-space thresholds. The integration and market-outcome lemmas can be reused for related channel games. Contributions establishing the stated milestones, or reusable lemmas about these bounded price regions, fit the mission's scope.

Selected references

Bruno Jullien, Markus Reisinger and Patrick Rey, Personalized Pricing and Distribution Strategies, Management Science, 2023. DOI 10.1287/mnsc.2022.4437. Formalization source: authors' manuscript of March 2022, PDF SHA-256 25a6c84ac0c48c6720f6a9e1f9b1f1ec516412c31dac044ac84c1d4c72dfc253, Proposition 4 and Online Appendix A.

9 thms2 active usersReviewed

Economics Mechanism Design Operations Research·Captain: mikedeng1

The Voice of Customers in Customization II: Under O-Learning, the Cheap-Signaling Separating Equilibrium Exists If and Only If θH/θL ≥ ΛResearch Paper

Motivation

Firms that customize products, especially in business-to-business and service markets, need to learn what each customer wants before designing for that customer. Liang Guo's paper The Voice of Customers in Customization (SSRN 3994319; published in Management Science, DOI 10.1287/mnsc.2021.04025) compares two ways a seller can learn a customer's preference. Under A-Learning the customer describes its preference and the seller designs the product. Under O-Learning the customer proposes the design itself and the seller decides whether to accept it. The customer's preference is private, and the price is bargained after the product has been made, so a customer has a reason to misrepresent itself in either case: a customer believed to value quality less is charged less.

This mission formalizes the paper's characterization of when O-Learning reveals preferences without distortion: each customer type requests exactly the design it would request if its preference were public. The paper calls this the cheap-signaling equilibrium. A companion mission in this series formalizes the analogous result for A-Learning (Proposition 1), and another shows that O-Learning has no separating equilibrium at all below the threshold found here.

Setting

A seller faces buyers whose quality preference is $\theta\in\{\theta_H,\theta_L\}$ with $\theta_H>\theta_L>0$ . Each buyer knows its own $\theta$ . The seller holds the prior that a fraction $\alpha\in(0,1)$ of buyers has $\theta_H$ . A product has a quality $q\ge 0$ . Producing it costs $kq^2$ and selling it costs $sq^2$ , with $k,s>0$ . The selling cost is incurred before the price is set. In the price stage either party makes a take-it-or-leave-it offer: the seller with probability $\gamma\in(0,1)$ , charging $\hat\theta q$ where $\hat\theta$ is its belief about the buyer, and the buyer with probability $1-\gamma$ , offering $kq^2$ .

The O-Learning game has three stages.

Each buyer submits a quality request $q(\theta)\ge 0$ .
The seller, holding a posterior belief $\hat\theta(q)$ , accepts or rejects the request. It accepts if and only if its expected profit is nonnegative:

\gamma(\hat\theta q-kq^2)-sq^2\ge 0.

The price is set as above. A rejected request ends the game with payoff $0$ to both parties.

A buyer of true preference $\theta$ whose request $q$ is accepted under belief $\hat\theta$ expects

\mu(q,\theta,\hat\theta)=\gamma\max\{\theta q-\hat\theta q,0\}+(1-\gamma)\max\{\theta q-kq^2,0\}.\tag{9}

A separating equilibrium consists of distinct requests $q_H\ne q_L$ and a belief function $\hat\theta(\cdot)$ satisfying three conditions. Beliefs are consistent on the equilibrium path: $\hat\theta(q_H)=\theta_H$ and $\hat\theta(q_L)=\theta_L$ . Beliefs off the path are arbitrary. No type gains by deviating to any other request $q\ge 0$ .

If the preference were public, the buyer would choose $q$ to maximize $\mu(q,\theta,\theta)$ subject to acceptance. The solution is the first-best request

q^*(\theta)=\min\Big\{\frac{\gamma\theta}{s+\gamma k},\ \frac{\theta}{2k}\Big\}.

The thresholds are

\Lambda_{H1}=\frac{\gamma(s+k)}{(1-\gamma)s},\qquad \Lambda_{H2}=\frac{1+\gamma}{1-\gamma},\qquad \Lambda_L=\frac{s}{\gamma k},\qquad \Lambda=\max\{\min\{\Lambda_{H1},\Lambda_{H2}\},\Lambda_L\}.

Formalization targets

Goal: Proposition 3 (p. 17)

The requests $q^O_H=q^*(\theta_H)$ , $q^O_L=q^*(\theta_L)$ form a separating equilibrium for some belief function if and only if

\frac{\theta_H}{\theta_L}\ge\Lambda.

When this holds, the equilibrium is supported by the out-of-equilibrium belief $\hat\theta(q)=\theta_L$ if $\gamma\le s/k$ , and by $\hat\theta(q)=\theta_H$ if $\gamma\ge s/k$ .

Milestones

In attack order:

Seller acceptance (§3.3, p. 16). For $q\ge 0$ , the seller accepts a request iff $q\le\gamma\hat\theta/(s+\gamma k)$ .
The first-best request solves (10) (§3.3, p. 16). $q^*(\theta)$ is the unique maximizer of $\mu(q,\theta,\theta)$ over the acceptable requests.
The case form of $q^*$ (Appendix, Proof of Proposition 3, p. 28). $q^*(\theta)=\gamma\theta/(s+\gamma k)$ if $\gamma\le s/k$ , and $q^*(\theta)=\theta/(2k)$ if $\gamma\ge s/k$ .
Necessity of (11)–(12) (p. 17). If $(q^O_H,q^O_L)$ is a separating equilibrium under any beliefs, then

\mu(q^*(\theta_H),\theta_H,\theta_H)\ge\mu(q^*(\theta_L),\theta_H,\theta_L)\quad\text{and}\quad\mu(q^*(\theta_L),\theta_L,\theta_L)\ge\mu(q^*(\theta_H),\theta_L,\theta_H).

$\gamma\le s/k$ (p. 28). $\mathrm{IC}'_H\iff\theta_H/\theta_L\ge\Lambda_{H1}$ , and $\mathrm{IC}'_L\iff\theta_H/\theta_L\ge\Lambda_L$ .
$\gamma\ge s/k$ (p. 28). $\mathrm{IC}'_H\iff\theta_H/\theta_L\ge\Lambda_{H2}$ , and $\mathrm{IC}'_L$ holds strictly.
$\Lambda_{H1}\le\Lambda_{H2}\iff\gamma\le s/k$ (p. 28).

Significance

Proposition 3 locates the boundary of truthful self-design. Above $\Lambda$ , a buyer who designs its own product can both reveal its type and obtain its full-information design. The seller then learns preferences without distorting quality. Below $\Lambda$ , the companion mission shows that no separating equilibrium exists at all. The paper builds on this threshold. Proposition 7 compares $\Lambda$ with the A-Learning threshold $\Delta$ to decide which learning mode supports customization over a wider range of preferences. Proposition 8 compares the seller's and buyers' payoffs in the two separating equilibria and shows that the seller prefers to design while the buyers prefer to self-design.

The result is proved in the paper's Appendix. As far as the series' searches show, it has not been machine-checked. This mission poses a formal version of the O-Learning game, its equilibrium notion, and the deviation arguments the paper sketches in a sentence each.

Difficulty

The incentive constraints are polynomial inequalities in the ratio $\theta_H/\theta_L$ once $q^*$ is substituted. The work is elsewhere.

First, the equilibrium quantifies over every request $q\ge 0$ , not only over mimicking the other type. A deviation interacts with the belief the seller holds at that request and with the acceptance rule, and the payoff (9) has two kinks. The proof shows that the two stated off-path beliefs deter every deviation. Each regime needs a different belief: the low-type belief works when the acceptance constraint binds at the first-best, and the high-type belief works when it does not.

Second, the "only if" direction has to hold for every belief function. The argument must show that mimicking the other type's first-best request is always accepted, whatever the seller believes elsewhere.

Third, the paper's proof writes the payoffs without the $\max\{\cdot,0\}$ terms. Those identities hold only on part of the domain, and the formal argument has to track where.

Formalization scope

The O-Learning objects live in the namespace CustomerVoice.OLearn, in a single definition file. The model is a structure with real fields $\theta_H,\theta_L,\alpha,\gamma,k,s$ . Buyer types use the shared CustomerVoice.ALearn.BType, an inductive type with constructors H and L. The standing assumptions $\theta_H>\theta_L>0$ , $\alpha,\gamma\in(0,1)$ and $k,s>0$ are a hypothesis of every theorem. $\alpha$ does not enter this mission but is kept as printed. No other hypothesis is added.

Commitments of the formalization:

Qualities, requests and deviations are real numbers $q\ge 0$ .
The payoff $\mu$ keeps both $\max\{\cdot,0\}$ terms.
The seller accepts at indifference, as the paper prints its acceptance rule.
A rejected request pays $0$ .
A belief function is any total map from requests to the two types. It is pinned only on the equilibrium path.
The price stage is in reduced form, entering only through (9) and the acceptance inequality.
Optimality in (10) is stated as attainment of the maximum (IsMaxOn on the acceptable interval) together with uniqueness.

Ruled-out trivializations. Acceptance is the printed inequality, not the threshold $q\le\gamma\hat\theta/(s+\gamma k)$ , which is milestone 1. The requests are $q^*(\theta)$ , and milestone 2 proves that $q^*(\theta)$ solves (10). The equilibrium is a perfect Bayesian equilibrium against all deviations, not the conjunction of (11) and (12). The "only if" direction quantifies over all belief functions. $\Lambda$ is the printed expression, not an infimum of ratios at which an equilibrium exists.

The development needs only elementary real algebra and one-variable concave quadratics from Mathlib. The equilibrium definition is a template for the other O-Learning mission of the series. Proofs of any milestone, and alternative arguments for the deviation step, are welcome.

The source is the SSRN author version (SSRN 3994319, version of 2023-11-29). All page and display numbers refer to it, and the proofs behind the milestones are in its Appendix.

Selected references

Liang Guo, The Voice of Customers in Customization, SSRN working paper 3994319, version of 2023-11-29. https://ssrn.com/abstract=3994319
Liang Guo, The Voice of Customers in Customization, Management Science. https://doi.org/10.1287/mnsc.2021.04025
Vincent P. Crawford and Joel Sobel, Strategic Information Transmission, Econometrica 50(6), 1982. https://doi.org/10.2307/1913390

10 thms2 active usersReviewed

Economics Operations Research Probability·Captain: mikedeng1

Information Design for Congested Social Services: Optimal Need-Based Persuasion 3: Information Design Pareto-Dominates Full Information Exactly When Low-Need Arrivals Exceed a ThresholdResearch Paper

Motivation

Public and nonprofit services such as food banks, shelters, free clinics and legal aid often run with too little capacity and serve two kinds of users: people with no alternative, and people who have a reasonable outside option. When the queue is long, a user who has an alternative but joins anyway imposes waiting costs on everyone behind them, including the users who cannot go elsewhere. Pricing is usually ruled out in such settings, which leaves the provider one lever: what it tells arriving users about congestion.

Anunrojwong, Iyer and Manshadi (arXiv:2005.07253v3; Management Science, 2023) study this lever as a Bayesian persuasion problem in a queue, building on the revenue-maximization model of Lingenbrink and Iyer (Operations Research 67(5):1397–1416, 2019). The natural benchmark is full information: announce the queue length and let users decide. This mission formalizes the paper's answer to when full information can be improved for both user types at once, and by how much.

Setting

A single server serves users first come, first served, with exponential service times of rate $1$ . High-need users (type H) arrive as a Poisson stream of rate $\lambda_H\ge0$ and always join. Low-need users (type L) arrive at rate $\lambda_L>0$ and either join or take an outside option worth $0$ . Write $\lambda=\lambda_L+\lambda_H\le1$ . A type- $i$ user who joins with $n$ users already present receives utility $u_i(n)$ . The standing assumptions are $u_i(0)>0$ , $u_i(k)<0$ for some $k$ , each $u_i$ strictly decreasing, and the increments $u_L(n)-u_L(n+1)$ non-increasing (Assumption 1).

By a revelation-principle argument (Lemma 1 of the paper, from Lingenbrink and Iyer), a recommendation mechanism that users obey is described by the queue's stationary distribution $\pi=(\pi_n)_{n\ge0}$ . An admission policy is a distribution with $\lambda_H\pi_n\le\pi_{n+1}\le\lambda\pi_n$ for all $n$ ; their set is $\Pi_{AP}$ . A signaling mechanism is an admission policy that also satisfies the obedience constraints

J(\pi)=\sum_{n\ge0}(\pi_{n+1}-\lambda_H\pi_n)u_L(n)\ge0,\qquad L(\pi)=\sum_{n\ge0}(\lambda\pi_n-\pi_{n+1})u_L(n)\le0,

called (JOIN) and (LEAVE); their set is $\Pi_{SM}$ . The welfare of the two types is $W_L(\pi)=J(\pi)$ and $W_H(\pi)=\lambda_H\sum_n\pi_nu_H(n)$ . A policy $\hat\pi$ Pareto-dominates $\pi$ if it is at least as good for both types and strictly better for one; $\pi$ is Pareto-efficient within a class if no member of the class dominates it.

A threshold policy $\pi_x$ , $x=m+a\ge0$ , admits L users when fewer than $m$ users are present, admits them with probability $a$ at $m$ , and turns them away above $m$ . Write $W_L(x)$ , $W_H(x)$ and $L(x)$ for its welfare and (LEAVE) value. The full-information threshold $m_{fi}$ is the smallest $k$ with $u_L(k)<0$ , and the full-information mechanism is $\mathsf{fi}=\pi_{m_{fi}}$ .

Formalization targets

Goal: Proposition 3(1)–(2)

For $\lambda_H\in(0,1)$ , with $u_L,u_H$ fixed, there is a threshold $\bar\Lambda_L(\lambda_H)\in(0,1-\lambda_H]$ such that some signaling mechanism Pareto-dominates $\mathsf{fi}$ if and only if $\lambda_L\ge\bar\Lambda_L(\lambda_H)$ , and

\bar\Lambda_L(\lambda_H)\ \ge\ (1-\lambda_H)\,\frac{u_L(m_{fi}-1)}{u_L(0)-\sum_{k=1}^{m_{fi}-1}\lambda_H^k\big(u_L(k-1)-u_L(k)\big)}\ >\ 0 .

If moreover $\lambda<1$ , $u_L(m_{fi}-1)\le W_L(\mathsf{fi})$ , $u_H(m_{fi})\le W_H(\mathsf{fi})$ , $L(m_{fi}-1)\le0$ and $W_H(\mathsf{fi})>0$ , then a signaling mechanism $\mathsf{sm}$ exists with

W_L(\mathsf{sm})\ge\beta_{L,sm}W_L(\mathsf{fi}),\qquad W_H(\mathsf{sm})\ge\beta_{H,sm}W_H(\mathsf{fi}),

where $\beta_{L,sm}=1+\frac{\lambda_H(1-\lambda)\lambda_L\lambda^{m_{fi}-1}}{1-\lambda_H-\lambda_L\lambda^{m_{fi}-1}}>1$ and $\beta_{H,sm}=1+\frac{(1-\lambda_H)(1-\lambda)\lambda_L\lambda^{m_{fi}-1}}{1-\lambda_H-\lambda_L\lambda^{m_{fi}-1}}>1$ .

Milestones

Lemma 3: the geometric sandwich $\lambda_H^{k-q}\pi_q\le\pi_k\le\lambda^{k-q}\pi_q$ on $\Pi_{AP}$ .
Theorems 1 and 2: Pareto-efficient signaling mechanisms and admission policies have a threshold structure with threshold at most $m_{fi}$ .
Lemma 2: maximizers of $\theta W_L+(1-\theta)W_H$ exist.
Theorem 3: when (LEAVE) is slack, efficiency within $\Pi_{SM}$ and within $\Pi_{AP}$ coincide.
Lemma 5(1)–(2): $W_H(x)$ is strictly decreasing, and $W_L(x)$ is unimodal and monotone between consecutive integers.
$\mathsf{fi}\in\Pi_{SM}$ with $L(\mathsf{fi})<0$ .
Theorem 4: exactly one of " $\mathsf{fi}$ is Pareto-efficient among admission policies" and "a signaling mechanism dominates $\mathsf{fi}$ " holds, the first if and only if $W_L(m_{fi})>W_L(m_{fi}-1)$ .
From the proof of Proposition 3: the equivalence of that condition with $f(\lambda_L,\lambda_H)<0$ , an identity for $W_L(m-1)$ and an inequality for $W_H(m-1)$ , for $1\le m\le m_{fi}$ .

Significance

The proposition gives a clean regime split. Full information is already Pareto-efficient when low-need demand is light. Once $\lambda_L$ crosses an explicit level, revealing everything leaves welfare on the table for both types, so a provider who cares about either group has a reason to hide some queue information. The lower bound on $\bar\Lambda_L$ is explicit in the primitives, and the factors $\beta_{L,sm},\beta_{H,sm}$ give a guaranteed improvement, not only an existence statement. Theorem 4, the milestone behind part 1, reduces the comparison to two adjacent thresholds.

The paper proves these results on paper. To our knowledge none of them has a machine-checked proof. A formal development checks the "little algebra" steps that the paper compresses (the equivalence with $f<0$ , the welfare identities of p. 41–42). It also produces a reusable layer for persuasion in birth–death queues: obedient mechanisms as distributions, threshold policies, and Pareto efficiency within a class. The companion missions of this series (threshold structure, the homogeneous case, first-best) are stated over the same layer.

Difficulty

The threshold $\bar\Lambda_L$ comes from analysing the sign of $f(\cdot,\lambda_H)$ on $(0,1-\lambda_H]$ . Translating "fi is not dominated" into that sign condition is where the work lies. The obvious attempt, comparing $\mathsf{fi}$ only with nearby threshold policies, settles one direction: if $W_L(m_{fi}-1)\ge W_L(m_{fi})$ , the threshold $m_{fi}-1$ dominates. The converse needs every competitor in $\Pi_{AP}$ , not just threshold policies. That requires the structure theorem for efficient admission policies, the existence of maximizers, and unimodality of $W_L$ , followed by a transfer from $\Pi_{AP}$ to $\Pi_{SM}$ that only works because (LEAVE) is slack at $\mathsf{fi}$ . The welfare series are infinite, and the threshold family is parametrised by a real $x$ whose fractional part enters nonlinearly, so the comparisons are not finite-dimensional linear algebra.

Formalization scope

Everything is stated over a structure Model with real fields $\lambda_L,\lambda_H$ and utilities $u_L,u_H:\mathbb N\to\mathbb R$ , with a predicate Standing holding the standing assumptions ( $\lim_ku_i(k)<0$ is encoded as $\exists k,\ u_i(k)<0$ ). Queue lengths are natural numbers, and the two types are separate fields. Membership in $\Pi_{AP}$ includes summability of $\pi_nu_L(n)$ and $\pi_nu_H(n)$ : the paper treats all welfare as finite, and an unrestricted tsum would assign $0$ to divergent welfare. $W_L$ is the right-hand form of (2), with no division by $\lambda_L\pi_n$ . A finite threshold requires $\pi\in\Pi_{AP}$ , $\pi_m>0$ and a joining fraction in $[0,1]$ , as in Definition 2. Threshold policies are defined from their unnormalised weights, $\mathsf{fi}$ is $\pi_{m_{fi}}$ as a distribution, and Pareto efficiency is Definition 1 within an explicit class. "Exactly one" is exclusive or.

Added hypotheses, each disclosed in the item that carries it:

Convergence of $\sum_n\lambda_H^nu_H(n)$ . This is the finite-welfare convention, equivalent to $\Pi_{AP}\ne\emptyset$ when $\lambda_H>0$ .
Lemma 2's hypothesis ( $\lambda<1$ , or $u_L,u_H\to-\infty$ ) wherever existence of maximizers is used.
$u_L(m_{fi}-1)\ne0$ in Proposition 3. Without it the claimed $\bar\Lambda_L>0$ is false.
$\lambda_H>0$ in Lemma 5(1) and Theorem 4, as required by §4.2's heterogeneous setting. For $\lambda_H=0$ , $W_H\equiv0$ , and Theorem 4's strict adjacent-threshold comparison can fail at a tie.

The page's range $\lambda_L\in[\bar\Lambda_L,1)$ is intersected with $\lambda\le1$ . In part 2, " $\mathsf{sm}$ " is read existentially.

Ruled out as trivializing: choosing $\bar\Lambda_L$ after $\lambda_L$ (the goal quantifies it once, with $\lambda_H,u_L,u_H$ fixed); defining $\mathsf{fi}$ through its welfare; replacing Pareto efficiency by maximization of a weighted welfare; replacing exclusive or by inclusive or; and any constant that differs from the page's $\beta_{L,sm}$ , $\beta_{H,sm}$ or lower bound symbol for symbol.

A complete development needs geometric and arithmetico-geometric series, rearrangement of infinite sums over $\mathbb N$ , and convexity arguments in the space of summable sequences. Proofs of any milestone are welcome, as are lemmas about threshold policies that the other missions of the series can reuse.

Selected references

J. Anunrojwong, K. Iyer, V. Manshadi, Information Design for Congested Social Services: Optimal Need-Based Persuasion, Management Science, 2023; read as arXiv:2005.07253v3 (2022). https://arxiv.org/abs/2005.07253
D. Lingenbrink, K. Iyer, Optimal Signaling Mechanisms in Unobservable Queues, Operations Research 67(5):1397–1416, 2019.
E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590
D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 5th ed., Wiley, 2018.

15 thms2 active usersReviewed

Completed

Economics Mechanism Design Operations Research·Captain: mikedeng1

The Voice of Customers in Customization I: Under A-Learning, Truthful Cheap-Talk Communication Is an Equilibrium If and Only If θH/θL ≥ ΔResearch Paper

Motivation

Sellers often ask customers what they want before designing a product or service. The answer can affect both the quality delivered and the price paid. Because a customer can send a costless, unverifiable message, the seller cannot assume that a stated preference is true. Guo's customization model asks when the customer's own incentives make truthful communication sustainable. This matters for products with substantial presale effort, such as prototypes, proposals, and sales assistance: the seller incurs that effort before the final transaction price is set. The paper distinguishes this selling cost from the cost of producing the eventual product. This mission concerns the paper's A-Learning game, in which the seller learns through a customer's message before choosing quality.

Setting

Each buyer wants one unit of a product with quality $q\geq0$ . A buyer with preference $\theta$ values it at $\theta q$ and can decline to trade. The preference is private and has two possible values, $\theta_H>\theta_L>0$ . The high type has prior share $\alpha\in(0,1)$ . Producing quality $q$ costs $kq^2$ and selling it costs $sq^2$ , with $k,s>0$ . The selling cost is incurred at the design stage. In the final price-setting stage, the seller makes a take-it-or-leave-it offer with probability $\gamma\in(0,1)$ ; the buyer makes the offer with probability $1-\gamma$ . These are the assumptions of §2, pp. 5–9.

Under A-Learning, the buyer sends one of two costless messages before the seller chooses quality. A separating message rule sends different messages for the high and low types. On receiving message $m$ , the seller believes the type is $\hat\theta(m)\in\{\theta_H,\theta_L\}$ . If its belief is $\hat\theta$ , the seller's expected payoff from offering quality $q$ is

v(q,\hat\theta)=\gamma(\hat\theta q-kq^2)-sq^2.

At a given quality, a buyer whose actual type is $\theta$ receives

u_A(\theta,\hat\theta,q)=\gamma\max\{\theta q-\hat\theta q,0\}+(1-\gamma)\max\{\theta q-kq^2,0\}.

The maxima preserve the buyer's option not to purchase. In the paper's perfect Bayesian equilibrium, the seller's beliefs agree with the types that send the observed messages, the seller chooses a nonnegative quality maximizing $v$ for each message, and each type chooses a message maximizing its own payoff. With two distinct messages and a separating rule, both messages occur on the equilibrium path. These payoff and equilibrium conditions are stated in §3.2, pp. 11–12, equations (4)–(7).

Formalization targets

The seller's printed optimal design for belief $\hat\theta$ is

q(\hat\theta)=\frac{\gamma\hat\theta}{2s+2\gamma k}.

With $u(\theta,\hat\theta)=u_A(\theta,\hat\theta,q(\hat\theta))$ , the two incentive compatibility conditions are $u(\theta_H,\theta_H)\geq u(\theta_H,\theta_L)$ and $u(\theta_L,\theta_L)\geq u(\theta_L,\theta_H)$ . The supporting targets identify the seller's optimal design, characterize informative equilibrium by these two conditions, and express each condition as a threshold on type heterogeneity. They follow §3.2, pp. 12–13.

The goal is Proposition 1: an informative A-Learning equilibrium exists exactly when

\frac{\theta_H}{\theta_L}\geq\Delta:=\max\left\{\Delta_H,\Delta_L\right\},\qquad \Delta_H=\frac{\gamma[2s+(1+\gamma)k]}{(1-\gamma)(2s+\gamma k)},\qquad \Delta_L=\frac{2s+\gamma k}{\gamma k}.

The weak inequality includes the boundary at which a buyer is indifferent between messages. The Appendix's proof uses strict inequalities in a corresponding line; the statement on p. 13 and Proposition 1 use weak ones. The milestone list retains the source's optimal-design sentence, equations (6)–(7), and the two threshold sentences in their order in the SSRN author copy.

Significance

The theorem gives a precise answer to whether costless buyer communication can transmit preference information before a seller customizes a product. The condition separates the two possible failures of truthful reporting: a high type may prefer the design induced by the low message, and a low type may prefer the design induced by the high message. It also shows why the relevant threshold depends on bargaining power and both cost coefficients, while the prior share $\alpha$ does not enter this particular equilibrium-existence condition. The result is a theorem of the paper; the mission seeks its machine-checked formulation and proof.

The formal development makes the equilibrium claim more than a comparison of two algebraic payoffs. It must connect an actual separating message strategy, beliefs, a seller optimum, and buyer best responses to the two incentive conditions. The model's payoff definitions and equilibrium predicate are reusable for other statements about A-Learning in the paper, including comparisons of equilibrium quality and payoffs. The threshold lemmas can also be reused when comparing A-Learning with O-Learning.

Difficulty

Costless messages alone impose no truthful-reporting discipline. A seller's belief changes both the design chosen after a message and the price a buyer might face. The high and low types therefore face different deviation incentives. A comparison that ignores the seller's design decision misses the equilibrium requirement; a comparison that treats every buyer as purchasing misses the low type's option to refuse an overpriced high-quality product. The second issue is visible in the $\max\{\cdot,0\}$ terms of equation (5). The equilibrium result has to hold at equality in the thresholds as well as above them.

Formalization scope

The Lean model uses real parameters $\theta_H,\theta_L,\alpha,\gamma,k,s$ and a two-constructor type for buyer types. Its standing assumptions are exactly $\theta_H>\theta_L>0$ , $0<\alpha<1$ , $0<\gamma<1$ , $k>0$ , and $s>0$ . A separate two-constructor type represents the two possible messages. Quality is real and every seller optimization ranges over $q\geq0$ ; optimality means that the chosen design attains the maximum. Buyer deviations range over both messages. Beliefs identify the types on the equilibrium path. The type's purchase option is kept in both maximum terms of the buyer payoff.

The price-setting stage is represented by the paper's reduced-form payoffs (4) and (5), without a separate bargaining game. The prior share $\alpha$ is retained among the standing primitives even though it cancels from Proposition 1. The closed-form design is used in $u(\theta,\hat\theta)$ and the incentive conditions, while an equilibrium requires actual seller maximization. An equilibrium is not defined as the conjunction of incentive conditions, and $\Delta$ is the printed maximum of the two explicit fractions. Separation rules out a one-message or pooling interpretation. The supporting statements require real arithmetic, optimization on a nonnegative domain, and finite case analysis for the two types and two messages. Contributions that preserve these definitions and the paper's weak boundary are welcome. The known proofs behind the milestones are in the Appendix of the SSRN version, pp. 27–28.

Selected references

Liang Guo, The Voice of Customers in Customization, SSRN working paper 3994319, author-copy version of 2023-11-29. SSRN abstract and paper. Published as a Management Science article, DOI 10.1287/mnsc.2021.04025.

6 thms2 active usersReviewed

Economics Operations Research·Captain: mikedeng1

Softening Competition Through Unilateral Sharing of Customer Data: For Every Monotone-Hazard-Rate Distribution, Sharing Data on [z^N, b′] Makes Both Firms Strictly Better OffResearch Paper

Why a firm would hand customer data to a rival

Large platforms that also sell their own products (Amazon, JD.com, app stores) hold detailed data on consumers and sometimes share part of it with the independent sellers they compete with. The usual view in the personalized-pricing literature is that information is a competitive weapon: a firm that knows more about consumers can price discriminate and capture more surplus, so giving that knowledge to a rival should only hurt. Thisse and Vives (American Economic Review, 1988) showed that when both firms on a Hotelling line can price every consumer individually, competition intensifies and the profits of the informed firm fall.

Choe, Cong and Wang (Monash Discussion Paper 2021-10, revised October 20, 2022; published in Management Science, 2024, doi:10.1287/mnsc.2023.4689) show that this is not the whole picture: an informed firm can strictly gain by sharing data on a well-chosen segment of consumers with an uninformed rival, and the rival gains too. This mission formalizes that result, Proposition 1 of the paper, together with the steps its proof is built from.

Setting

Consumers are located on the interval $[0,1]$ . A consumer's location has cumulative distribution function $F$ with density $f>0$ , continuous on $[0,1]$ , and the hazard rate

h(x)=\frac{f(x)}{1-F(x)}

is strictly increasing on $[0,1)$ (the monotone hazard rate condition). Firm 1 sits at $0$ and knows every consumer's location; firm 2 sits at $1$ and knows none. A consumer at $x$ who buys from firm $i$ at price $p_i$ pays $p_i$ plus a transport cost equal to her distance to firm $i$ ; production is costless and the market is fully covered.

Benchmark. Without data sharing, firm 2 sets one uniform price $p_2$ and firm 1 undercuts it consumer by consumer, so firm 2 serves $[z,1]$ with $p_2=2z-1$ and earns $(2z-1)(1-F(z))$ . The first-order condition gives the benchmark marginal consumer $z^N$ and price $p^N_2$ :

z^N=\frac12+\frac1{h(z^N)},\qquad p^N_2=\frac2{h(z^N)}=2z^N-1.

The benchmark profits are $\pi^N_1=\int_0^{z^N}(p^N_2+1-2x)\,dF(x)$ and $\pi^N_2=p^N_2(1-F(z^N))$ .

Data sharing on $[a,b]$ . Firm 1 gives firm 2 the locations of the consumers in $[a,b]$ . Firm 2 then chooses a uniform price for the consumers it does not know and personalized prices on $[a,b]$ . Its uniform price either serves only $[b,1]$ , at price $2b-1$ and profit $\pi_{21}(b)=(2b-1)(1-F(b))$ , or serves $[z',a]\cup[b,1]$ for some $z'\le a$ , with best profit

\pi_{22}(a,b)=\max_{z'\in[0,a]}(2z'-1)\bigl(1-F(b)+F(a)-F(z')\bigr).

When firm 2 chooses the first option, the profits are

\pi_1(a,b)=\int_0^a\bigl((2b-1)+(1-2x)\bigr)\,dF(x),\qquad \pi_2(a,b)=\int_a^b(2x-1)\,dF(x)+\pi_{21}(b).

Firm 2's incentive constraint (IC) is $\pi_{21}(b)\ge\pi_{22}(a,b)$ .

Formalization targets

Goal: Proposition 1

For every distribution $(F,f)$ satisfying the conditions above:

\pi_1(z^N,b)>\pi^N_1\quad\text{and}\quad\pi_2(z^N,b)>\pi^N_2\qquad\text{for all } b\in(z^N,1],

and there exists $b'\in(z^N,1)$ with

\pi_{21}(b')>\pi_{22}(z^N,b'),

so sharing data on $[z^N,b']$ satisfies firm 2's incentive constraint and makes both firms strictly better off than without sharing.

Milestones

Eq. (1): $z^N$ exists and is unique in $(1/2,1)$ .
$z^N$ is the unique maximizer of $\pi_{21}$ on $[0,1]$ .
Lemma 2: if firm 2's uniform price serves $[z',a]\cup[b,1]$ with $z'$ solving the first-order condition (5), then $z'<z^N$ , firm 2's price falls below $p^N_2$ , and firm 1 earns less than $\pi^N_1$ .
$\pi_1(z^N,b)-\pi^N_1=2(b-z^N)F(z^N)$ .
$\pi_2(z^N,b)-\pi^N_2>\int_b^1(2b-2z^N)\,dF(x)>0$ for $z^N<b<1$ .
With $\hat\pi_{22}(b)=\pi_{22}(z^N,b)$ : $\pi_{21}(z^N)=\hat\pi_{22}(z^N)$ and $\pi_{21}(1)<\hat\pi_{22}(1)$ .
$\hat\pi_{22}(b)<\hat\pi_{22}(z^N)$ for every $b\in(z^N,1]$ .

Significance

The result reverses the standard intuition that a firm's informational advantage should be guarded. Firm 1 shares data only on firm 2's own customer base $[z^N,b']$ , which it could not win anyway, and keeps the data on the most loyal consumers $[b',1]$ private. Firm 2 then prefers to extract surplus from those loyal consumers with a high uniform price $2b'-1>p^N_2$ , and firm 1 raises its personalized prices accordingly. Competition is softened without firm 1 conceding market share. The statement holds for every monotone-hazard-rate distribution, not for a parametric family, which is what makes it a structural claim rather than a numerical example. It underlies the paper's analysis of optimal data sharing (Section 3.3) and its welfare conclusion that consumer surplus falls (Proposition 3), and it is the benchmark against which the paper's extensions (sales fees, data sale, entry) are compared.

The paper's proof is complete for the first part. For the existence of $b'$ , the written argument infers a negative derivative of $\hat\pi_{22}$ at $z^N$ from a strict inequality, which does not follow as written and presupposes differentiability of a maximum value function; the statement itself is true. A machine-checked proof closes that step. To the best of current knowledge none of these results has been formalized.

Difficulty

The two profit comparisons in the first part are integral identities and estimates that only need the fundamental theorem of calculus and $f>0$ . The existence of $b'$ is the hard part. Both $\pi_{21}(b)$ and $\hat\pi_{22}(b)$ start from the same value at $b=z^N$ , and $\pi_{21}$ has zero derivative there, so the comparison is decided at first order by how fast $\hat\pi_{22}$ decreases. But $\hat\pi_{22}$ is a maximum over $z'\in[0,z^N]$ whose maximizer moves with $b$ and need not be unique, so $\hat\pi_{22}$ is not known to be differentiable, and the strict decrease of milestone 7 alone does not give a linear rate. A proof has to bound $\hat\pi_{22}(b)$ from above by $\pi_{21}(z^N)$ minus a term proportional to $b-z^N$ , uniformly over the possible maximizers, and compare it with the second-order behaviour of $\pi_{21}$ near its maximum. Existence of $z^N$ similarly needs the hazard rate to blow up at $1$ , which uses $F(1)=1$ and $f(1)>0$ .

Formalization scope

All objects are real-valued functions on $\mathbb R$ with hypotheses only on $[0,1]$ . The distribution is the structure MHRDist F f: $F(0)=0$ , $F(1)=1$ , $F$ has derivative $f$ within $[0,1]$ at every point of $[0,1]$ , $f$ is continuous and strictly positive on $[0,1]$ , and $h=f/(1-F)$ is strictly increasing on $[0,1)$ . The paper's "smooth" is read as continuously differentiable, a weaker assumption, so the formal theorems are at least as strong as the paper's. Every $dF$ integral is an interval integral of the integrand times $f$ , always with increasing bounds. $z^N$ enters as a number zN with the hypothesis IsZN F f zN ( $z^N\in(1/2,1)$ and $z^N=1/2+1/h(z^N)$ ); milestone 1 shows exactly one such number exists, so no statement is vacuous. $\pi_{22}$ is defined as the supremum of the profit over $z'\in[0,a]$ (a maximum, since the set is compact and the function continuous), never through the first-order condition (5); the incentive inequality in the goal is strict, as in the paper's proof.

A trivializing formalization is ruled out: $\pi_{22}$ is the actual maximum, not a free parameter or the value at a stationary point, and $z^N$ is pinned by Eq. (1), whose solution is shown to exist.

A complete development needs the fundamental theorem of calculus for interval integrals, compactness and the intermediate value theorem on $[0,1]$ , and a uniform first-order estimate on a parametric maximum. The lemmas on hazard rates and on the maximizer of $(2z-1)(1-F(z))$ are reusable for other Hotelling and pricing models with monotone-hazard-rate demand. Contributions are welcome on any milestone, and alternative proofs of the existence of $b'$ are of particular interest.

Selected references

Chongwoo Choe, Jiajia Cong, Chengsi Wang, Softening Competition through Unilateral Sharing of Customer Data, Monash University Department of Economics Discussion Paper 2021-10, revised October 20, 2022 (the version formalized here; all page and equation numbers refer to it); published in Management Science, 2024. https://doi.org/10.1287/mnsc.2023.4689
Jacques-François Thisse, Xavier Vives, On the Strategic Choice of Spatial Price Policy, American Economic Review 78(1), 1988, 127–137.
Greg Shaffer, Z. John Zhang, Competitive One-to-One Promotions, Management Science 48(9), 2002, 1143–1160.

10 thms2 active usersReviewed

Economics Operations Research·Captain: mikedeng1

The Voice of Customers in Customization IV: The A-Learning Threshold Δ Exceeds the O-Learning Threshold Λ If and Only If γ < max{2s/(2s+k), (√(s²+4sk) − s)/(2k)}Research Paper

Motivation

A seller who customizes products for buyers must learn what each buyer wants, and buyers have private information about how much they value quality. Liang Guo's paper The Voice of Customers in Customization (Management Science, doi:10.1287/mnsc.2021.04025; author copy SSRN 3994319) compares two ways of learning those preferences. Under A-Learning ("asking") the buyer sends an unverifiable, costless message about its type and the seller then designs the product. Under O-Learning ("observing") the buyer itself proposes the quality it wants, and the seller accepts or rejects the proposal. In both, the price is set afterwards by bargaining in which the seller makes the take-it-or-leave-it offer with probability $\gamma$ .

Customization works only if buyer types are revealed in equilibrium. The paper shows that each approach admits a separating equilibrium exactly when the buyers are heterogeneous enough: the ratio $\theta_H/\theta_L$ of the two types' quality preferences must exceed a critical value, $\Delta$ under A-Learning (Proposition 1) and $\Lambda$ under O-Learning (Proposition 3). Which approach makes customization easier to sustain is then a comparison of two explicit numbers. Proposition 7 answers it, and its answer depends only on the seller's bargaining power and the two cost coefficients. This is the question a manager choosing between surveys and interviews (asking) and design-it-yourself tools (observing) faces in the model.

Setting

A model is a tuple of real numbers $(\theta_H,\theta_L,\alpha,\gamma,k,s)$ :

$\theta_H$ and $\theta_L$ are the quality preferences of the high and the low buyer type; a buyer of type $\theta$ buying quality $q\ge0$ at price $p$ gets $\theta q-p$ ;
$\alpha$ is the prior share of high-type buyers;
$\gamma$ is the seller's bargaining power, the probability that the seller (rather than the buyer) makes the take-it-or-leave-it price offer;
$k$ is the production-cost coefficient (a product of quality $q$ costs $kq^2$ ) and $s$ is the selling-cost coefficient (selling it costs $sq^2$ ).

The paper's standing assumptions (§2, pp. 5–6) are

\theta_H>\theta_L>0,\qquad \alpha\in(0,1),\qquad \gamma\in(0,1),\qquad k>0,\qquad s>0 .

The A-Learning thresholds (Proposition 1, p. 12, and p. 13) are

\Delta_H=\frac{\gamma[2s+(1+\gamma)k]}{(1-\gamma)(2s+\gamma k)},\qquad \Delta_L=\frac{2s+\gamma k}{\gamma k},\qquad \Delta=\max\{\Delta_H,\Delta_L\}.

$\Delta_H$ is the ratio above which the high type does not gain by claiming to be low, and $\Delta_L$ the ratio above which the low type does not gain by claiming to be high.

The O-Learning thresholds (Proposition 3, p. 17) are

\Lambda_{H1}=\frac{\gamma(s+k)}{(1-\gamma)s},\qquad \Lambda_{H2}=\frac{1+\gamma}{1-\gamma},\qquad \Lambda_L=\frac{s}{\gamma k},\qquad \Lambda=\max\{\min\{\Lambda_{H1},\Lambda_{H2}\},\Lambda_L\}.

$\Lambda_{H1}$ and $\Lambda_{H2}$ are the high type's thresholds in the two regimes $\gamma\le s/k$ (seller acceptance binds) and $\gamma\ge s/k$ (it does not); $\Lambda_L$ is the low type's.

Formalization targets

Goal: Proposition 7 (p. 22)

\Delta>\Lambda\quad\Longleftrightarrow\quad\gamma<\max\Big\{\frac{2s}{2s+k},\ \frac{\sqrt{s^2+4sk}-s}{2k}\Big\},

for every model satisfying the standing assumptions. The paper phrases this as "the critical value of $\theta_H/\theta_L$ to sustain the separating equilibrium is larger under the A-Learning customization than under the O-Learning customization (i.e., $\Delta>\Lambda$ )"; the parenthetical fixes the statement as a comparison of the two printed thresholds.

Milestones (Appendix, Proof of Proposition 7, p. 29)

$\Delta_H<\Lambda_{H1}$ ;
$\Delta_H<\Lambda_{H2}$ ;
$\Delta_L>\Lambda_L$ ;
$\Delta>\Lambda\iff\Delta_L>\min\{\Lambda_{H1},\Lambda_{H2}\}$ .

Significance

The result. Proposition 7 says that neither learning approach dominates the other. When the seller's bargaining power is low, A-Learning requires more heterogeneous buyers than O-Learning, so empowering buyers to design their own products sustains customization over a larger range of markets; when the seller is powerful, the order reverses. Milestones 1–3 carry the paper's economic reading: the low type's incentive to reveal itself is weaker under A-Learning ( $\Delta_L>\Lambda_L$ ), the high type's is stronger ( $\Delta_H<\min\{\Lambda_{H1},\Lambda_{H2}\}$ ), and the comparison is decided by which effect dominates. The cutoff on $\gamma$ is explicit in $s$ and $k$ , which is what makes the comparison usable for comparative statics.

Formalizing it. The result is proved in the paper, in a short Appendix argument (p. 29); it has not been machine-checked. A formal proof pins down that the reduction is correct for every parameter value allowed by the standing assumptions, including the boundary cases $\gamma=s/k$ (where $\Lambda_{H1}=\Lambda_{H2}$ ) and the case where the two candidate cutoffs coincide. Together with the companion missions of this series, which formalize Propositions 1 and 3 as statements about the equilibria of the two games, it gives a fully checked version of the paper's comparison of the two approaches.

Difficulty

Both critical values are nested maxima and minima of rational functions of $(\gamma,k,s)$ , and which term attains each maximum or minimum changes across the parameter space, in particular at $\gamma=s/k$ , where $\Lambda_{H1}$ and $\Lambda_{H2}$ exchange order. A direct case split on the attaining terms therefore produces many cases, several of which turn on sign conditions that hold only under the standing assumptions. The cutoff on the right-hand side is a maximum of two expressions of different kinds, one rational and one involving $\sqrt{s^2+4sk}$ , and neither of them dominates the other for all $(k,s)$ , so neither can be dropped. Strictness must be tracked throughout, since both sides of the equivalence are strict and the boundary $\Delta=\Lambda$ is attained.

Formalization scope

All objects live in the namespace CustomerVoice.Thresholds. A structure Model holds the six real primitives, Model.Standing is the conjunction of the standing assumptions, and Model.DeltaH, DeltaL, Delta, LambdaH1, LambdaH2, LambdaL, Lambda are the printed closed-form expressions, with $\max$ and $\min$ on $\mathbb R$ and the square root as Real.sqrt. Every theorem takes a model and the hypothesis M.Standing; no other hypothesis is added. Only $\gamma$ , $k$ and $s$ enter the thresholds; $\theta_H$ , $\theta_L$ and $\alpha$ are carried so that the model is the paper's. Under the standing assumptions all denominators are positive, so Lean's convention $x/0=0$ is never used.

The thresholds are defined as the paper prints them. Defining $\Delta$ or $\Lambda$ as the least type ratio at which an equilibrium exists, replacing them by simplified forms that hold only in a regime (for instance $\Lambda=\Lambda_{H2}$ when $\gamma\ge s/k$ ), replacing the right-hand side of Proposition 7 by an equivalent condition the paper does not print, or proving only one direction of the equivalence, would each be a different statement and is ruled out.

The two games and the equilibrium characterizations behind $\Delta$ and $\Lambda$ (Propositions 1 and 3) are not part of this mission; they are the goals of missions I and II of this series, and the model is defined again here because draft missions cannot import each other. No library beyond Mathlib's ordered-field and square-root API is needed. Contributions welcome: proofs of the four milestones and the goal, and helper lemmas solving the two quadratic inequalities $\Delta_L>\Lambda_{H1}$ and $\Delta_L>\Lambda_{H2}$ in $\gamma$ .

The source is the SSRN author copy of the paper (version of 2023-11-29); all page numbers are its printed pages, and the proof the milestones come from is in its Appendix.

Selected references

Liang Guo, The Voice of Customers in Customization, Management Science. doi:10.1287/mnsc.2021.04025. Author copy: SSRN working paper 3994319, version of 2023-11-29, ssrn.com/abstract=3994319.
Vincent P. Crawford and Joel Sobel, Strategic Information Transmission, Econometrica 50(6), 1982. doi:10.2307/1913390.

6 thms2 active usersReviewed

Analysis Operations Research Optimization·Captain: mikedeng1

A Sensitivity Analysis of the Price of Anarchy in Nonatomic Congestion Games 3: The Price of Anarchy Is Locally Lipschitz at Games with Constant Costs or Strictly Increasing C¹ CostsResearch Paper

Motivation

The price of anarchy (PoA) of a nonatomic congestion game is the ratio of the total cost of a Wardrop equilibrium to the minimum total cost. Worst-case bounds on it over whole classes of cost functions are classical (Roughgarden and Tardos, 2002; Correa, Schulz and Stier-Moses, 2004). In practice the demands and cost functions of a traffic model are estimated, never known exactly, so a second question matters as much as the worst case: how much does the PoA of a given game move when its data move?

Wu and Möhring (arXiv:2007.13979v3, published in Mathematics of Operations Research, 2023) answer this with a metric on games that compares demands and cost functions simultaneously. They show that the PoA is continuous, that it is Hölder continuous with exponent $1/2$ near every game whose costs are Lipschitz, and that it is not uniformly Hölder continuous. This mission formalizes their Theorem 12 (§4.3): at two special classes of games, games with constant costs and games with strictly increasing continuously differentiable costs, the exponent improves to $1$ , so the PoA is locally Lipschitz. The authors motivate the result by the differentiability results of Cominetti, Dose and Scarsini (2020), which suggest Lipschitz behaviour at games whose costs have strictly positive derivatives.

Setting

Fix a finite set $A$ of arcs, a finite nonempty set $K$ of origin–destination (O/D) pairs, and for each $k\in K$ a set $S_k$ of at least two paths, each a nonempty set of arcs; every arc lies on some path. A game $\Gamma=(\tau,d)$ consists of arc cost functions $\tau_a$ , continuous, non-decreasing and non-negative on $[0,\infty)$ , and demands $d_k\ge 0$ with total demand $T(d)=\sum_k d_k>0$ ; moreover $\tau_a(x)>0$ for $x\in(0,T(d)]$ . These games form the game space $\mathcal G(G,K,S)$ .

A flow $f=(f_s)_{s\in S}\ge 0$ routes each demand, $\sum_{s\in S_k} f_s=d_k$ . The arc flow is $f_a=\sum_{s\ni a} f_s$ , the path cost $\tau_s(f)=\sum_{a\in s}\tau_a(f_a)$ , and the total cost $C(\Gamma,f)=\sum_a f_a\tau_a(f_a)$ . A flow $\tilde f$ is a Wardrop equilibrium (WE) if every used path of a pair is a cheapest path of that pair. The SO cost $C^*(\Gamma)$ is the minimum total cost, the WE cost $\tilde C(\Gamma)$ is the total cost of a WE flow (all WE flows have the same cost), and the PoA is

\rho(\Gamma)=\frac{\tilde C(\Gamma)}{C^*(\Gamma)}.

The distance of two games $\Gamma=(\tau,d)$ and $\Gamma'=(\sigma,d')$ is

\|\Gamma-\Gamma'\|=\max\Big\{\|d-d'\|_\infty,\ \max_{a\in A}\max_{x\in[0,\min\{T(d),T(d')\}]}|\tau_a(x)-\sigma_a(x)|,\ \|\tau(T(d))-\sigma(T(d'))\|_\infty\Big\},

which compares cost functions only on the range both games use, plus their values at the respective total demands.

Formalization targets

Goal: Theorem 12

Let $\Gamma=(\tau,d)\in\mathcal G(G,K,S)$ .

If every $\tau_a$ is constant on $[0,T(d)]$ , or
if every $\tau_a$ is continuously differentiable on $[0,T(d)]$ with $\tau_a'\ge m_\Gamma>0$ there,

then there are $\epsilon_\Gamma>0$ and $\kappa_\Gamma>0$ such that

|\rho(\Gamma)-\rho(\Gamma')|\le\kappa_\Gamma\cdot\|\Gamma-\Gamma'\|\qquad\text{for all }\Gamma'\in\mathcal G(G,K,S)\text{ with }\|\Gamma-\Gamma'\|<\epsilon_\Gamma.

The goal leaves the constants unspecified; only their existence, depending on $\Gamma$ alone, is asserted.

Milestones

Proof of Theorem 12a), p. 37. A game whose costs are constant on $[0,T(d)]$ has $\rho(\Gamma)=1$ .
(4.33), p. 37. Near such a game, $0\le\rho(\Gamma')-\rho(\Gamma)\le\frac{8\,|A|\,T(d)\,(|K|+1)}{C^*(\Gamma)}\|\Gamma-\Gamma'\|$ .
(4.39), p. 38. For WE flows $\tilde f,\tilde g$ of two games $\Gamma_1=(\pi^1,w)$ , $\Gamma_2=(\pi^2,w)$ with equal demands,

0\le\sum_a(\pi^1_a(\tilde f_a)-\pi^2_a(\tilde g_a))(\tilde g_a-\tilde f_a)\le\sum_a(\pi^1_a(\tilde g_a)-\pi^2_a(\tilde f_a))(\tilde g_a-\tilde f_a)\le 2|A|\,T(w)\,\|\Gamma_1-\Gamma_2\|.

(4.40), p. 38, first four inequalities. If moreover the costs of $\Gamma_1$ are $C^1$ on $[0,T(w)]$ with derivative $\ge m>0$ , then

m\sum_a|\tilde g_a-\tilde f_a|^2\le\sum_a(\pi^1_a(\tilde g_a)-\pi^1_a(\tilde f_a))(\tilde g_a-\tilde f_a)\le\sum_a(\pi^1_a(\tilde g_a)-\pi^2_a(\tilde g_a))(\tilde g_a-\tilde f_a)\le\|\Gamma_1-\Gamma_2\|\sum_a|\tilde g_a-\tilde f_a|.

Significance

At a general game with Lipschitz costs the PoA is only Hölder continuous with exponent $1/2$ in this metric, and the paper shows that no exponent works uniformly over the game space. Theorem 12 identifies two natural classes of games at which the sensitivity is linear: constant costs (the PoA equals $1$ and grows at most linearly under perturbation) and strictly increasing $C^1$ costs, which include affine costs with positive slopes. For these games an estimation error of size $\delta$ in demands and costs changes the PoA by $O(\delta)$ .

The result is proved in the paper; it is not formalized anywhere. A complete development would also provide machine-checked equilibrium-comparison estimates between two games of one demand slice ((4.39)–(4.40)), which are reusable for any stability analysis of Wardrop equilibria. The paper's explicit constants in (4.41)–(4.46) are off by a factor $\sqrt{|A|}$ (the last step of (4.40) uses $\sum_a|x_a|\le\sqrt{\sum_a x_a^2}$ ); the existential Theorem 12 is unaffected, and a formalization with correct explicit constants is a welcome addition.

Difficulty

The PoA is a ratio of two optimal values, and the perturbed game $\Gamma'$ may change the demand vector and the costs at once, including the costs on $(T(d),T(d')]$ , which $\Gamma$ 's hypotheses do not control. A direct comparison of $\Gamma$ and $\Gamma'$ therefore fails: the WE flows live in different feasible sets, and the hypotheses on $\Gamma$ say nothing beyond $T(d)$ . The general Hölder- $1/2$ argument loses a square root exactly where it bounds the distance between the arc flows of the two equilibria through an approximate-equilibrium estimate; obtaining exponent $1$ requires an estimate in which the flow difference enters linearly, and this is where strict monotonicity of the costs is needed. Constant costs are degenerate in the opposite direction: the WE is far from unique, and only costs, not flows, can be compared.

Formalization scope

The model follows §2–§3.2 of the paper and reuses the published definition KellyStochasticNetworks_Wardrop for arc flows, feasibility and the Wardrop condition. Paths are nonempty $0/1$ incidence columns (a generalization of loop-free paths that the proofs do not use); $K$ is nonempty and Condition 1 is standing ( $|S_k|\ge 2$ , every arc on a path). Costs are functions $\mathbb R\to\mathbb R$ constrained on $[0,\infty)$ only. $C^*$ is an infimum over all flows, $\tilde C$ a supremum over WE flows, $\rho=\tilde C/C^*$ ; the distance is (3.3) with the sup norm on demand and endpoint vectors and a supremum over the compact set $A\times[0,\min\{T(d),T(d')\}]$ . The derivative in Theorem 12b) is derivWithin on $[0,T(d)]$ , one-sided at the endpoints, and $C^1$ is ContDiffOn ℝ 1 on that interval.

Every statement quantifies over games in the game space only: off it, $\rho$ would be a junk ratio such as $0/0=0$ . The paper prints the conclusions of Theorem 12 and (4.33) with a strict inequality, which fails at $\Gamma'=\Gamma$ ; the non-strict form is posed, and no hypothesis $\Gamma'\neq\Gamma$ is added (distinct games can have distance $0$ ). Milestones (4.39) and (4.40) are posed for two arbitrary games of one demand slice, the general form of the paper's step for its auxiliary game.

A complete development needs existence of SO and WE flows on the game space, the variational characterization of Wardrop equilibria, the mean value theorem on a closed interval with one-sided derivatives, and continuity of $C^*$ in the metric; contributions of any of these as separate lemmas are welcome. The source is the arXiv preprint v3; the published Mathematics of Operations Research version is not the cited artifact.

Selected references

Z. Wu, R. H. Möhring, A sensitivity analysis of the price of anarchy in non-atomic congestion games, Mathematics of Operations Research 48(3), 2023; cited as arXiv:2007.13979v3, 2021. https://arxiv.org/abs/2007.13979v3
T. Roughgarden, É. Tardos, How bad is selfish routing?, Journal of the ACM 49(2), 2002. https://doi.org/10.1145/506147.506153
J. R. Correa, A. S. Schulz, N. E. Stier-Moses, Selfish routing in capacitated networks, Mathematics of Operations Research 29(4), 2004. https://doi.org/10.1287/moor.1040.0098
R. Cominetti, V. Dose, M. Scarsini, The price of anarchy in routing games as a function of the demand, arXiv:1907.10101v2, 2020. https://arxiv.org/abs/1907.10101
J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers 1(3), 1952. https://doi.org/10.1680/ipeds.1952.11259

8 thms2 active usersReviewed

Analysis Operations Research Optimization·Captain: mikedeng1

A Sensitivity Analysis of the Price of Anarchy in Nonatomic Congestion Games 1: The Price of Anarchy Is Hölder Continuous with Exponent 1/2 at Every Game with Costs Lipschitz on [0, T(d)]Research Paper

Motivation

The price of anarchy (PoA) of a nonatomic congestion game is the ratio of the total cost of a Wardrop equilibrium to the minimum possible total cost. It quantifies how much selfish routing loses compared with central coordination, and it has been studied intensively since Koutsoupias and Papadimitriou (1999) and Roughgarden and Tardos (2002), mostly through worst-case bounds over classes of cost functions.

Worst-case bounds say nothing about how the PoA of one particular network behaves when its data change. In transport applications both the cost functions (capacities, tolls, travel-time models) and the demands are estimated, so the PoA is only useful if small errors in the data cause small errors in the PoA. Wu and Möhring (arXiv:2007.13979, published in Mathematics of Operations Research, 2023) study this sensitivity question in a setting where cost functions and demands change simultaneously. Earlier sensitivity results changed only the demands, with the cost functions fixed: Englert, Franke and Olbrich (2010) bounded the growth of the PoA of a single-O/D network with polynomial costs of degree at most $\beta$ by a factor $(1+\epsilon)^\beta$ when the demand grows by a factor $1+\epsilon$ ; Takalloo and Kwon (2020) extended this to several O/D pairs whose demands are scaled together; and Cominetti, Dose and Scarsini (arXiv:1907.10101) studied differentiability of the PoA as a function of the demand of a single O/D pair. The main theorem of the paper, Theorem 9, is the subject of this mission.

Setting

A network consists of a finite set $A$ of arcs, a finite non-empty set $\mathcal K$ of origin–destination (O/D) pairs, and for every $k \in \mathcal K$ a non-empty set $\mathcal S_k$ of paths; each path is a non-empty set of arcs. From §3.1 onward the paper also assumes every arc lies on some path and every $\mathcal S_k$ has at least two paths (Condition 1).

A game $\Gamma = (\tau, d)$ on the network consists of cost functions $\tau_a : [0,\infty) \to [0,\infty)$ , one per arc, that are continuous and non-decreasing, and demands $d_k \ge 0$ , one per O/D pair. The total demand is $T(d) = \sum_k d_k$ . The game space $\mathcal G(G,\mathcal K,\mathcal S)$ consists of the games with $T(d) > 0$ and $\tau_a(x) > 0$ for all $x \in (0, T(d)]$ .

A flow $f = (f_s)$ assigns a non-negative amount to every path, with $\sum_{s\in\mathcal S_k} f_s = d_k$ . Its arc flows are $f_a = \sum_{s \ni a} f_s$ , its path costs $\tau_s(f) = \sum_{a\in s}\tau_a(f_a)$ , and its total cost

C(\Gamma, f) = \sum_{a\in A} f_a\,\tau_a(f_a).

A Wardrop equilibrium (WE) is a flow in which every used path of a pair is a cheapest path of that pair. The SO cost $\mathcal C^*(\Gamma)$ is the minimum total cost over all flows, the WE cost $\tilde{\mathcal C}(\Gamma)$ is the total cost of a WE flow (all WE flows have the same cost), and

\rho(\Gamma) = \frac{\tilde{\mathcal C}(\Gamma)}{\mathcal C^*(\Gamma)}.

Games are compared by the distance

\|\Gamma - \Gamma'\| = \max\Big\{\|d-d'\|_\infty,\ \max_{a\in A}\max_{x\in[0,\min\{T(d),T(d')\}]}|\tau_a(x) - \sigma_a(x)|,\ \|\tau(T(d)) - \sigma(T(d'))\|_\infty\Big\}

for $\Gamma = (\tau, d)$ and $\Gamma' = (\sigma, d')$ . It compares cost functions only on the range of flow values both games can produce, plus the values at the respective total demands. A function $h$ is Lipschitz continuous on $[0,T]$ with constant $M$ if $|h(x) - h(y)| \le M|x-y|$ for all $x, y \in [0,T]$ .

Formalization targets

Goal: Theorem 9 (p. 26)

Let $\Gamma = (\tau, d)$ be a game of the game space whose cost functions are Lipschitz continuous on $[0, T(d)]$ . Then there are $\epsilon_\Gamma > 0$ and $\kappa_\Gamma > 0$ , depending only on $\Gamma$ , such that

|\rho(\Gamma) - \rho(\Gamma')| \le \kappa_\Gamma\,\|\Gamma - \Gamma'\|^{1/2}\quad\text{for every game } \Gamma' \text{ of the game space with } \|\Gamma - \Gamma'\| < \epsilon_\Gamma.

The goal fixes the exponent $1/2$ and leaves the radius and the constant existential, which is the form the paper claims.

Milestones

Lemma 1a)–c) (p. 13): properties of $\epsilon$ -approximate WE flows, ending with

|C(\Gamma, f) - C(\Gamma, \tilde f)| \le |A|\sqrt{M\epsilon}\,T(d) + \epsilon

for an $\epsilon$ -approximate WE flow $f$ and a WE flow $\tilde f$ when all costs are $M$ -Lipschitz on $[0,T(d)]$ . 2. Lemma 10a)–d) (p. 27): on a demand slice (games with a common demand vector $w$ ), $\mathcal C^*$ is Lipschitz, WE flows of one game are $|A|\,T(w)\,\|\Gamma_1-\Gamma_2\|$ -approximate WE flows of the other, and $\tilde{\mathcal C}$ and $\rho$ are Hölder with exponent $1/2$ with explicit constants. 3. Lemma 11a)–c) (p. 31): on a cost slice (games with a common cost vector and $T(w') \le T(w)$ ), explicit Hölder bounds of exponent $1/2$ for $\tilde{\mathcal C}$ and $\rho$ and a Lipschitz bound for $\mathcal C^*$ .

Significance

Theorem 9 is the first pointwise Hölder continuity result for the PoA on the whole game space, with demands and costs perturbed together. Its hypothesis is mild (Lipschitz costs on a compact interval, which covers polynomial, BPR-type and piecewise linear costs), and such games are dense in the game space. Together with Theorem 8 of the same paper, which shows that no uniform Hölder bound exists, it describes exactly what kind of stability the PoA has: local, with a constant depending on the game, and exponent $1/2$ in general. The explicit constants of Lemmas 10 and 11 give computable error bounds for the PoA of a network whose data are known only approximately.

The result is proved in the paper; no machine-checked proof exists. This mission formalizes the statement and the explicit slice estimates the proof rests on. Lemma 1 is a self-contained statement about approximate Wardrop equilibria that is useful well beyond this paper, for instance for analysing iterative traffic-assignment algorithms, which only ever produce approximate equilibria.

Difficulty

The obvious approach compares an equilibrium of $\Gamma$ with an equilibrium of $\Gamma'$ directly. This fails because the two games have different demand vectors, so their flows live in different polytopes: an equilibrium of one game is not even a flow of the other. The paper separates the perturbation into a change of costs at fixed demand and a change of demand at fixed costs, through an auxiliary game, and each half needs its own argument. On a demand slice an equilibrium of one game is only an approximate equilibrium of the other, and the passage from an approximate equilibrium to its cost loses a square root (Lemma 1c), which is tight by Example 2). On a cost slice the demand has to be removed path by path from an equilibrium while keeping it an equilibrium of a shifted game. Finally, the constants of the slice estimates depend on the auxiliary game, and they must be controlled uniformly near $\Gamma$ .

Formalization scope

The Lean development fixes the following conventions.

The network is a structure with $|A|$ arcs, $|\mathcal S|$ paths and $|\mathcal K|$ O/D pairs, a 0/1 arc–path incidence matrix and the map sending a path to its pair. Lemma 1 uses the §2 model assumptions: 0/1 incidence, non-empty paths, $\mathcal K \neq \emptyset$ , and $|\mathcal S_k| \ge 1$ . The later results add Condition 1 (every arc on a path, $|\mathcal S_k| \ge 2$ ), as assumed from §3.1. Paths are arbitrary non-empty 0/1 columns, not necessarily loop-free paths of a digraph; the results do not use loop-freeness.
Cost functions are maps $\mathbb R \to \mathbb R$ required to be continuous, non-decreasing and non-negative on $[0,\infty)$ only.
Arc flows, Wardrop equilibria (2.1) and the potential (2.6) come from the published definition KellyStochasticNetworks_Wardrop. $\epsilon$ -approximate WE flows follow (2.7) in arc form. The total cost uses the arc form, which equals the path form for 0/1 incidence.
$\mathcal C^*$ is the infimum of costs over flows, $\tilde{\mathcal C}$ the supremum of costs over WE flows, $\rho$ their quotient. The middle term of the distance is the supremum of the image of the compact set $A\times[0,\min\{T(d),T(d')\}]$ , and $\|\cdot\|_\infty$ is the sup norm.
Every statement about $\rho$ , $\mathcal C^*$ or $\tilde{\mathcal C}$ quantifies over games of the game space, where $\rho$ is a genuine ratio of positive numbers. Off the game space Lean's division by zero would give $\rho = 0$ , so quantifying over all pairs $(\tau, d)$ would trivialize the statements; this is ruled out. In the goal, $\epsilon_\Gamma$ and $\kappa_\Gamma$ are chosen before $\Gamma'$ .
Several printed strict inequalities are posed as non-strict, because they fail at $\Gamma' = \Gamma$ or are attained in the paper's own Example 2. In Lemma 11 the printed constants are corrected by a factor $|\mathcal K|$ that the paper's own argument needs; each item's Formalization Note quotes the printed form.

A complete development needs: existence of Wardrop equilibria and uniqueness of their cost on the game space, existence of social optima, the integral inequality (2.9) for monotone costs, positivity of $\mathcal C^*$ on the game space, and the path-by-path demand-reduction construction of Lemma 11. The existence and uniqueness results and Lemma 1 are reusable in any formalization of selfish routing. Proofs of any milestone are welcome, as are the supporting lemmas above.

The source is the arXiv preprint arXiv:2007.13979v3 (23 Aug 2021); all page and theorem numbers refer to it, not to the published version.

Selected references

Z. Wu, R. H. Möhring, A sensitivity analysis of the price of anarchy in non-atomic congestion games, arXiv:2007.13979v3, 2021; Mathematics of Operations Research 48(3), 2023. https://arxiv.org/abs/2007.13979, https://doi.org/10.1287/moor.2022.1292
T. Roughgarden, É. Tardos, How bad is selfish routing?, Journal of the ACM 49(2), 2002. https://doi.org/10.1145/506147.506153
E. Koutsoupias, C. Papadimitriou, Worst-case equilibria, STACS 1999. https://doi.org/10.1007/3-540-49116-3_38
J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers 1(3), 1952. https://doi.org/10.1680/ipeds.1952.11259
M. Englert, T. Franke, L. Olbrich, Sensitivity of Wardrop equilibria, Theory of Computing Systems 47(1):3–14, 2010.
M. Takalloo, C. Kwon, Sensitivity of Wardrop equilibria: revisited, Optimization Letters 14(3):781–796, 2020.
R. Cominetti, V. Dose, M. Scarsini, The price of anarchy in routing games as a function of the demand, 2020. https://arxiv.org/abs/1907.10101

13 thms2 active usersReviewed

Operations Research Optimization·Captain: mikedeng1

A Sensitivity Analysis of the Price of Anarchy in Nonatomic Congestion Games 4: The Price of Anarchy Is Not Uniformly Hölder Continuous and No Game Has the Whole Space as a Hölder NeighborhoodResearch Paper

Motivation

The price of anarchy (PoA) of a nonatomic congestion game measures how much total cost is lost when a continuum of selfish users routes traffic instead of a central planner. Worst-case bounds on the PoA over classes of cost functions are classical: $4/3$ for affine costs and $\Theta(\beta/\ln\beta)$ for polynomial costs of degree at most $\beta$ (Roughgarden and Tardos 2002; Roughgarden 2003). Worst-case bounds say nothing about how the PoA of one particular instance reacts when its demands and cost functions are perturbed, which is what matters when traffic data are measured with error or change over time.

Z. Wu and R. H. Möhring (arXiv:2007.13979v3, published in Mathematics of Operations Research, 2023) study this sensitivity through Hölder continuity of the PoA map $\Gamma \mapsto \rho(\Gamma)$ on a metric space of games. Earlier work considered changes of the demand alone: Englert et al. (2010), Takalloo and Kwon (2020) and Cominetti et al. (2020), as cited in the paper, fix the cost functions and vary the demand. Wu and Möhring vary both. Their main positive results are local: Hölder continuity with exponent $1/2$ near every game with Lipschitz costs. This mission formalizes their negative result, Theorem 8, which says that no global version of this regularity is possible.

Setting

Fix a network with arcs $A$ , a non-empty finite set $K$ of origin–destination (O/D) pairs, and for each pair $k$ a set $S_k$ of paths, each a non-empty set of arcs, with $|S_k| \ge 2$ and every arc on some path (Condition 1). A game $\Gamma = (\tau, d)$ consists of cost functions $\tau_a$ , continuous, non-decreasing and non-negative on $[0,\infty)$ , and demands $d_k \ge 0$ with total demand $T(d) = \sum_k d_k$ . The game space $\mathcal G(G,K,S)$ consists of the games with $T(d) > 0$ and $\tau_a(x) > 0$ for $x \in (0, T(d)]$ (Condition 2).

A flow splits each $d_k$ non-negatively over $S_k$ ; its arc flows are $f_a = \sum_{s \ni a} f_s$ and its total cost is $C(\Gamma, f) = \sum_a f_a \tau_a(f_a)$ . A Wardrop equilibrium (WE) is a flow in which every used path of a pair has minimal cost among the paths of that pair. With $C^*(\Gamma)$ the minimum total cost and $\tilde C(\Gamma)$ the total cost of a WE flow,

\rho(\Gamma) = \frac{\tilde C(\Gamma)}{C^*(\Gamma)}.

The distance of two games $\Gamma = (\tau, d)$ , $\Gamma' = (\sigma, d')$ is

\|\Gamma - \Gamma'\| = \max\Big\{\|d - d'\|_\infty,\ \max_{a,\ x \in [0, \min\{T(d),T(d')\}]} |\tau_a(x) - \sigma_a(x)|,\ \|\tau(T(d)) - \sigma(T(d'))\|_\infty\Big\}.

The cost normalization $\Psi_\upsilon(\tau, d) = (\tau/\upsilon, d)$ , $\upsilon > 0$ , divides all costs by $\upsilon$ . A $\gamma$ -neighborhood of $\Gamma$ is an open set $U \ni \Gamma$ of games on which $|\rho(\Gamma) - \rho(\Gamma')| \le \varkappa_\Gamma \|\Gamma - \Gamma'\|^\gamma$ for some constant $\varkappa_\Gamma > 0$ .

Formalization targets

Goal: Theorem 8b)

For every game $\Gamma \in \mathcal G(G,K,S)$ and every $\gamma > 0$ ,

\neg\,\exists\, \varkappa > 0\ \ \forall \Gamma' \in \mathcal G(G,K,S):\ |\rho(\Gamma) - \rho(\Gamma')| \le \varkappa\, \|\Gamma - \Gamma'\|^\gamma,

that is, the whole game space is never a $\gamma$ -neighborhood: Hölder continuity of $\rho$ holds at best locally, even with a constant depending on the game.

Milestones

$\rho(\Psi_\upsilon(\Gamma)) = \rho(\Gamma)$ for $\upsilon > 0$ (§3.5).
$\|\Psi_\upsilon(\Gamma) - \Psi_\upsilon(\Gamma')\| = \|\Gamma - \Gamma'\|/\upsilon$ when $d = d'$ (3.11).
Some demand vector carries two games with different PoA (p. 24).
Theorem 8a): no $\gamma > 0$ , $\varkappa > 0$ make $\rho$ uniformly Hölder continuous on $\mathcal G(G,K,S)$ .
$\rho$ is unbounded on the demand slice $\{\Gamma' : d' = d\}$ whenever $d$ is supported on a single O/D pair (p. 25, corrected; see below).

Significance

Theorem 8 separates what can be proved about the sensitivity of the PoA from what cannot. Part a) rules out uniform Hölder (in particular Lipschitz) bounds; part b) rules out global bounds even with a game-dependent constant. Together they explain the shape of the paper's positive results (Theorems 9 and 12), which hold on balls around a game with constants that depend on that game.

The result is proved in the paper; no machine-checked version exists. Formalizing it fixes the exact hypotheses under which it holds. Two are not visible on the page: paths must form an antichain (otherwise $\rho \equiv 1$ is possible), and the unboundedness step of part b) does not hold on every demand slice. The milestones on cost normalizations are reusable for any scale-invariance argument about the PoA.

Difficulty

The invariance and scaling milestones are bookkeeping about suprema and infima. The substance is in the constructions. For 8a), two games with equal demands and different PoA are needed, which requires an explicit game whose Wardrop equilibrium is strictly inefficient on an arbitrary network satisfying Condition 1 and the antichain condition, so the WE cost and the SO cost must be computed or bounded, not just estimated asymptotically.

For 8b), the paper argues that a global Hölder bound makes $\rho$ bounded on the demand slice of $\Gamma$ , and that $\rho$ is unbounded there because the slice contains Pigou-like games. The second step fails in general: with several O/D pairs, other pairs can be forced through the arcs that distinguish the paths of every pair, and on such a slice $\rho$ can be bounded (an explicit three-pair network with $\rho \le 5/2$ on the slice $d = (1,1,1)$ is recorded in the milestone). The natural repair compares $\Gamma$ with games on a different slice, whose demand sits on one pair, and requires bounding the distance between games with different demands as the costs are normalized away.

Formalization scope

Lean represents paths as $0/1$ columns of an arc–path incidence matrix and pairs as a map from paths to pairs, on top of the published KellyStochasticNetworks_Wardrop definitions (arc flows, feasible flows, Wardrop's first principle). The commitments are:

the standing assumptions are G1–G2 (non-empty $K$ , non-empty paths), $0/1$ incidences and Condition 1;
the antichain condition (no path of a pair inside another path of the same pair) is an added hypothesis of every theorem. It holds for loop-free paths of a digraph, which the paper assumes;
costs are real functions whose properties are required on $[0,\infty)$ only;
$C^*$ is an infimum over all flows and $\tilde C$ a supremum over WE flows. All WE flows have the same cost;
the distance uses the sup norm and a supremum over the compact set $A \times [0, \min\{T(d),T(d')\}]$ ;
powers are real powers with $\gamma > 0$ .

Every game in every statement ranges over the game space. A formalization quantifying over arbitrary pairs $(\tau, d)$ would be trivial: Lean's $0/0 = 0$ gives such pairs $\rho = 0$ , and a junk game next to a real one breaks any Hölder bound for free.

The unboundedness milestone is posed for single-pair demand slices instead of the page's arbitrary slice, because the page's version is false for some multi-pair networks. Its asymptotic rate $\Theta(\beta/\ln\beta)$ is cited by the paper and not posed. Contributions of the two constructions (a strictly inefficient game for 8a, Pigou-type games on one pair for 8b) and of the distance estimates are welcome; related Pigou statements exist as SelfishRouting.Linear.figure_3_pigou (Roughgarden–Tardos).

The source is the arXiv preprint v3; the published MOR version is not the cited artifact.

Selected references

Z. Wu, R. H. Möhring, A sensitivity analysis of the price of anarchy in nonatomic congestion games, Mathematics of Operations Research 48(3), 2023; cited as arXiv:2007.13979v3 (2021). https://arxiv.org/abs/2007.13979v3
T. Roughgarden, É. Tardos, How bad is selfish routing?, Journal of the ACM 49(2), 2002. https://doi.org/10.1145/506147.506153
T. Roughgarden, The price of anarchy is independent of the network topology, Journal of Computer and System Sciences 67(2), 2003. https://doi.org/10.1016/S0022-0000(03)00044-8

8 thms2 active usersReviewed

Operations Research Optimization·Captain: mikedeng1

A Sensitivity Analysis of the Price of Anarchy in Nonatomic Congestion Games 5: For Small Total Demand the Price of Anarchy Exceeds 1 by at Most an Explicit Multiple of the Total DemandResearch Paper

Motivation

The price of anarchy (PoA) of a nonatomic congestion game is the ratio between the total travel cost at a Wardrop equilibrium, where every traveller uses a cheapest route, and the minimum total cost a central planner could achieve. Worst-case bounds on the PoA are classical (Roughgarden and Tardos, 2002), but traffic studies observe that the empirical PoA is close to $1$ both in light and in heavy traffic (Youn, Gastner and Jeong, 2008; O'Hare, Connors and Watling, 2016). This raises the question of how the PoA of a fixed network with fixed cost functions behaves as the demand varies.

For decreasing demand the literature had one convergence result: for polynomial costs, Colini-Baldeschi, Cominetti, Mertikopoulos and Scarsini (2020) show $\rho \to 1$ when the total demand tends to $0$ with fixed demand proportions, at rate $O(T(d))$ . Wu and Möhring (2021) obtain a rate for arbitrary cost functions that are strictly positive and Lipschitz near $0$ , with no condition on the demand proportions, as a corollary of their sensitivity analysis of the PoA. This mission formalizes that corollary, Corollary 5.1 of arXiv:2007.13979v3.

Setting

A structure consists of a finite set $A$ of arcs, a finite nonempty set $\mathcal K$ of origin–destination (O/D) pairs, and for every pair $k$ a set $\mathcal S_k$ of at least two paths, each a nonempty set of arcs; every arc lies on some path. A game $\Gamma = (\tau, d)$ is a vector of arc cost functions $\tau_a : [0,\infty) \to [0,\infty)$ , continuous and non-decreasing, together with demands $d_k \ge 0$ of total $T(d) = \sum_k d_k$ . The game space $\mathcal G(G, \mathcal K, \mathcal S)$ consists of the games with $T(d) > 0$ and $\tau_a(x) > 0$ on $(0, T(d)]$ .

A flow $f = (f_s)$ routes $d_k$ over $\mathcal S_k$ with $f_s \ge 0$ . Arc flows are $f_a = \sum_{s \ni a} f_s$ and the total cost is $C(\Gamma, f) = \sum_a f_a \tau_a(f_a)$ . A flow is a Wardrop equilibrium if every used path is a cheapest path of its pair. With $\mathcal C^*(\Gamma)$ the minimum total cost and $\tilde{\mathcal C}(\Gamma)$ the cost of a Wardrop equilibrium (all equilibria have the same cost),

\rho(\Gamma) = \frac{\tilde{\mathcal C}(\Gamma)}{\mathcal C^*(\Gamma)} \ge 1.

Games are compared by the distance (3.3),

\|\Gamma - \Gamma'\| = \max\Big\{\|d - d'\|_\infty,\ \max_{a,\ x \in [0, \min\{T(d), T(d')\}]} |\tau_a(x) - \sigma_a(x)|,\ \|\tau(T(d)) - \sigma(T(d'))\|_\infty\Big\},

and the demand normalization $\Lambda_\upsilon(\tau, d) = (\tau \circ \upsilon, d/\upsilon)$ , with $(\tau_a \circ \upsilon)(x) = \tau_a(x\upsilon)$ , rescales a game to a different total demand. The cost slice of $\tau$ is the set of games whose costs agree with $\tau$ on $[0, T(d)]$ .

Formalization targets

Goal: Corollary 5.1 (p. 43)

Let the costs $\tau_a$ be strictly positive on $[0,\infty)$ and Lipschitz on $[0, b]$ with constant $M_\tau > 0$ , and let $\tau_{\min}(0) = \min_a \tau_a(0)$ . There is $\delta > 0$ such that for every demand vector $d \ge 0$ with $0 < T(d) < \delta$ ,

\rho(\tau, d) \le 1 + \frac{8 \cdot |A| \cdot (|\mathcal K| + 1)}{\tau_{\min}(0)} \cdot M_\tau \cdot T(d).

Milestones

§3.5, p. 22. $\Lambda_\upsilon$ preserves the game space, maps WE and SO flows to WE and SO flows (divided by $\upsilon$ ), scales the total cost by $1/\upsilon$ , and leaves $\rho$ unchanged.
p. 43, first display. With $\sigma_a \equiv \tau_a(0)$ and $\Gamma' = (\sigma, d/T(d))$ : $\|\Gamma' - \Lambda_{T(d)}(\tau, d)\| = \max_a |\tau_a(T(d)) - \tau_a(0)| \le M_\tau T(d)$ when $T(d) \le b$ .
p. 43. $\mathcal C^*(\Gamma') \ge \tau_{\min}(0)$ for every $d$ .
p. 43, second display. For $T(d)$ below a threshold independent of $d$ : $\rho(\Gamma') = 1$ and $|\rho(\Lambda_{T(d)}(\tau,d)) - \rho(\Gamma')| \le 8|A|(|\mathcal K|+1) M_\tau T(d)/\tau_{\min}(0)$ .

Significance

The corollary gives a rate of convergence of the PoA to $1$ in light traffic for every cost vector that is strictly positive at $0$ and Lipschitz near $0$ , with an explicit constant depending only on the number of arcs, the number of O/D pairs, the Lipschitz constant and the free-flow costs $\tau_a(0)$ . It removes the fixed-proportion condition on the demands needed in the earlier polynomial result, and it combines with the heavy-traffic results for regularly varying costs to show that the PoA is bounded on whole cost slices (p. 43).

The result is proved in the paper, in a few lines on top of the local Lipschitz estimate (4.33) of Theorem 12a). To our knowledge it has no machine-checked proof. Formalizing it requires a Lean model of nonatomic congestion games with demand normalizations and the metric (3.3), together with the comparison between a game of total demand $1$ and the constant-cost game at the same demand, which is reusable for other light-traffic statements.

Difficulty

A direct bound $\rho(\tau, d) \le 1 + c\,T(d)$ cannot simply be read off as $T(d) \to 0$ : the costs $\mathcal C^*$ and $\tilde{\mathcal C}$ both tend to $0$ with the demand, so their ratio is a quotient of two vanishing quantities, and an additive estimate on each cost says nothing about the ratio. The difficulty is to obtain a bound in which neither the threshold on $T(d)$ nor the constant depends on the demand vector $d$ , including the proportions $d_k/T(d)$ , which may vary arbitrarily, and some of which may vanish. Any argument whose constants depend on the particular game near which it works (as a pointwise Hölder constant does) gives only a pointwise statement, not the uniform one asserted here.

Formalization scope

The Lean development lives in the namespace SensitivityPoA.SmallDemand and builds on the published definition KellyStochasticNetworks_Wardrop (flows, arc flows, Wardrop's first principle). Conventions:

The structure is a 0/1 arc–route incidence matrix with a map from routes to O/D pairs. Standing assumptions (disclosed): every route contains an arc, $\mathcal K$ is nonempty, and Condition 1 (every arc on some route, $|\mathcal S_k| \ge 2$ ). Routes are arbitrary 0/1 columns, a generalization of loop-free paths.
Cost functions are functions $\mathbb R \to \mathbb R$ that are continuous, non-decreasing and non-negative on $[0,\infty)$ . "Strictly positive" means $\tau_a(x) > 0$ for all $x \ge 0$ . "Lipschitz on $[0,b]$ with constant $M_\tau$ " means $|\tau_a(x) - \tau_a(y)| \le M_\tau |x-y|$ for $x, y \in [0,b]$ ; nothing is assumed beyond $b$ .
$\mathcal C^*$ is the real infimum of the total cost over flows, $\tilde{\mathcal C}$ the real supremum over WE flows, $\rho$ their quotient. The maxima in (3.3) are real suprema of images of compact sets and Mathlib's sup norm.
The corollary is stated for the game $(\tau, d)$ itself; games of the cost slice agree with it on $[0, T(d)]$ .
Corrected slip. The corollary prints the constant $8 \cdot M_\tau \cdot |A| \cdot (|\mathcal K|+1)/\tau_{\min}(0) \cdot M_\tau$ , with $M_\tau$ twice. The display it summarizes has $M_\tau$ once, which is what is posed; it implies the printed form whenever $M_\tau \ge 1$ .

A trivializing formalization is ruled out: the threshold $\delta$ is chosen before $d$ (choosing it after $d$ makes the statement vacuous), $T(d) > 0$ is required (at $T(d) = 0$ Lean's $0/0 = 0$ would make $\rho = 0$ ), every game considered lies in the game space, and the bounds use $\le$ , which holds at equality cases.

Contributions welcome: proofs of the milestones, the comparison of WE costs under pointwise cost perturbation (the variational inequality of Wardrop equilibria), and existence of Wardrop equilibria for costs that are continuous and monotone only on $[0,\infty)$ . The source is the arXiv preprint v3; the published version in Mathematics of Operations Research is not the cited artifact.

Selected references

Z. Wu, R. H. Möhring, A sensitivity analysis of the PoA in non-atomic congestion games, arXiv:2007.13979v3, 2021; published as A Sensitivity Analysis of the Price of Anarchy in Nonatomic Congestion Games, Mathematics of Operations Research 48(3), 2023. https://arxiv.org/abs/2007.13979 , https://doi.org/10.1287/moor.2022.1292
R. Colini-Baldeschi, R. Cominetti, P. Mertikopoulos, M. Scarsini, When is selfish routing bad? The price of anarchy in light and heavy traffic, Operations Research 68(2), 2020. https://doi.org/10.1287/opre.2019.1894
T. Roughgarden, É. Tardos, How bad is selfish routing?, Journal of the ACM 49(2), 2002. https://doi.org/10.1145/506147.506153
H. Youn, M. T. Gastner, H. Jeong, Price of anarchy in transportation networks: efficiency and optimality control, Physical Review Letters 101, 2008. https://doi.org/10.1103/PhysRevLett.101.128701
S. J. O'Hare, R. D. Connors, D. P. Watling, Mechanisms that govern how the price of anarchy varies with travel demand, Transportation Research Part B: Methodological 84:55–80, 2016 (cited in arXiv:2007.13979v3, p. 50).

7 thms2 active usersReviewed

Analysis Operations Research Optimization+1·Captain: mikedeng1

A Sensitivity Analysis of the Price of Anarchy in Nonatomic Congestion Games 2: The Social Optimum Cost, the Wardrop Equilibrium Cost and the Price of Anarchy Are Continuous on the Game SpaceResearch Paper

Motivation

Traffic users choose routes for themselves, while a planner may choose routes that minimize everyone's combined travel cost. The price of anarchy measures the cost of the users' equilibrium relative to the planner's optimum. Travel demand and arc latency functions are estimated from data and change over time, so a ratio that changes abruptly under a small input change would be difficult to interpret or use. Wu and Möhring study this sensitivity for nonatomic congestion games, where each individual user has negligible influence on arc flows. Their preprint proves that the optimum cost, equilibrium cost, and their ratio vary continuously over the game space they define. This mission isolates that foundational continuity result. It supplies the qualitative starting point for the paper's later Hölder and Lipschitz estimates.

The cited artifact is arXiv:2007.13979v3, dated 2021. The article subsequently appeared in Mathematics of Operations Research in 2023, but theorem numbers and pages here refer to the preprint.

Setting

Fix finite sets $A$ of arcs, $S$ of routes, and $K$ of origin–destination pairs. Each route $s$ serves one pair $k$ and contains at least one arc. Every arc belongs to some route, and every pair has at least two routes. A game $\Gamma=(\tau,d)$ assigns each arc $a$ a nonnegative, nondecreasing, continuous latency function $\tau_a:[0,\infty)\to[0,\infty)$ and each pair $k$ a nonnegative demand $d_k$ . The total demand is $T(d)=\sum_{k\in K}d_k$ . These are the paper's basic model and standing combinatorial assumptions (pp. 10–11 and 14).

A feasible flow $f$ puts nonnegative traffic on routes so that the traffic for each pair sums to its demand. The induced arc flow is $f_a=\sum_{s\ni a}f_s$ . Its total cost is

C(\Gamma,f)=\sum_{a\in A} f_a\tau_a(f_a).

A social optimum (SO) is a feasible flow minimizing total cost. A Wardrop equilibrium (WE) is a feasible flow in which every route carrying positive traffic has minimum cost among the routes serving the same pair. Write $C^*(\Gamma)$ for the SO cost and $\widetilde C(\Gamma)$ for the WE cost. The paper shows that all SO flows have the same cost and all WE flows have the same cost (pp. 11–12 and 18).

A generalized game has the stated nonnegative demands and regular latency functions. The game space $\mathcal G(G,K,S)$ further requires $T(d)>0$ and $\tau_a(x)>0$ for every arc and every $0<x\le T(d)$ , the paper's Condition 2. On this space, the optimum cost is positive and the price of anarchy is defined by

\rho(\Gamma)=\frac{\widetilde C(\Gamma)}{C^*(\Gamma)}.

For $\Gamma=(\tau,d)$ and $\Gamma'=(\sigma,d')$ , the paper's distance $\operatorname{Dist}(\Gamma,\Gamma')$ is the maximum of three discrepancies: the sup norm of $d-d'$ , the largest $|\tau_a(x)-\sigma_a(x)|$ for $a\in A$ and $0\le x\le\min\{T(d),T(d')\}$ , and the sup norm of $\tau(T(d))-\sigma(T(d'))$ . The last term compares costs at the two games' respective demand endpoints. Games with equal demands and equal latency functions up to that demand are identified as equivalent (pp. 15–17, (3.1)–(3.3)).

Formalization targets

The supporting milestones establish a positive lower bound for $C^*$ and an upper bound for $\rho$ (Lemma 3), the distance properties of generalized games (Lemma 4), and behavior of feasible, SO, and WE flows under convergent game sequences (Lemma 5). The goal is the paper's Theorem 6, p. 19: for any sequence $\Gamma_n\in\mathcal G(G,K,S)$ with $\operatorname{Dist}(\Gamma_n,\Gamma)\to0$ and $\Gamma\in\mathcal G(G,K,S)$ ,

C^*(\Gamma_n)\to C^*(\Gamma),\qquad \widetilde C(\Gamma_n)\to\widetilde C(\Gamma),\qquad \rho(\Gamma_n)\to\rho(\Gamma).

Significance

The theorem establishes that sufficiently small changes in both demand and latency data produce small changes in the two total costs and their ratio. It allows the PoA to be treated as a stable observable of a game, including where the identity of an optimum or equilibrium flow changes. The result is qualitative: it does not supply a uniform rate of change. The same paper investigates sharper rates under additional assumptions (§4).

The mathematical result is proved in the paper. In this mission its statements and definitions are compiled Lean drafts, while proofs of Theorem 6 and its milestone lemmas remain open. A completed development would make the game-space metric, limit-of-flow statements, and cost continuity available for later sensitivity results on nonatomic routing.

Difficulty

Pointwise continuity of each $\tau_a$ does not by itself control an optimum or equilibrium when demands change: the feasible-flow sets change with $d$ , and a flow for one game need not be feasible for another. A converging sequence of games can also have different optimal or equilibrium flows at every index. The distance compares functions only on demand-relevant intervals, so limits of costs must respect those varying intervals. Finally, continuity of the quotient requires a positive optimum cost throughout the game space; the paper's Condition 2 is what makes that denominator meaningful (pp. 15–19).

Formalization scope

Lean uses finite types for arcs, routes, and pairs; a route is a nonempty $0$ – $1$ incidence column and is assigned to one pair. This admits arbitrary route collections rather than insisting on loop-free directed graph paths. The standing network predicate records the nonempty pair set, nonempty routes, every arc's membership in a route, and at least two routes per pair. Costs are total functions on the reals, with continuity, monotonicity, and nonnegativity required only on $[0,\infty)$ . Flow feasibility, arc flow, the Wardrop condition, and the potential reuse the published KellyStochasticNetworks_Wardrop definition. The total cost uses the arc formula; $C^*$ is an infimum over feasible flows and $\widetilde C$ a supremum over WE flows. On valid games these recover the paper's common SO and WE costs.

The distance uses the sup norm on finite vectors and a real supremum over the bounded shared demand interval. Convergence is stated sequentially, following the paper, without imposing a metric-space instance on raw games that may be equivalent. Every theorem involving $\rho$ quantifies over the game space, so a zero denominator or an empty equilibrium set cannot supply a spurious value. The route-count and arc-count factors in Lemma 3 are the actual finite cardinalities. Contributions that establish existence and compactness of relevant flow sets, equivalence of the arc and path cost formulas, and the stated limit properties are useful beyond this theorem.

Selected references

Z. Wu and R. H. Möhring, A sensitivity analysis of the PoA in non-atomic congestion games, arXiv:2007.13979v3, 2021. Preprint.
Z. Wu and R. H. Möhring, A Sensitivity Analysis of the Price of Anarchy in Nonatomic Congestion Games, Mathematics of Operations Research 48(3), 2023. DOI.

9 thms2 active usersReviewed

Completed

Mechanism Design·Captain: mikedeng1

Allocating Indivisible Goods to Strategic Agents: Pure Nash Equilibria and Fairness 2: Round-Robin Has a Pure Nash Equilibrium in Every Instance with Additive ValuationsResearch Paper

Motivation

Fair division of indivisible goods asks how to split a set of items among agents with different values so that nobody has strong grounds to complain. Algorithms with fairness guarantees, such as Round-Robin, which always produces an allocation that is envy-free up to one good (EF1) when agents report their true additive valuations (Caragiannis et al., 2019), assume that agents report truthfully. Real agents are strategic, and truthful reporting is generally not an equilibrium of sequential allocation mechanisms (Kohler and Chandrasekaran, 1971). Amanatidis, Birmpas, Fusco, Lazos, Leonardi and Reiffenhäuser (arXiv:2109.08644, Mathematics of Operations Research 2024) ask instead whether the outcomes of a mechanism's pure Nash equilibria are fair. For that question to be meaningful, equilibria must exist.

Timeline.

2017: Aziz, Goldberg and Walsh (ADT 2017, LNCS 10576, pp. 270–283, volume) show that Round-Robin has pure Nash equilibria, built from the so-called bluff profile, whenever every agent values every good positively and no agent values two goods equally.
2021–2024: Amanatidis et al. prove that every PNE of Round-Robin is EF1 with respect to the true valuations (their Theorem 3.3), and in Appendix A remove the positivity and strictness assumptions from the existence result (Theorem A.3).

Setting

An instance is a triple $(N, M, v)$ : a set $N = \{1, \dots, n\}$ of $n \ge 1$ agents, a set $M = \{g_1, \dots, g_m\}$ of goods, and for every agent $i$ a non-negative value $v_i(g) \ge 0$ for every good $g$ . Valuations are additive: $v_i(S) = \sum_{g \in S} v_i(g)$ . Zero values and ties are allowed. All goods must be allocated.

Agents do not report $v_i$ . Each agent submits a bid $\mathbf b_i \in \mathbb R^m_{\ge 0}$ , and a mechanism maps the bid profile $\mathbf b = (\mathbf b_1, \dots, \mathbf b_n)$ to an allocation. In Round-Robin (Mechanism 1) the agents take turns in the order $1, 2, \dots, n, 1, 2, \dots$ . At each turn the active agent receives the still-available good with the largest bid. Ties are broken lexicographically: $g$ beats $h$ for agent $i$ if $\mathbf b_i(g) > \mathbf b_i(h)$ , or if $\mathbf b_i(g) = \mathbf b_i(h)$ and $g$ has the smaller index.

A bid $\mathbf b_i$ is a best response to $\mathbf b_{-i}$ if $v_i(\mathrm{RR}(\mathbf b'_i, \mathbf b_{-i})_i) \le v_i(\mathrm{RR}(\mathbf b)_i)$ for every $\mathbf b'_i \in \mathbb R^m_{\ge 0}$ . A profile is a pure Nash equilibrium (PNE) if every agent's bid is a best response (Definition 2.7). The mechanism reads only bids. The bundles are judged with the true values.

Formalization targets

Goal: Theorem A.3

For every instance with non-negative additive valuations,

\exists\, \mathbf b \in (\mathbb R^m_{\ge 0})^n\quad \forall i \in N\ \ \forall \mathbf b'_i \in \mathbb R^m_{\ge 0}:\quad v_i\big(\mathrm{RR}(\mathbf b'_i, \mathbf b_{-i})_i\big) \le v_i\big(\mathrm{RR}(\mathbf b)_i\big).

Milestones

Theorem A.2 (cited from Aziz et al.): the same conclusion when $v_i(g) > 0$ for all $i, g$ and each $v_i$ is injective on goods.
Positive strict perturbation (proof of Theorem A.3, first paragraph): every value vector $w \ge 0$ has a positive, injective, order-consistent $w'$ with $w(T) \le w'(T) \le w(T) + 2\varepsilon/3$ for every bundle $T$ . Here $\varepsilon$ is the smallest positive gap between two bundle values.
Equilibrium transfer (proof of Theorem A.3, third paragraph): if $v_i(T) \le v'_i(T) \le v_i(T) + 2\varepsilon_i/3$ for all $i$ and $T$ , then every PNE of Round-Robin under $v'$ is a PNE under $v$ .

Significance

Theorem A.3 is half of the paper's headline result for Round-Robin. Theorem 3.3 says that every PNE is EF1 with respect to the true valuations, and Theorem A.3 says that a PNE always exists. Together they show that a designer using Round-Robin gets EF1 outcomes at equilibrium on every additive instance, not only on strict ones. Without existence, the fairness of equilibria would be vacuous on the instances with ties or zero values, which arise naturally (indifferent agents, worthless goods).

The result is proved in the paper, modulo the cited Theorem A.2. As far as is known, none of it is machine-checked. A complete formalization would check the bluff-profile equilibrium of Aziz et al. for bid-based Round-Robin with lexicographic tie-breaking and deviations over all real bid vectors. It would also repair a gap in the perturbation argument. The page measures the perturbation against the smallest difference between two goods, which does not bound the difference between two bundles (values $0, 3, 5, 9$ : the good gap is $2$ , but $\{g_1, g_4\}$ and $\{g_2, g_3\}$ differ by $1$ ). The milestones use the bundle-level gap, which makes the argument go through.

Difficulty

The obstacle is Theorem A.2. Truthful bidding is not an equilibrium: on page 7 of the paper, with two agents and three goods, agent 1 gains by bidding for a good that agent 2 would otherwise take first. So an equilibrium must be constructed, and verifying it requires bounding the value of every deviation of every agent. A deviation changes the order in which all later goods are taken, so its effect is not local. The equilibrium property quantifies over a continuum of real bid vectors. Reducing to strict positive valuations also requires care: a perturbation that is small for each good can still reverse a comparison between two bundles.

Formalization scope

Agents are Fin n with [NeZero n], goods are Fin m, both 0-based. Values are v : Fin n → Fin m → ℝ with 0 ≤ v i g, and val v i S is the sum over S. Bids are non-negative real vectors. IsPNE mech v b requires every bid to be non-negative and every agent's bid to be a best response against all non-negative deviations, with bundle values computed from the true v.

Round-Robin is computed step by step. rank c sorts goods by non-increasing bid with a stable sort, which implements the lexicographic tie-breaking. rrFrom s G runs Round-Robin from start agent s on goods G. The goal uses only roundRobin = rrFrom 0 univ (Mechanism 1). goodGap is the page's $\varepsilon$ , and bundleGap is the repaired one used in milestones 2–3.

The goal has no positivity or injectivity hypothesis. Several statements would trivialize it and are excluded: an equilibrium over rankings or over a finite menu of bids instead of all of $\mathbb R^m_{\ge 0}$ ; bundle values measured on bids instead of true values; and Round-Robin with arbitrary rather than lexicographic tie-breaking, which would change the mechanism.

Needed infrastructure: the run of Round-Robin as a function of rankings, invariance of the allocation under bid changes that preserve the ranking, and the bluff-profile construction. These are reusable for any sequential allocation mechanism. The equilibrium-transfer milestone holds for any mechanism and is elementary. Lemma A.1 (a strict perturbation preserving best responses, p. 23) is formalized in the companion mission on EF1 equilibria. Contributions of the infrastructure above, of a proof of Theorem A.2, and of alternative existence proofs are welcome.

Selected references

G. Amanatidis, G. Birmpas, F. Fusco, P. Lazos, S. Leonardi, R. Reiffenhäuser, Allocating Indivisible Goods to Strategic Agents: Pure Nash Equilibria and Fairness, Mathematics of Operations Research, 2024; arXiv:2109.08644v2. https://arxiv.org/abs/2109.08644
H. Aziz, P. Goldberg, T. Walsh, Equilibria in Sequential Allocation, Algorithmic Decision Theory (ADT), LNCS 10576, pp. 270–283, 2017. https://doi.org/10.1007/978-3-319-67504-6 (proceedings volume)
I. Caragiannis, D. Kurokawa, H. Moulin, A. D. Procaccia, N. Shah, J. Wang, The Unreasonable Fairness of Maximum Nash Welfare, ACM Transactions on Economics and Computation, 2019. https://doi.org/10.1145/3355902
D. A. Kohler, R. Chandrasekaran, A Class of Sequential Games, Operations Research 19(2), 1971. https://doi.org/10.1287/opre.19.2.270

6 thms2 active usersReviewed

Completed

Mechanism Design·Captain: mikedeng1

Allocating Indivisible Goods to Strategic Agents: Pure Nash Equilibria and Fairness 3: Mod-Cut&Choose Always Has a Pure Nash Equilibrium and Every One Is MMS and EFXResearch Paper

Motivation

Fair division of indivisible goods asks how to split a set of items among agents with different tastes so that nobody has a strong reason to complain. Fairness notions such as envy-freeness up to any good (EFX) and the maximin share (MMS) have been studied extensively as algorithmic targets: given the agents' valuations, compute an allocation satisfying the notion. In practice the valuations are private, and an agent may misreport them to obtain a better bundle. Truthful mechanisms are too weak for this setting: for two agents, no truthful mechanism without payments produces EFX (or even EF1) allocations when there are more than four goods (Amanatidis, Birmpas, Christodoulou, Markakis, EC 2017).

Amanatidis, Birmpas, Fusco, Lazos, Leonardi and Reiffenhäuser (arXiv:2109.08644, Mathematics of Operations Research 2024) take a different route. They let agents bid strategically and ask how fair the pure Nash equilibria of a non-truthful mechanism are with respect to the agents' true valuations. For two agents they study a modified version of the classical cut-and-choose protocol, due in this form to Plaut and Roughgarden (SIAM J. Discrete Math. 2020). They show that it always has equilibria and that all of them are MMS, and hence EFX. As an algorithm run on truthful values, the same mechanism guarantees no more than a $5/6$ fraction of the maximin share.

Setting

There are two agents $N=\{1,2\}$ and a set $M=\{g_1,\dots,g_m\}$ of $m$ indivisible goods. Agent $i$ has a non-negative value $v_i(g)$ for each good and values a bundle $S\subseteq M$ additively, $v_i(S)=\sum_{g\in S}v_i(g)$ . There is no free disposal, so an allocation $(A_1,A_2)$ is a partition of $M$ .

EFX (Definition 2.1): for all $i,j$ and every good $g\in A_j$ with $v_i(g)>0$ , $v_i(A_i)\ge v_i(A_j\setminus\{g\})$ .
Maximin share (Definition 2.3): $\mu_i=\max_{(X_1,X_2)}\min\{v_i(X_1),v_i(X_2)\}$ , the maximum over partitions of $M$ into two bundles. An allocation is MMS if $v_i(A_i)\ge\mu_i$ for both agents.
Bids: each agent reports a bid vector $\mathbf b_i\in\mathbb R^m_{\ge0}$ , and $\mathbf b_i(S)=\sum_{h\in S}\mathbf b_i(h)$ .
Pure Nash equilibrium (Definition 2.7): a bid profile $\mathbf b$ is a PNE of a mechanism $\mathcal M$ if no agent $i$ has a bid $\mathbf b'_i\in\mathbb R^m_{\ge0}$ with $v_i(\mathcal M(\mathbf b'_i,\mathbf b_{-i}))>v_i(\mathcal M(\mathbf b))$ .

Mod-Cut&Choose (Mechanism 2) works as follows:

It sorts the goods in non-increasing order of agent 1's bid, breaking ties by index.
It builds two bundles $E_1,E_2$ greedily: each good goes to the bundle with the smaller $\mathbf b_1$ -value, ties to $E_1$ .
Agent 2 receives the bundle with the larger $\mathbf b_2$ -value (ties to $E_1$ ), and agent 1 receives the other.

In the Lean development these objects are val, IsBestResponse, IsPNE and rank (namespace StrategicAlloc.RRFair, shared with the sibling missions) and IsEFX, mu, IsApproxMMS, cut and modCutChoose (namespace StrategicAlloc.CutChoose).

Formalization targets

Goal: Theorem 4.3 (p. 18)

For every instance with two agents and non-negative additive valuations,

\exists\,\mathbf b:\ \mathbf b\text{ is a PNE of Mod-Cut\&Choose},\qquad\text{and}\qquad \forall\,\text{PNE }\mathbf b:\ \mathcal M(\mathbf b)\text{ is MMS and EFX w.r.t. } v_1,v_2 .

Both halves are part of the goal. Existence alone, or fairness of equilibria alone, is a weaker statement.

Milestones

Theorem 2.5 (p. 5): for two agents every MMS allocation is EFX.
§2.1, p. 5: $n\cdot\mu_i(n,S)\le v_i(S)$ . This is the published open statement LittleCharity.MMS.mms_le_average, used here as a reference.
Lemma 4.1 (p. 17): for every partition $(X_1,X_2)$ of $M$ , agent 1 has a non-negative bid under which the cut is $\{E_1,E_2\}=\{X_1,X_2\}$ .
Corollary 4.2 (p. 18): agent 1 can force a $\mu_1$ -partition, i.e. a cut with $\min\{v_1(E_1),v_1(E_2)\}=\mu_1$ .
Proof of Theorem 4.3, p. 18: agent 2's truthful bid is a best response to every bid of agent 1.
Proof of Theorem 4.3, p. 18: with her truthful bid, agent 2 receives at least $v_2(M)/2$ .

Significance

The theorem identifies a simple mechanism whose strategic outcomes are as fair as the best allocations that exist for two agents: every MMS allocation is EFX, and an MMS allocation always exists for two agents. The mechanism achieves this without any truthfulness requirement. It is the positive counterpart to the impossibility results for truthful mechanisms. It is also the starting point of §4.2 of the same paper, which asks how much of this guarantee survives for every mechanism whose equilibria are always EFX (Theorems 4.5 and 4.7).

The result is proved in the paper. As far as the platform's catalogue shows, none of it is formalized. This mission produces:

a machine-checked model of strategic fair division with bids, in which deviations range over all non-negative real bid vectors;
an executable definition of Mod-Cut&Choose with its exact tie-breaking;
formal proofs of the "agent 1 can force any cut" lemma and of MMS ⇒ EFX for two agents.

Difficulty

The fairness half is short once its ingredients are available. The weight lies in Lemma 4.1: the cut phase is a greedy procedure over a bid-sorted order, and showing that every partition of $M$ can be produced requires explicit bids and an invariant along the greedy loop. The case where both sets have at least two goods needs carefully calibrated values. The tie-breaking rules (lexicographic sorting, ties to $E_1$ in both phases) enter the argument, and the formalization fixes them exactly.

A natural shortcut is to restrict agent 1's strategies to orderings of the goods, or to assume that any cut is reachable. Either one turns Lemma 4.1 into an assumption. The existence half needs no compactness argument: the set of possible cuts is finite, so a best cut for agent 1 exists, but this has to be connected with deviations over the continuum of real bid vectors.

Formalization scope

Agents are Fin 2 (agent 1 is 0) and goods are Fin m, indexed in the order $g_1,\dots,g_m$ that lexicographic tie-breaking refers to.
Valuations and bids are functions Fin 2 → Fin m → ℝ. Non-negativity of $v$ is a hypothesis of every theorem, and every bid in a profile or deviation is required to be non-negative.
mu v i reuses the published LittleCharity.MMS.mms with two bundles and $S=M$ .
EFX is the paper's Definition 2.1, which removes only goods of positive value. The every-good variant LittleCharity.MMS.IsEFX is not used.
Disclosed correction: line 2 of Mechanism 2 on the page sorts "w.r.t. $v_1$ ". A mechanism reads only bids, and the proof of Lemma 4.1 sorts by the declared bids, so the formal mechanism sorts by agent 1's bid $\mathbf b_1$ .

The statements rule out the trivializing formalizations. Deviations are not restricted to a subset of bids (rankings, truthful bids, a finite menu). MMS and EFX are measured with the true valuations, never with the bids. The mechanism's tie-breaking is fixed rather than arbitrary.

A complete development needs basic finite-sum and finite-supremum facts and a proof that the greedy cut covers $M$ with disjoint bundles. The model layer (val, IsEFX, IsPNE over all non-negative bids) is shared with the four sibling missions on Round-Robin and on mechanisms with EFX equilibria. Proofs of any milestone, and of mms_le_average, are welcome.

Selected references

G. Amanatidis, G. Birmpas, F. Fusco, P. Lazos, S. Leonardi, R. Reiffenhäuser, Allocating Indivisible Goods to Strategic Agents: Pure Nash Equilibria and Fairness, Mathematics of Operations Research, 2024; arXiv:2109.08644v2. https://arxiv.org/abs/2109.08644
B. Plaut, T. Roughgarden, Almost Envy-Freeness with General Valuations, SIAM Journal on Discrete Mathematics 34(2), 2020. https://doi.org/10.1137/19M124397X
I. Caragiannis, D. Kurokawa, H. Moulin, A. D. Procaccia, N. Shah, J. Wang, The Unreasonable Fairness of Maximum Nash Welfare, ACM Transactions on Economics and Computation 7(3), 2019. https://doi.org/10.1145/3355902
G. Amanatidis, G. Birmpas, G. Christodoulou, E. Markakis, Truthful Allocation Mechanisms Without Payments: Characterization and Implications on Fairness, EC 2017. https://doi.org/10.1145/3033274.3085147

11 thms2 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Designing Approximately Optimal Search on Matching Platforms 2: Every Set of Assortments Has a Unique Profile of Thresholds Equal to Expected UtilitiesResearch Paper

Motivation

Online matching platforms for dating, freelancing or ride sharing do not match agents themselves. They decide whom each agent gets to see and how often, and the agents then accept or reject. Immorlica, Lucier, Manshadi and Wei (arXiv:2102.09017, Management Science 2023) model this as directed search. The platform designs assortments, which are rates at which types of agents meet, and the agents play an equilibrium of the induced search game. The platform's design problem only makes sense if every choice of assortments leads to a single, well-defined equilibrium outcome. Otherwise "the welfare of an assortment" is not a function of the assortment. This is not automatic: even for simple asymmetric preferences under random meetings, multiple stationary equilibria can arise (Burdett and Coles 1997).

This mission formalizes that well-posedness result, Proposition 3.1(1) of the paper, together with the fixed-point and iteration lemmas of Appendix A.3 and Appendix B.3 on which its proof rests. It is the companion of the mission on the paper's quarter-approximation theorem (Theorem 4.1), which uses the same model.

The source is the arXiv v2 preprint (18 Aug 2021). The Management Science version may number results differently.

Setting

There are finitely many agent types on each side of the market, a set $\mathcal M$ and a set $\mathcal W$ , with $\Theta=\mathcal M\cup\mathcal W$ . Agents of every type leave the market unmatched at a life-event rate $\delta>0$ , and type $\theta$ arrives at rate $\alpha_\theta>0$ . When an agent of type $m$ meets an agent of type $w$ , the pair draws one utility $u\sim F_{mw}$ . Valuations are symmetric: both agents receive $u$ if they match, and $F_{wm}:=F_{mw}$ . Each $F_{mw}$ is a probability law on $\mathbb R$ with no atoms (a "continuous distribution").

An assortment for type $\theta$ is a family of rates $\lambda_\theta(\theta')\ge0$ at which type- $\theta$ agents meet type- $\theta'$ agents on the opposite side. Under a threshold strategy with threshold $\tau_\theta$ , a type- $\theta$ agent accepts a meeting if and only if $u\ge\tau_\theta$ . A meeting turns into a match when both agents accept, i.e. when $u\ge\max(\tau_\theta,\tau_{\theta'})$ . If every type plays a threshold strategy, the expected utility of a type- $\theta$ agent is (equation (5))

\bar u_\theta(\tau)=\frac{\sum_{\theta'}\lambda_\theta(\theta')\int_{\max(\tau_\theta,\tau_{\theta'})}^\infty u\,dF_{\theta\theta'}}{\delta+\sum_{\theta'}\lambda_\theta(\theta')\int_{\max(\tau_\theta,\tau_{\theta'})}^\infty dF_{\theta\theta'}} .

A type's own threshold enters its own utility through $\max(\tau_\theta,\tau_{\theta'})$ .

One type's equation. Fix the thresholds $\tau_i$ of the opposite types. Write $B(t)$ for the right-hand side of (5) with $\tau_\theta$ replaced by $t$ . Lemma A.3 states that $t=B(t)$ has exactly one solution. The best-response map of Appendix A.3 sends a profile $\tau$ to the profile in which each type's new threshold is that solution, computed against the opposite side's thresholds in $\tau$ . A best-response sequence starts at the all-zero profile and applies this map repeatedly.

Formalization targets

Goal: Proposition 3.1, item 1 (fixed-point form)

For any fixed assortments there is exactly one threshold profile $\tau\in\mathbb R^{\mathcal M}\times\mathbb R^{\mathcal W}$ with

\tau_\theta=\bar u_\theta(\tau)\qquad\text{for every }\theta\in\Theta .

Uniqueness ranges over all real profiles.

Milestones

Lemma B.1 (p. 40). With $\lambda_i>0$ and $\tau_i\ge0$ , $\rho=\max_{t\ge0}B(t)$ is attained and satisfies $B(\rho)=\rho$ . $B$ is weakly increasing on $(-\infty,\rho]$ and weakly decreasing on $[\rho,\infty)$ .
Lemma A.3 (p. 35). With $\lambda_i\ge0$ and arbitrary $\tau_i$ , the equation $t=B(t)$ has exactly one real solution.
§A.3, p. 37, first claim. Along a best-response sequence $\tau^{(0)}\equiv0,\tau^{(1)},\dots$ , the odd iterates are weakly decreasing and the even iterates are weakly increasing, componentwise.
§A.3, p. 37, second claim. Every odd iterate dominates every even iterate: $\tau^{(2j)}\le\tau^{(2i+1)}$ .
Proposition A.4 (p. 36). There is a universal $C$ such that $\tau^{(C|\Theta|)}$ is a fixed point of the best-response map, and the sequence is constant from that index on.

Significance

Proposition 3.1 is what makes the platform's problem OptimalDirectedSearch well defined. Assortments determine a unique threshold profile. That profile determines the matching rates (Lemma 3.2) and, through stationarity, the population masses. Welfare is then a function of the assortments, and the program (6) used for Theorem 4.1 encodes exactly this fixed point as its incentive constraint (6e). The constructive proof also yields an algorithm: iterate best responses from zero, and the iteration stops after $O(|\Theta|)$ rounds.

Formalizing it adds three things beyond the paper. First, a checked version of an argument the paper gives informally, including the odd/even sandwich of the iteration, which the paper proves in a few lines. Second, a reusable fixed-point and unimodality lemma for ratios of tail integrals, $B(t)=\int_t^\infty u\,dG\,/\,(\delta+\int_t^\infty dG)$ , which recurs in reservation-value arguments in search theory. Third, an exact accounting of the hypotheses: integrable utilities and the reading of the best-response map. To our knowledge none of these results has been machine-checked.

Difficulty

The obvious route to uniqueness, a contraction argument for the map $\tau\mapsto\bar u(\tau)$ , fails. That map is neither monotone nor contractive in general, since raising a type's own threshold can raise or lower its utility. Existence by Brouwer's fixed-point theorem gives no uniqueness and no algorithm. The best-response iteration does not converge monotonically either: its odd and even iterates move in opposite directions, so convergence in finitely many rounds is a combinatorial statement about the order of the thresholds, not a limit argument. A formal proof also needs continuity and monotonicity of tail integrals of atomless laws, which Mathlib provides only in pieces.

Formalization scope

The two sides are separate finite types M and W. A threshold profile is a pair of functions (M → ℝ) × (W → ℝ), ordered componentwise. A market records $\delta$ , $\alpha$ and the laws F m w : Measure ℝ. The standing assumptions are:

$\delta>0$ ;
$\alpha_\theta>0$ , which is implicit in the paper and stated explicitly;
each $F_{mw}$ is a probability measure with no atoms (NullSingletonClass);
each $F_{mw}$ has an integrable identity. This is implicit in the paper, which uses $\int u\,dF$ as a real number, and is stated explicitly.

Tails are $\int_a^\infty dF=F([a,\infty))$ and $\int_a^\infty u\,dF=\int_{[a,\infty)}u\,dF$ . Capacity (2), flow balance (3) and stationarity (1) are not hypotheses, because Proposition 3.1 holds for any fixed assortments.

The best-response map is encoded as a relation: each new threshold solves its own equation $t=B(t)$ against the opposite side's input thresholds. This is the paper's reading ("This map is a best response by Lemma A.3"). Evaluating (5) at the old profile, own old threshold included, would be a different map. Under that reading finite convergence and the p. 37 claims are false: with one type per side, $\lambda\equiv1$ , $\delta=1$ and $F$ uniform on $[0,1]$ , its iterates are rational and converge only in the limit to $2-\sqrt3$ .

Two formalizations would trivialize the goal, and both are ruled out. Uniqueness is over all real profiles, not only nonnegative ones or those reached by the iteration. The tail integrals are not allowed to vanish by default for non-integrable laws, because integrability is a hypothesis. $O(|\Theta|)$ is encoded with a constant chosen before the market.

Not formalized: the agents' Markov decision process of Appendix A.1. Consequently "this strategy profile is a Nash equilibrium", item 2 of Proposition 3.1, Lemmas A.1–A.2 and the best-response sentences of Lemma A.3 and Proposition A.4 are out of scope.

Contributions welcome: continuity and monotonicity lemmas for $a\mapsto\int_{[a,\infty)}u\,dF$ and $a\mapsto F([a,\infty))$ for atomless integrable laws, which are reusable well beyond this mission, and proofs of the milestones in any order.

Selected references

N. Immorlica, B. Lucier, V. Manshadi, A. Wei, Designing Approximately Optimal Search on Matching Platforms, Management Science, 2023; preprint arXiv:2102.09017v2, 2021. https://arxiv.org/abs/2102.09017
K. Burdett, M. G. Coles, Marriage and Class, Quarterly Journal of Economics 112(1), 1997. https://doi.org/10.1162/003355397555127

8 thms2 active usersReviewed

Completed

Combinatorics Mechanism Design Operations Research·Captain: mikedeng1

Combinatorial Auctions with Interdependent Valuations: SOS to the Rescue 3: The k-HL Mechanism Is Ex-Post IC-IR and a (k+3)-Approximation to Welfare with k Signal ValuesResearch Paper

Motivation

In many auctions a bidder's value for what she wins depends on information held by others. The value of an oil lease, a spectrum licence or a piece of art to one bidder depends on survey data, market forecasts or expert opinions that other bidders hold privately. The model of interdependent values (Milgrom and Weber, 1982) captures this: each agent $i$ holds a private signal $s_i$ , and every agent's value is a publicly known function of the whole signal profile $\mathbf s=(s_1,\dots,s_n)$ .

With interdependent values, maximizing welfare in ex-post equilibrium is impossible unless the valuations satisfy the single-crossing condition (Maskin, 1992; Dasgupta and Maskin, 2000), and even single crossing does not suffice beyond single-item auctions with single-dimensional signals. Without any condition, there are valuations for which no deterministic mechanism achieves a bounded approximation ratio and no randomized mechanism does better than a factor $n$ (Eden, Feldman, Fiat and Goldner, ACM EC 2018; Examples 1.2–1.3 of the source). Eden, Feldman, Fiat, Goldner and Karlin (arXiv:1903.08384v2, 2019) introduce submodularity over signals (SOS): raising one signal increases a value by less when the other signals are higher. They show that SOS valuations admit constant-factor, or signal-space-dependent, approximations in settings where single crossing fails, including combinatorial auctions. This mission formalizes their Theorem 6.1, the case of combinatorial auctions with single-dimensional signals taking $k$ values.

Timeline. Milgrom–Weber (1982) introduce the interdependent values model. Maskin (1992) and Dasgupta–Maskin (2000) show that single crossing makes efficient auctions truthful. Jehiel–Moldovanu (2001) show that efficient implementation fails generically with multidimensional signals. Eden–Feldman–Fiat–Goldner (2018) give approximations under a relaxed, $c$ -single-crossing condition, with ratios depending on $c$ and $n$ . Eden–Feldman–Fiat–Goldner–Karlin (2019; Mathematics of Operations Research, 2024) introduce SOS and prove Theorems 4.1, 5.1, 6.1 and 6.5.

Setting

There are $n$ agents and $m$ items, and $k\ge1$ signal values. Each agent $i$ has a signal $s_i\in\{0,1,\dots,k-1\}$ , and $\{0,\dots,k-1\}^n$ is the grid. Agent $i$ 's value for a bundle $T\subseteq[m]$ at the profile $\mathbf s$ is $v_{iT}(\mathbf s)\ge0$ ; the empty bundle is worth $0$ , and for nonempty $T$ , $v_{iT}$ is weakly increasing in every signal and strictly increasing in $s_i$ . We write $(\mathbf s_{-i},x_i)$ for the profile with agent $i$ 's signal replaced by $x$ , and $(\mathbf s_A,\mathbf 0_B)$ for the profile that keeps the signals of the agents in $A$ and sets those in $B$ to $0$ .

A function $w$ of the profile is SOS if for every coordinate $j$ , all $x,\delta\ge0$ with $x+\delta\le k-1$ , and grid profiles with $\mathbf s'_{-j}\le\mathbf s_{-j}$ coordinatewise,

w(\mathbf s_{-j},x+\delta)-w(\mathbf s_{-j},x)\;\le\;w(\mathbf s'_{-j},x+\delta)-w(\mathbf s'_{-j},x).

The setting is SOS when every $v_{iT}$ is.

A feasible allocation gives disjoint bundles $T_1,\dots,T_n$ ; its welfare at $\mathbf s$ is $\sum_i v_{iT_i}(\mathbf s)$ . A deterministic mechanism maps reported profiles to an allocation and payments. Agent $i$ 's utility is her value, at the true profile, for the bundle she receives at the reported profile, minus her payment. The mechanism is ex-post IC if truthful reporting maximizes each agent's utility whenever the others report truthfully, and ex-post IR if that utility is nonnegative. A randomized mechanism is universally ex-post IC-IR if every deterministic mechanism in its support is.

The mechanism k-HL runs, with probability $p_{RT}=\frac{k-1}{k+3}$ , Random Threshold: choose $\ell$ uniformly in $\{1,\dots,k-1\}$ , call $N_{\ge\ell}=\{i:s_i\ge\ell\}$ the high agents, allocate to them a feasible allocation maximizing $\sum_{i\in N_{\ge\ell}}v_{iS_i}(\mathbf s_{N_{<\ell}},\ell_{N_{\ge\ell}})$ , and charge agent $i$ receiving $\bar T_i$ the price $v_{i\bar T_i}(\mathbf s_{-i},s_i=\ell-1)$ . Otherwise it runs Random Sampling: split the agents uniformly at random into $A$ and $B$ , allocate to $B$ a feasible allocation maximizing $\sum_{i\in B}v_{iS_i}(\mathbf s_A,\mathbf 0_B)$ , and charge nothing. In the Lean development (namespace InterdepSOS.KHL) these are rtAlloc, rtPay, rsAlloc and khlWelfare.

Formalization targets

Goal: Theorem 6.1 (p. 20)

For SOS valuations with $k$ signal values, every Random Threshold component and every Random Sampling component is ex-post IC and IR, and for every grid profile $\mathbf s$ and every feasible allocation $T^*$ ,

\sum_i v_{iT^*_i}(\mathbf s)\;\le\;(k+3)\,\mathbb E\bigl[\text{welfare of k-HL at }\mathbf s\bigr],

where the expectation is over $\ell$ , over $(A,B)$ and over the coin choosing between the two mechanisms, and welfare is measured with true values at the truthful profile.

Milestones

Displays (6)–(7): the welfare of any allocation is at most $\mathsf{OTHER}+\mathsf{SELF}$ , where $\mathsf{OTHER}=\sum_i v_{iT_i}(\mathbf s_{-i},0_i)$ and $\mathsf{SELF}=\sum_{\ell=1}^{k-1}\sum_{i:s_i=\ell}v_{iT_i}(\mathbf 0_{-i},s_i)$ .
Random Sampling is ex-post IC-IR for every partition.
Random Threshold is ex-post IC-IR for every threshold.
Lemma 6.2: $\mathsf{SELF}\le(k-1)\,\mathbb E[\text{welfare of Random Threshold}]$ .
Lemma 6.3: $\mathsf{OTHER}\le4\,\mathbb E[\text{welfare of Random Sampling}]$ .

Significance

Theorem 6.1 is the paper's answer for general combinatorial auctions with single-dimensional signals and arbitrary bundle valuations, a setting where single crossing gives nothing and where the random-sampling technique of the single-parameter case (Theorem 4.1) is not enough on its own: Random Sampling alone covers only the contribution of the other agents' signals. The ratio $k+3$ depends on the size of the signal space but not on the number of agents or items. The same decomposition, with Random Threshold replaced by a bucketing mechanism, yields the $(2\log_2k+4)$ -approximation for strong-SOS valuations (Theorem 6.5), so milestones 1 and 5 are shared by both results.

The result is proved in the paper; no machine-checked version is known to exist. A formalization fixes the incentive argument precisely (which data the allocation may depend on, how ties are broken) and makes the uniform averages over thresholds and partitions explicit. The development reuses the Key Lemma 3.1 of the paper, which is posed in a sibling mission of this series.

Difficulty

Two points resist a direct argument. First, incentive compatibility of Random Threshold requires that a high agent who changes her report within $\{\ell,\dots,k-1\}$ leaves the allocation unchanged, and this is true only if the argmax rule sees the reports through the proxy data $(\mathbf s_{N_{<\ell}},\ell_{N_{\ge\ell}})$ alone: an argmax rule that breaks ties using the full report profile can make a high agent's bundle, and hence her utility, depend on her report. The formalization must therefore state precisely what the allocation rule may depend on. Second, the welfare bound for Random Sampling rests on the Key Lemma 3.1 (zeroing a uniformly random half of the other signals keeps, in expectation, half of an SOS value), which here has to hold on the discrete grid $\{0,\dots,k-1\}^n$ , with SOS assumed only there; the expectations over partitions and thresholds are finite averages whose bookkeeping (agents in $A$ receive nothing, agents outside $N_{\ge\ell}$ receive nothing) must match the mechanism exactly.

Formalization scope

Agents are Fin n, items Fin m, bundles Finset (Fin m), signals natural numbers with the grid condition InGrid k s. All hypotheses on valuations (nonnegativity, monotonicity, strict monotonicity in the own signal, SOS) are imposed on grid profiles only, with the shifted coordinate staying below $k$ ; a condition on all of $\mathbb N^n$ would be stronger than the paper's. The empty bundle is worth $0$ and the monotonicity clauses concern nonempty bundles. Allocations are maps Fin n → Finset (Fin m) with pairwise disjoint values; agents outside the eligible set receive $\emptyset$ .

The argmax allocations are produced by arbitrary selectors, functions of the threshold (or of $B$ ) and of the proxy profile, required to return a feasible maximizer of the proxy welfare; the theorems quantify over all such selectors. Expectations are finite uniform averages, $\frac1{k-1}\sum_{\ell=1}^{k-1}$ and $2^{-n}\sum_{B\subseteq[n]}$ , never an existential or universal quantifier over $\ell$ or $B$ . The ratio is stated against every feasible allocation, with welfare at true values, never with proxy values and never through a supremum. IC and IR are stated for every component of the mixture, with the paper's explicit payments. Random Sampling zeroes the signals of all of $B$ , the agent's own included (the page's " $v_{ij}(\mathbf s_A,\mathbf 0_B)$ " is read as $v_{iT}(\mathbf s_A,\mathbf 0_B)$ ). For $k=1$ , $p_{RT}=0$ and the threshold average is the empty sum.

Lemmas 6.2 and 6.3 and displays (6)–(7) are stated for every feasible allocation (every assignment, for (6)–(7)), which is stronger than the paper's statements for a welfare-maximizing $T^*$ .

Needed infrastructure: the Key Lemma 3.1 on the discrete grid, finite averages over subsets, and a lemma that a maximizer over a subfamily of allocations dominates any restriction of a feasible allocation. Contributions of proofs of the milestones in any order are welcome; the IC-IR milestones are independent of the welfare milestones.

The source is the arXiv preprint arXiv:1903.08384v2; the Mathematics of Operations Research (2024) version is not the cited source, and its numbering may differ.

Selected references

A. Eden, M. Feldman, A. Fiat, K. Goldner, A. R. Karlin, Combinatorial Auctions with Interdependent Valuations: SOS to the Rescue, arXiv:1903.08384v2, 2019. https://arxiv.org/abs/1903.08384v2
A. Eden, M. Feldman, A. Fiat, K. Goldner, Interdependent Values without Single-Crossing, ACM EC 2018 (cited as [Eden et al., 2018] in the source).
E. Maskin, Auctions and Privatization, in H. Siebert (ed.), Privatization, 1992 (cited as [Maskin, 1992] in the source).
P. Milgrom, R. Weber, A Theory of Auctions and Competitive Bidding, Econometrica 50(5), 1982. https://doi.org/10.2307/1911865
P. Dasgupta, E. Maskin, Efficient Auctions, Quarterly Journal of Economics 115(2), 2000. https://doi.org/10.1162/003355300554737
P. Jehiel, B. Moldovanu, Efficient Design with Interdependent Valuations, Econometrica 69(5), 2001. https://doi.org/10.1111/1468-0262.00248

9 thms2 active usersReviewed

Economics·Captain: mikedeng1

Online Advertising, Data Sharing, and Consumer Control 3: Under Topics-Style Category Tracking Both Advertisers Bid on ADX1 Exactly When the Inaccuracy τ Is Below an Explicit Threshold τ̃ > 1Research Paper

Motivation

Online display advertising is sold through ad exchanges, and much of its value comes from targeting: showing an ad to consumers known to be interested in the advertised product. For two decades the main tracking technology was the third-party cookie, under which an exchange can follow a consumer only after an advertiser agrees to share the data from its own website. Google's proposed replacement for Chrome, the Topics system, instead lets the browser itself assign consumers to interest categories. Advertisers no longer control that data, and the categories are coarse, so some ads reach consumers who are not interested.

Johnson, Jungbauer and Preuss (SSRN 3898798, Nov. 2022; published in Management Science, 2024, doi:10.1287/mnsc.2022.03385) study how data sharing and consumer control shape competition between ad exchanges. Their §3 adds a Topics-style category system to the base model and asks when advertisers use it, and how the exchange that runs it profits from its accuracy. This mission formalizes that section.

Setting

There are two advertisers $A_1, A_2$ and two exchanges. ADX1 runs the Topics system. It reaches all $1+\eta_2$ consumers interested in the product category, but reaching a mass one of them takes $\tau>1$ ad impressions; $\tau$ is the system's inaccuracy. ADX2 offers retargeting through another technology. An advertiser bidding there reaches a fraction $\sigma$ of the $1-\alpha$ consumers who recently visited its own website. An impression costs $w$ . A consumer reached by a single advertiser is worth the monopoly profit $M$ , and one reached by both is worth the competition profit $C$ . The parameters satisfy

0<\alpha<\tfrac12,\qquad 0<w<C<M<2C,\qquad 0<\varphi<1,\qquad \eta_2>0,\qquad \tau>1,\qquad 0\le\sigma<1,

where $\varphi$ is the share of the ad price an exchange keeps.

The advertisers bid simultaneously, each on one exchange. Write $\pi(x,y)$ for the profit of an advertiser on exchange $x$ when its rival is on $y$ (p. 17):

\pi(1,1)=(1+\eta_2)(C-\tau w),\qquad \pi(2,2)=\sigma[\alpha M+(1-2\alpha)C-(1-\alpha)w],

\pi(1,2)=(1+\eta_2)M-\sigma(1-\alpha)(M-C)-(1+\eta_2)\tau w,\qquad \pi(2,1)=\sigma(1-\alpha)(C-w).

An equilibrium is a pure Nash equilibrium of this symmetric $2\times2$ game. ADX1's revenue is $\varphi w$ per impression sold on it, and an advertiser bidding on ADX1 buys $\tau(1+\eta_2)$ impressions. The proof of the main result uses the thresholds

w_1=\frac{(1+\eta_2)-\sigma(1-\alpha)}{\tau(1+\eta_2)-\sigma(1-\alpha)}\,C,\qquad w_2=\frac{[(1+\eta_2)-\sigma]M+\alpha\sigma C}{\tau(1+\eta_2)-\sigma(1-\alpha)},

and the accuracy threshold

\tilde\tau=\frac{(1+\eta_2)-\sigma(1-\alpha)}{w(1+\eta_2)}\,C+\frac{\sigma(1-\alpha)}{1+\eta_2}.

In Lean these objects are Params, Params.Standing, payoff, IsNE, revenue, w₁, w₂ and tauTilde, in the namespace AdDataSharing.Topics.

Formalization targets

Goal: Proposition 5 (threshold corrected)

\tilde\tau>1\quad\text{and}\quad\Big[(1,1)\text{ is the unique equilibrium}\iff \tau<\tilde\tau\Big].

Bidding on ADX1 means cross-targeting the rival's visitors, which Topics cannot avoid. The goal therefore says that both advertisers cross-target exactly when the system is not too inaccurate, and that this region is never empty.

Milestones

$(1,1)$ is an equilibrium $\iff w\le w_1\iff \tau\le\tilde\tau$ (proof of Proposition 5, p. 29).
$(2,2)$ is an equilibrium $\iff w\ge w_2$ (pp. 29–30).
Each asymmetric profile is an equilibrium $\iff w_1\le w\le w_2$ (p. 30).
$w_1<w_2$ (p. 30).
$\tilde\tau>1$ (p. 30).
Proposition 7 (i): for $\tau<\tau'<\tilde\tau$ , ADX1's equilibrium revenue at $\tau'$ strictly exceeds that at $\tau$ (p. 19).
Proposition 7 (ii): $\tilde\tau$ is strictly decreasing in $\sigma$ (p. 19).
Corollary 2: above some $\bar\tau$ the game has an equilibrium, and ADX1's revenue in every equilibrium is strictly below its revenue in every equilibrium of the base game of §1 without Topics (p. 19).

Significance

Proposition 5 is the entry point of the paper's Topics analysis. It identifies when a category-based system is actually used, and it implies that removing advertisers' property rights over their data leads to more information being shared about consumers' purchase interests. Proposition 7 adds an incentive result: inside the region of use, the exchange running Topics gains from making it less accurate, because inaccuracy sells more impressions. A weaker rival exchange widens that region. Corollary 2 adds a regulatory point: a privacy rule that sets a high minimum inaccuracy can lead the exchange not to introduce the system at all. Corollary 2 compares against ADX1's equilibrium revenue in the base game of §1, which mission 1 of this series formalizes; its definitions are shared with this mission.

The results are proved in the paper, and none of them has a machine-checked proof. Formalizing them also corrects the printed statement. Display (6) on p. 17 omits a factor $1/(1+\eta_2)$ , and with the printed threshold the equivalence of Proposition 5 is false. The mission states the threshold that the page's own deviation condition gives.

Difficulty

The algebra is elementary, and the care lies in the equilibrium bookkeeping. "In the equilibrium both advertisers bid on ADX1" is a uniqueness claim. At $\tau=\tilde\tau$ the profile $(1,1)$ is still an equilibrium, but the asymmetric profiles are equilibria too. A proof that only checks deviations from $(1,1)$ therefore gets the wrong boundary. A proof also has to rule out every other profile, using $w_1<w_2$ and the signs of the denominators. Each threshold is a quotient, and its denominator $\tau(1+\eta_2)-\sigma(1-\alpha)$ is positive only because $\tau>1>\sigma$ . Proposition 7 (i) compares two different games, and Corollary 2 needs equilibrium existence together with a threshold that is uniform in the profile.

Formalization scope

All quantities are real. The game is the platform's general two-player pure Nash equilibrium CompetingChains.Cournot.IsPureNash, which this mission references, applied with payoffs $\pi(x,y)$ and $\pi(y,x)$ . There is no contracting stage and no equilibrium selection, as footnote 22 of the paper states. Deviation inequalities are weak, so the exact conditions read $w\le w_1$ and $w\ge w_2$ where the proof writes strict inequalities as sufficient conditions.

Three assumptions are added relative to §3, and each is disclosed. $C>w$ is used throughout the paper and stated on p. 21. $\sigma\ge0$ is the reading of "a fraction $\sigma<1$ ". $\eta_2>0$ comes from the base model, where it reads $\eta_2>\eta_1>0$ . The inequalities $2C>M$ and $\varphi<1$ are kept as paper assumptions; they are inert here. Divisions outside the standing assumptions return Lean's junk value $0$ , and every theorem assumes the standing assumptions.

Several formalizations would trivialize the targets, and none is used. "Both advertisers bid on ADX1" is defined through IsNE and uniqueness, not as an inequality on payoff numbers. The printed threshold (6) is never posed. Statements quantifying over all equilibria also assert that an equilibrium exists, so they cannot hold vacuously. All definitions are local to this mission except the referenced Nash equilibrium notion. Contributions are welcome on any milestone, and a reusable lemma characterizing pure equilibria of $2\times2$ symmetric games would serve all of them.

Selected references

J. P. Johnson, T. Jungbauer, M. Preuss, Online Advertising, Data Sharing, and Consumer Control, SSRN working paper 3898798, version of November 2, 2022. https://ssrn.com/abstract=3898798
J. P. Johnson, T. Jungbauer, M. Preuss, Online Advertising, Data Sharing, and Consumer Control, Management Science, 2024. https://doi.org/10.1287/mnsc.2022.03385

12 thms2 active usersReviewed

Economics Operations Research·Captain: mikedeng1

Sharing Sequentially Triggered Losses: Automated Conflict Resolution Through Smart Contracts 3: The Midpoint Fixed-Fraction Rule Is the Shapley Value and the Nucleolus of the Liability GameResearch Paper

Motivation

When one breached contract forces the next party to breach its own contract, a single failure travels down a loss chain: agent 1 (the initiator) causes a loss $\ell_1$ to agent 2, which can then no longer honour its agreement with agent 3 and causes it a loss $\ell_2$ , and so on until agent $n$ causes a loss $\ell_n$ to a final victim. Gudmundsson, Hougaard and Ko (Management Science 70(3), 2024) ask how the total loss should be shared among the agents of the chain, with the aim of encoding the answer in a smart contract that settles such disputes automatically.

Their central rules are the fixed-fraction rules $\varphi^\lambda$ , under which every agent pays a fixed fraction $\lambda$ of the loss it caused and the initiator also pays the remaining fraction $1-\lambda$ of the total. An axiomatic characterization (their Theorem 1) singles out the whole family $\lambda\in[0,1]$ but not a particular member. This mission formalizes the paper's game-theoretic argument for the midpoint $\lambda=1/2$ : the cooperative game that records which coalitions are liable for which losses has the midpoint allocation as both its Shapley value and its nucleolus, the two best-known single-valued solutions of cooperative game theory.

Setting

Agents are $N=\{1,\dots,n\}$ with $n\ge1$ . A loss problem is a vector $\ell=(\ell_1,\dots,\ell_n)\in\mathcal L^n=\mathbb R^n_{\ge0}$ , where $\ell_i$ is the loss agent $i$ causes to agent $i+1$ ; the total loss is $L=\ell_1+\dots+\ell_n$ . The fixed-fraction rule with parameter $\lambda$ assigns

\varphi^\lambda_1(\ell)=\lambda\ell_1+(1-\lambda)L,\qquad \varphi^\lambda_i(\ell)=\lambda\ell_i\ (i\ge2).

A transferable-utility game on $N$ is a function $v$ assigning a real number to every coalition $S\subseteq N$ . The liability game of $\ell$ is

v_\ell(S)=\begin{cases}\sum_{i\in S}\ell_i&\text{if }1\in S,\\0&\text{otherwise:}\end{cases}

a coalition is liable for the losses its members caused only if it contains the initiator, without whom no loss would have occurred. The contribution of player $i$ to the grand coalition is $M_i(v)=v(N)-v(N\setminus\{i\})$ .

Two solution concepts are compared with $\varphi^{1/2}(\ell)$ .

The Shapley value gives player $i$

\mathrm{Sh}_i(v)=\sum_{S\subseteq N\setminus\{i\}}\frac{|S|!\,(n-|S|-1)!}{n!}\bigl(v(S\cup\{i\})-v(S)\bigr).

An imputation is a vector $x$ with $\sum_{i\in N}x_i=v(N)$ and $x_i\ge v(\{i\})$ for all $i$ . The excess of $S$ at $x$ is $e(S,x)=v(S)-\sum_{i\in S}x_i$ , and the excess vector $\theta(x)$ lists the $2^n$ excesses in non-increasing order. The nucleolus $\nu(v)$ (Schmeidler 1969) is the imputation whose excess vector is lexicographically smallest.

A game is convex if $v(\emptyset)=0$ and $v(S)+v(T)\le v(S\cup T)+v(S\cap T)$ for all $S,T$ .

Formalization targets

Goal: Theorem 3 (p. 15)

For every $\ell\in\mathcal L^n$ ,

\mathrm{Sh}(v_\ell)=\varphi^{1/2}(\ell)\qquad\text{and}\qquad \nu(v_\ell)=\varphi^{1/2}(\ell),

where the second identity is stated as: $\varphi^{1/2}(\ell)$ is an imputation of $v_\ell$ with lexicographically minimal sorted excess vector, and every imputation with this property equals $\varphi^{1/2}(\ell)$ .

Milestones (Appendix A, proof of Theorem 3, p. 24)

$v_\ell$ is convex.
(§4.2, p. 15; referenced, already on the platform) the core of a convex game is non-empty and contains its Shapley value, which applies to $v_\ell$ by milestone 1.
$M_1(v_\ell)=L$ and $M_i(v_\ell)=\ell_i$ for $i\ne1$ .
Every nucleolus $\nu$ of $v_\ell$ satisfies $\nu_i=M_i(v_\ell)/2=\ell_i/2=\varphi^{1/2}_i(\ell)$ for $i\ne1$ , and $\nu_1=\varphi^{1/2}_1(\ell)$ .
The Shapley value of $v_\ell$ is a nucleolus of $v_\ell$ .

Significance

The result. Theorem 1 of the paper leaves a one-parameter family of rules, and a designer who writes the rule into a contract must still choose $\lambda$ . Theorem 3 gives a reason for $\lambda=1/2$ that does not depend on the axioms: if losses are treated as the worth of coalitions, two solution concepts that are built on unrelated principles (average marginal contributions on one side, lexicographic minimization of complaints on the other) both return $\varphi^{1/2}(\ell)$ . Together with the paper's Theorem 2 (equidistance from ideal allocations, a separate mission of this series) it makes the midpoint the paper's recommended rule.

Formalizing it. The paper proves Theorem 3 by citing two results of Muto, Nakayama, Potters and Tijs (1988) on big boss games, the nucleolus formula (their Theorem 4.2) and the coincidence of Shapley value and nucleolus for convex big boss games (their Theorem 4.5); the paper itself proves only convexity and the marginal contributions. A formal proof must therefore establish the nucleolus of $v_\ell$ directly from Schmeidler's lexicographic definition. No nucleolus definition exists on the platform (searched 2026-10-14), and this mission introduces one. The Shapley value and convex games are reused from the platform's published definitions, and the core-contains-the-Shapley-value theorem for convex games is already proved there.

Difficulty

Convexity and the marginal contributions are finite case analyses. The Shapley identity is a weighted sum over all coalitions not containing a player and needs the combinatorial identities behind the weights; for $v_\ell$ only the position of the initiator relative to $S$ matters.

The substantive part is the nucleolus. Its definition compares sorted vectors of $2^n$ excesses, so an argument cannot treat one coalition at a time: showing that a candidate is lexicographically minimal requires controlling how a change of the payoff vector permutes the order of all excesses. The obvious first idea, minimizing only the largest excess (the least core), generally leaves a set of imputations rather than a point, so the comparison must go down the whole sorted list. Coalitions whose excesses tie, which happens for instance when some $\ell_i=0$ , are where informal arguments about sorted excess vectors are usually loose, and a formal proof has to handle them.

Formalization scope

Agents are Fin n with the initiator at index 0; [NeZero n] encodes $n\ge1$ , which the paper assumes because $1\in N$ . Loss vectors are Fin n → ℝ with the hypothesis IsLoss ℓ ( $\ell_i\ge0$ ).
A game is Finset (Fin n) → ℝ. The Shapley value is the published Supermodularity.Cooperative.ShapleyValue and convexity the published Supermodularity.Cooperative.IsConvexGame (the supermodular form, equivalent to the increasing-marginal-contribution form used on p. 24).
The nucleolus is defined in the mission's Nucleolus file: imputations with efficiency and individual rationality, excess $v(S)-\sum_{i\in S}x_i$ over all $2^n$ coalitions including $\emptyset$ and $N$ , sorted by ≥ into a list, and compared with List.Lex (· < ·). Including $\emptyset$ and $N$ does not change the order, since their excess is $0$ at every imputation.
The goal states both identities. The nucleolus half is not replaced by membership in the core or by minimality of the largest excess, the minimization runs over imputations and not over all of $\mathbb R^n$ , and uniqueness is stated explicitly rather than taken from Schmeidler's theorem.
The paper never defines the nucleolus or the Shapley value; the standard definitions (Schmeidler 1969; Shapley 1953) are used.

Contributions welcome: proofs of the milestones; general lemmas on sorted excess vectors (e.g. Kohlberg-type criteria for the nucleolus), which are reusable for every later nucleolus result; Schmeidler's existence and uniqueness theorem; and the general big boss game results of Muto et al. (1988).

Selected references

J. Gudmundsson, J. L. Hougaard, C. Y. Ko, Sharing Sequentially Triggered Losses: Automated Conflict Resolution Through Smart Contracts, Management Science 70(3):1773–1786, 2024 (accepted manuscript, 2023). https://doi.org/10.1287/mnsc.2023.4772
S. Muto, M. Nakayama, J. Potters, S. Tijs, On big boss games, The Economic Studies Quarterly 39(4):303–321, 1988. https://doi.org/10.11398/economics1986.39.303
D. Schmeidler, The nucleolus of a characteristic function game, SIAM Journal on Applied Mathematics 17(6):1163–1170, 1969. https://doi.org/10.1137/0117107
L. S. Shapley, A value for n-person games, in Contributions to the Theory of Games II, Annals of Mathematics Studies 28, Princeton University Press, 1953, pp. 307–317. https://doi.org/10.1515/9781400881970-018
L. S. Shapley, Cores of convex games, International Journal of Game Theory 1:11–26, 1971. https://doi.org/10.1007/BF01753431

13 thms2 active usersReviewed

Completed

Economics·Captain: mikedeng1

Sharing Sequentially Triggered Losses: Automated Conflict Resolution Through Smart Contracts 2: For Equal Losses the Midpoint Fixed-Fraction Rule Is Equidistant from All Ideal AllocationsResearch Paper

Motivation

When a contract breach propagates along a supply chain, one failure triggers the next: a supplier delivers late, the manufacturer misses its own delivery, the distributor misses its, and so on. Each link suffers a loss caused by its predecessor, and the question is who should be liable for what. Gudmundsson, Hougaard and Ko (Management Science 70(3), 2024) study this as an axiomatic cost-sharing problem, with the aim of rules simple enough to be executed automatically by a smart contract.

Their first main result characterizes a one-parameter family, the fixed-fraction rules $\varphi^\lambda$ , $\lambda\in[0,1]$ , by four axioms. The axioms do not single out a member of the family. Section 4 of the paper gives two normative arguments for the midpoint $\lambda=1/2$ . This mission formalizes the first of them, Theorem 2: for loss chains with equal losses, $\varphi^{1/2}$ is the allocation at equal Euclidean distance from every agent's "ideal" allocation. The construction follows the tradition of ideal points in bankruptcy, taxation and bargaining (Yu 1973; Chun 1988), with one ideal allocation per agent instead of a single ideal point.

Setting

There are $n\ge 1$ agents $1,\dots,n$ in a chain. Agent $i$ causes a loss $\ell_i\ge 0$ to agent $i+1$ ; a loss problem is $\ell=(\ell_1,\dots,\ell_n)\in L^n=\mathbb R^n_{\ge 0}$ , with total loss $L=\ell_1+\dots+\ell_n$ .

An allocation of $\ell$ is a vector $x\in\mathbb R^n$ of liabilities with $x_i\ge 0$ , with $x_1+\dots+x_m\ge \ell_1+\dots+\ell_m$ for $m=1,\dots,n-1$ (no initial segment of the chain pays less than the losses it caused), and with $x_1+\dots+x_n=L$ . The set of allocations is $X(\ell)$ , and the ordered allocations are $\bar X(\ell)=\{x\in X(\ell)\mid x_1\ge\dots\ge x_n\}$ .

The fixed-fraction rule with parameter $\lambda$ (Definition 1) is

\varphi^\lambda_1(\ell)=\lambda\ell_1+(1-\lambda)L,\qquad \varphi^\lambda_i(\ell)=\lambda\ell_i\quad (i\ge 2).

Each agent pays the fraction $\lambda$ of the loss it caused directly, and the initiator also pays the residual $(1-\lambda)L$ .

For $k=1,\dots,n$ the ideal allocation $c_k$ charges the first $k$ agents equally and the rest nothing:

c_k=\Big(\tfrac Lk,\dots,\tfrac Lk,0,\dots,0\Big)\qquad(k\text{ entries equal to }L/k).

When $\ell_1=\dots=\ell_n$ , $c_1=(L,0,\dots,0)$ is the allocation agent 2 would prefer among the ordered allocations, $c_{k-1}$ is the one agent $k$ would prefer, and $c_n=\ell$ is agent 1's. Distances are Euclidean: $d(x,y)=\big(\sum_i (x_i-y_i)^2\big)^{1/2}$ .

Formalization targets

Goal: Theorem 2 (p. 14)

For every $n\ge 1$ and $\ell\in L^n$ with $\ell_1=\dots=\ell_n$ ,

d\big(\varphi^{1/2}(\ell),c_k\big)=d\big(\varphi^{1/2}(\ell),c_{k'}\big)\qquad\text{for all }k,k'\in\{1,\dots,n\}.

Milestones (proof of Theorem 2, Appendix A, pp. 23–24)

For every $x\in\mathbb R^n$ and $1\le k\le n$ ,

d(x,c_k)^2=\sum_{i=1}^n x_i^2-\frac{2L}{k}\sum_{i=1}^k x_i+\frac{L^2}{k}.

If $L\neq 0$ , then $x$ is equidistant from $c_1,\dots,c_n$ if and only if there is $\alpha\in\mathbb R$ with $\sum_{i=1}^k x_i-L/2=\alpha k$ for $k=1,\dots,n$ .
If $x_1+\dots+x_n=L$ and the prefix system of milestone 2 holds, then $\alpha=L/(2n)$ , and for equal losses $x=\varphi^{1/2}(\ell)$ .

Companions (§4.1, p. 14)

Uniqueness: for equal losses, $\varphi^{1/2}(\ell)$ is the only allocation in $X(\ell)$ equidistant from $c_1,\dots,c_n$ .
Geometry: for equal losses, $\bar X(\ell)=\operatorname{conv}\{c_1,\dots,c_n\}$ .

Significance

Theorem 2 is one of the two arguments the paper gives for recommending $\varphi^{1/2}$ among the fixed-fraction rules; the other is that $\varphi^{1/2}$ is the Shapley value and the nucleolus of the associated liability game (Theorem 3, a separate mission of this series). The uniqueness companion turns the theorem into a selection principle: equalizing distances to ideal allocations determines the allocation completely. The paper also remarks that the same principle, applied to the elementary problems with unit-vector ideal allocations, selects the serial rule, which shows that the choice of ideal allocations drives the result.

The result is proved in the paper; to the best of our knowledge it has no machine-checked proof. The mission produces a formal model of loss chains, allocations and fixed-fraction rules on which the other missions of the series also build, and a checked version of the paper's computation, including the boundary cases ( $L=0$ , $n=1$ ) that the printed proof passes over.

Difficulty

The theorem is a computation, and the obstacles are the ones a careful formalization has to face rather than conceptual ones. The squared distance to $c_k$ splits into a part common to all $k$ and a part linear in the prefix sum $\sum_{i\le k}x_i$ , and the printed argument passes between the two forms by dividing by $L$ , which is not allowed for the zero problem. The uniqueness statement must also hold at $L=0$ , where every ideal allocation is the zero vector and the prefix characterization breaks down. Prefix sums over $\{1,\dots,k\}$ must be matched exactly with the $k$ nonzero coordinates of $c_k$ ; an off-by-one in either produces a different family of points. Finally, the equal-loss hypothesis cannot be dropped: for $\ell=(1,0)$ , $\varphi^{1/2}(\ell)=(1,0)=c_1$ , at distance $0$ from $c_1$ and $\sqrt{1/2}$ from $c_2$ .

Formalization scope

Agents are indexed $0,\dots,n-1$ in Lean (the paper's agent $i$ is index $i-1$ ), vectors are functions Fin n → ℝ, and nonnegativity of a loss vector is the predicate IsLoss. The fixed-fraction rule is a function of $\lambda$ , $n$ and $\ell$ ; $\lambda$ is named lam. The ideal allocation ideal ℓ k is defined for every natural $k$ but is used only for $1\le k\le n$ ; every statement quantifies over exactly that range, because ideal ℓ 0 is the zero vector in Lean and is not one of the paper's points. Distances are Mathlib's distance on EuclideanSpace ℝ (Fin n); the sup distance on Fin n → ℝ is not used, and would not even be detected by the Figure 1 example, where the sup distances to $c_1,c_2,c_3$ are also all equal.

Disclosed additions and corrections:

$n\ge 1$ in the goal, in milestone 3 and in the companions (the paper's $\mathbb N$ starts at $1$ ; at $n=0$ the convex-hull companion would be false and milestone 3's $\alpha$ undetermined).
$L\neq 0$ in milestone 2, where the paper divides by $L$ ; the equivalence is false at $L=0$ .
Milestone 3 uses $x_1+\dots+x_n=L$ where the page prints " $=1$ ".
Milestones 1 and 2 are stated for every $x\in\mathbb R^n$ ; the paper writes them for $x\in\bar X(\ell)$ but does not use that restriction.

A formalization that states the conclusion with the sup metric, that ranges $k$ over $0,\dots,n$ or $0,\dots,n-1$ , or that drops the equal-loss hypothesis does not formalize Theorem 2. Contributions of proofs of any item are welcome; milestone 1 is a finite-sum computation reusable for any distance-to-ideal-point argument in this setting.

Selected references

J. Gudmundsson, J. L. Hougaard, C. Y. Ko, Sharing Sequentially Triggered Losses: Automated Conflict Resolution Through Smart Contracts, Management Science 70(3), 1773–1786, 2024. https://doi.org/10.1287/mnsc.2023.4772 (formalized from the authors' accepted manuscript, 2023).
P. L. Yu, A class of solutions for group decision problems, Management Science 19, 936–946, 1973. https://doi.org/10.1287/mnsc.19.8.936
Y. Chun, The equal-loss principle for bargaining problems, Economics Letters 26, 103–106, 1988. https://doi.org/10.1016/0165-1765(88)90022-5
B.-G. Ju, J. D. Moreno-Ternero, Fair allocation of disputed properties, International Economic Review 58, 1279–1301, 2017. https://doi.org/10.1111/iere.12251

6 thms2 active usersReviewed

Economics Operations Research Optimization·Captain: mikedeng1

Marketplace Leakage 3: The Marketplace Bans Buyer–Seller Communication Above Π/(v − c), Below η_L When q > c/(v − Π), and Always When q Is Close to OneResearch Paper

Motivation

Online marketplaces match buyers with sellers and charge a fee per transaction. Once a buyer has found a seller on the platform, both have an incentive to complete the sale off the platform and split the fee they save. This leakage (also called disintermediation) is a central concern for service marketplaces such as Upwork, Thumbtack or AngelList, and several of them respond by hiding the identity of the parties and blocking direct messages until a transaction is committed.

A. Hagiu and J. Wright, Marketplace Leakage (Management Science, 2023; doi:10.1287/mnsc.2023.4757), build a model of a marketplace that cannot prevent leakage by contract and study six strategies against it. Section 5.2 studies the bluntest of them: banning buyer–seller communication. A ban stops leakage, but it also prevents buyers from learning whether the product suits them. Proposition 3 says exactly when the marketplace gains from the ban. This mission formalizes that proposition and the lemmas of its proof (Appendix §8.4).

Setting

There is one marketplace $M$ , one seller $S$ and a unit mass of buyers with unit demand. The product has value $v$ for buyers who want it and marginal cost $c<v$ ; the outside option is worth $0$ .

Allowing communication (the baseline). $M$ sets a fee $f$ per transaction. $S$ sets the on-platform price $p_m=v$ and a direct price $p_d\le v$ . A buyer who buys directly bears a switching cost $s$ with distribution $G$ ; with the uniform distribution of the paper,

G(s)=\min\{\max\{s/\mu,0\},1\},\qquad \mu>0 .

The seller maximizes its profit (1),

\pi(p_d)=(p_d-c)\,G(v-p_d)+(v-c-f)\,\bigl(1-G(v-p_d)\bigr),

and $M$ earns $f\,(1-G(v-p_d))$ , choosing $f\le v-c$ . The equilibrium profit of $M$ is $\Pi^*$ . With communication allowed, a buyer values the product at $v$ only with probability $q\in(0,1)$ , but learns their valuation; every payoff is multiplied by $q$ , so $M$ earns $q\Pi^*$ .

Banning communication. Under a ban there is no leakage, but a buyer learns their valuation only with probability $\eta\in[0,1]$ . Facing the fee $f$ , the seller has two options: the high price $p_m=v$ , selling to the fraction $\eta q$ of informed high-value buyers and earning $\eta q\,(v-c-f)$ ; and the low price $p_m=qv$ , selling also to the $1-\eta$ uninformed buyers and earning $(1-\eta+\eta q)(qv-c-f)$ . It takes the better option (ties to the low price) and lists if that option pays at least $0$ . $M$ earns $f$ per transaction and chooses $f\in\mathbb R$ . Its maximal revenue is the ban value $V(\eta)$ . Two closed forms appear:

\Pi_H(\eta)=\eta q(v-c),\qquad \Pi_L(\eta)=(1-\eta+\eta q)\Bigl(\frac{(1-(2-q)\eta)qv}{1-\eta}-c\Bigr).

$M$ prefers to ban if $V(\eta)>q\Pi^*$ and prefers to allow if $V(\eta)<q\Pi^*$ .

Formalization targets

Goal: Proposition 3 (pp. 15–16)

For $0<\Pi^*<v-c$ :

$M$ prefers to ban for every $\eta$ with $\Pi^*/(v-c)<\eta\le 1$ ;
if $q>c/(v-\Pi^*)$ , there is a unique $\eta_L\in[0,1)$ with $\Pi_L(\eta_L)=q\Pi^*$ , it is positive, and $M$ prefers to ban for every $\eta\in[0,\eta_L)$ ;
there is $q_0<1$ such that for $q\in(q_0,1)$ , $M$ prefers to ban for every $\eta\in[0,1]$ ;
with uniform switching costs, $c\ge 0$ , and $\Pi^*=\Pi^*(\mu)$ the baseline equilibrium profit: for each $\eta\in(0,1)$ , $M$ prefers to ban for all sufficiently small $\mu>0$ and prefers to allow for all sufficiently large $\mu$ .

Milestones

f>\frac{(1-(2-q)\eta)qv}{1-\eta}-c\iff \text{the seller prefers the high price}\qquad(\text{p. 15})

V(\eta)=\max\{\Pi_H(\eta),\Pi_L(\eta)\}\qquad(\text{p. 15})

\frac{d\Pi_L}{d\eta}=-\frac{(1-q)qv}{(1-\eta)^2}\bigl((2-\eta)q\eta+2(1-\eta)^2\bigr)+c(1-q)<0\ \text{ when } qv>c\qquad(\text{p. 38})

\Pi_L(\eta)\le\Pi_H(\eta)\iff\eta\ge\eta^*,\quad \eta^*=\frac{qv(2-q)-c-q\sqrt{(1-q)v(v-c)}}{qv(3(1-q)+q^2)-c}\in(0,1)\qquad(\text{p. 38})

\lim_{q\to1^-}\eta^*=1\qquad(\text{p. 38})

Significance

The proposition separates three regimes. When information loss is small ( $\eta$ near $1$ ) a ban costs almost nothing and removes leakage, so the marketplace bans. When information loss is large and buyers are a priori likely to value the product, the marketplace can induce the low price $qv$ and sell to everyone, so a ban pays again. In between, allowing communication can win. With uniform switching costs, the comparison turns on how much leakage costs: when switching is cheap (small $\mu$ ) the baseline profit $\mu/2$ is small and the ban wins; when it is expensive, leakage is rare and allowing communication wins. The result is proved in the paper by an informal appendix argument. No part of it has been machine-checked. A formal version pins down what the paper leaves implicit: the seller's tie-breaking, the domain of $\eta$ on which $\Pi_L$ is defined, which endpoints the strict preferences hold at, and the order of the quantifiers in "sufficiently close to zero (sufficiently large)".

Difficulty

The obvious argument compares two closed forms, but the ban value is not a closed form: it is a maximum over a fee that switches the seller's option and its listing decision. Showing that the maximum is $\max\{\Pi_H,\Pi_L\}$ requires checking that the threshold fee keeps the seller listing, and that fees above the threshold earn at most $\Pi_H$ . The second obstacle is the shape of $\Pi_L$ : it is a rational function with a pole at $\eta=1$ , and its monotonicity rests on the sign of the printed derivative. The comparison point $\eta^*$ involves a square root, so the equivalence $\Pi_L\le\Pi_H\iff\eta\ge\eta^*$ is a quadratic-root argument rather than a one-line inequality. Finally, part 4 needs the baseline equilibrium profit $\Pi^*(\mu)$ from the full baseline game, i.e. a solution of the seller's problem (1) and the marketplace's problem (3) under uniform $G$ .

Formalization scope

All objects are real-valued, with the paper's letters: v c μ q η f; PiStar stands for $\Pi^*$ . The standing assumptions $c<v$ , $0<q<1$ and $0\le\eta\le 1$ are explicit hypotheses. The statements use the reduced seller problem (1) with $p_m=v$ , as the paper does after its Lemma 1; Lemma 1 itself is not posed. The uniform $G$ is the clamped CDF. Seller optimality, the baseline equilibrium and the ban value are optimality predicates (IsGreatest over the fees), never sSup or a chosen maximizer.

Conventions and disclosed additions:

In parts 1–3, $\Pi^*$ is any real in $(0,v-c)$ , a generalization of the paper's $\Pi^*$ for a general "well behaved" $G$ ; the proof uses nothing else.
Part 4 is posed for each fixed $\eta\in(0,1)$ : it fails at $\eta=0$ (ban) when $qv\le c$ and at $\eta=1$ (allow). It adds $c\ge 0$ , without which the marketplace bans for every $\mu$ at small $\eta$ .
The milestones on the ban value, the derivative's sign and $\eta^*$ add $v>0$ , which the proof uses without stating; each is false for some $v\le 0$ .
$\Pi_L$ and the threshold divide by $1-\eta$ and are stated only for $\eta<1$ ; the game itself has no division.
"Prefers" is strict in both directions.

Trivializing formalizations are ruled out: the ban value is not defined as $\max\{\Pi_H,\Pi_L\}$ , the thresholds in $\mu$ are quantified after $\eta$ and not before, $\Pi^*$ is constrained to $(0,v-c)$ , and preferences are strict.

A complete development needs elementary real analysis only: derivatives of rational functions, the intermediate value theorem on $[0,1)$ , limits at $1$ , and the baseline solution of (1) and (3) under uniform switching costs. That baseline solution is reusable for the other missions of this series. Proofs of individual milestones are welcome independently.

Selected references

A. Hagiu, J. Wright, Marketplace Leakage, Management Science, 2023. Authors' manuscript dated March 2023. doi:10.1287/mnsc.2023.4757
A. Piolatto, F. Schuett, Information vs Competition: How Platform Design Affects Profits and Surplus, TILEC Discussion Paper DP2022-002, 2022 (cited in footnote 8 of the paper for the idea that limiting information exchange reduces transaction value on a platform).

8 thms2 active usersReviewed

Completed

Economics Operations Research Optimization·Captain: mikedeng1

Marketplace Leakage 4: The Marketplace Prefers Not to Impose a Price-Parity Clause If and Only If q < 1/2 and μ > (v − c)/2Research Paper

Motivation

Online marketplaces (Amazon, Booking.com, Airbnb, Upwork) charge sellers a fee on every transaction they intermediate. Once a buyer has found a seller on the marketplace, both have an incentive to complete the sale off the platform and split the fee they save. This is leakage (also called disintermediation or showrooming), and it limits the fees a marketplace can sustain. Hagiu and Wright, Marketplace Leakage (Management Science, 2023, doi:10.1287/mnsc.2023.4757), build a minimal model of leakage and compare the strategies a marketplace can use against it.

One of these strategies is contractual: a price-parity clause (PPC), under which the seller must not charge less in its direct channel than on the marketplace, on pain of being delisted. The paper notes that such clauses have been used by hotel-booking platforms, price-comparison platforms and Amazon (p. 22). The paper's Proposition 4 asks when a marketplace that cannot observe how easily buyers switch actually wants such a clause. This mission formalizes that proposition and the profit formulas behind it.

Setting

A marketplace $M$ , a seller $S$ and a unit mass of buyers with unit demand. Every buyer values $S$ 's product at $v$ ; $S$ 's marginal cost is $c<v$ ; the outside option is worth $0$ . $S$ sells on $M$ at price $p_m$ , paying $M$ a fee $f$ per transaction, or directly at price $p_d$ with no fee. A buyer who buys directly bears a switching cost $s$ . In the baseline state switching costs are uniform on $[0,\mu]$ , $\mu>0$ , with clamped distribution function $G(s)=\min\{\max\{s/\mu,0\},1\}$ . In the no-switching state switching costs are infinite and nobody buys directly. The baseline state occurs with probability $q$ . $S$ knows the state when it decides; $M$ does not when it sets $f$ .

Without a PPC, $S$ always lists, sets $p_m=v$ , and in the baseline state picks $p_d\le v$ to maximize

\pi(f,p_d)=(p_d-c)G(v-p_d)+(v-c-f)\big(1-G(v-p_d)\big).

A maximizer is a seller-optimal price $p_d^*(f)$ . $M$ 's value is

\Pi^*=\max_{f\le v-c} f\big(1-q\,G(v-p_d^*(f))\big).

With a PPC, a listed seller must set $p_d=p_m=v$ and earns $v-c-f$ . A seller that delists earns $\max_{c\le p_d\le v}(p_d-c)G(v-p_d)$ in the baseline state and $0$ in the no-switching state. It accepts $M$ 's offer when listing pays at least as much, so $M$ 's value $\Pi^*_{PPC}$ is the largest expected revenue $f\cdot\Pr[\text{accept}]$ over all fees $f$ .

Formalization targets

Goal: Proposition 4 (p. 23)

For $c<v$ , $\mu>0$ and $0<q\le 1$ , both values exist, and

\Pi^*>\Pi^*_{PPC}\iff q<\tfrac12\ \text{ and }\ \mu>\tfrac{v-c}{2},\qquad\text{otherwise}\quad \Pi^*_{PPC}\ge\Pi^* .

The goal states the comparison for any values satisfying the optimality predicates, so it is insensitive to how either value is later computed.

Milestones

$\Pi^*_{PPC}=\max\{v-c-D,\ (1-q)(v-c)\}$ , where $D=\max_{c\le p_d\le v}(p_d-c)G(v-p_d)$ (p. 23).
$D=\dfrac{(v-c)^2}{4\mu}$ if $\mu\ge\frac{v-c}{2}$ and $D=v-c-\mu$ otherwise, so $\Pi^*_{PPC}$ has a closed form (p. 39).
For $q<\tfrac12$ : $\displaystyle\Pi^*=(v-c)\Big(1-q\min\Big\{\frac{v-c}{2\mu},1\Big\}\Big)$ (p. 39).

Significance

Proposition 4 identifies a trade-off. A PPC removes leakage entirely, but it also takes away the seller's ability to divert some buyers when the fee turns out to be too high, so the seller may refuse to participate. When the baseline state is unlikely and switching costs in it are high, the marketplace earns more by tolerating leakage and charging the full surplus $v-c$ . In every other case the clause pays. This makes the welfare and competition-policy debate about parity clauses explicit in a two-parameter region. It also contrasts with the case without uncertainty, where a PPC is always better for the marketplace.

The paper's proof (§8.5, pp. 39–40) is a short case comparison between closed forms. It has not been machine-checked. The printed formula for $\Pi^*$ when $q\ge 1/2$ omits the corner fee $f=v-c$ and is wrong for small $\mu$ . The conclusion $\Pi^*_{PPC}\ge\Pi^*$ still holds there, but by a different comparison. A formal proof pins down which steps survive.

Difficulty

Two optimizations are nested. The seller's optimal direct price changes regime at $f=2\mu$ , where the uniform distribution's kink binds. The marketplace's revenue without a PPC is therefore piecewise in $f$ , with an interior candidate $\mu/q$ that is feasible only when $q\ge 1/2$ . Under a PPC, revenue is discontinuous in $f$ because acceptance switches on and off. Its maximum is attained only because acceptance is weak. Comparing the two values requires a case split over $q\gtrless\tfrac12$ and $\mu$ against $(v-c)/2$ and $q(v-c)$ , and the boundary cases include genuine ties ( $\Pi^*=\Pi^*_{PPC}$ for $q<\tfrac12$ , $\mu\le\frac{v-c}{2}$ ). Reading off a single printed closed form for $\Pi^*$ fails in part of the $q\ge 1/2$ region.

Formalization scope

All objects are in one definitions file in namespace MarketplaceLeakage.Parity. The parameters are real numbers v c μ q, with standing hypotheses c < v, 0 < μ, 0 < q, q ≤ 1 on every theorem. The paper states $v>c$ (p. 5) and $\mu>0$ (p. 9). $q\in(0,1]$ is added: $q$ is a probability, and at $q=0$ both values equal $v-c$ , so the "if" direction of the goal fails. $q=1$ is allowed. The statements use the reduced seller problem (1), as the paper does after its Lemma 1 (p. 7), with $p_m=v$ . Lemma 1 itself is not posed.

Committed conventions:

$G$ is the clamped uniform CDF.
Seller-optimality is a predicate (IsSOpt), not a formula.
$\Pi^*_{PPC}$ (IsPPCValue) is the attained maximum of $f\cdot(q\,\mathbf 1[\text{accept}_B]+(1-q)\,\mathbf 1[\text{accept}_N])$ over all $f\in\mathbb R$ . Acceptance is weak and is stated against every delisting price $c\le p_d\le v$ .
$\Pi^*$ (IsNoPPCValue) is the attained maximum of $f(1-qG(v-p_d))$ over $f\le v-c$ and seller-optimal $p_d$ .
"Prefers not to impose" is strict; "otherwise prefers to impose" is weak.

These choices rule out the trivializing formalizations. Neither value is defined by its printed max-expression, which would make the milestones definitional. Strict acceptance would leave the PPC optimum unattained. A value given by sSup would be meaningless off its domain. Reading "prefers to impose" strictly would make the statement false at the ties.

No published platform definitions are reused. A complete development needs only elementary real analysis: maximizing piecewise-quadratic functions, attainment on compact intervals, and case analysis over min/max. The lemmas on the seller's best response under the uniform $G$ are reusable in the companion missions on Propositions 1–3 of the same paper. Proofs of any milestone are welcome independently.

Selected references

A. Hagiu, J. Wright, Marketplace Leakage, Management Science, 2023 (authors' manuscript dated March 2023). https://doi.org/10.1287/mnsc.2023.4757

6 thms2 active usersReviewed

Economics Operations Research Optimization·Captain: mikedeng1

Quality Strategies in Network Markets: Under Potential Maximization the Equilibrium Quality Equates Marginal Cost to n Times the Harmonic-Mean Valuation Times the Uniform Average of ∂f(i,q)/∂qResearch Paper

Motivation

A firm that sells a network good (a platform, a communication service, a standard) faces consumers whose benefit from buying grows with the number of other buyers. When these network effects are strong, the buying decisions form a coordination game: everybody buying and nobody buying can both be equilibria at the same price and quality. The firm's choice of quality then depends on which equilibrium it expects consumers to play.

The classical answer, going back to Spence's analysis of monopoly quality (Spence 1975), is that a monopolist sets quality for the marginal consumer. Under the usual equilibrium-selection criteria (Pareto dominance, focality) the network-good monopolist inherits this logic. L. T. Chan, Quality Strategies in Network Markets (Management Science, 2023; SSRN copy 4203818), asks what happens when the firm instead anticipates potential maximization, a generalization of risk dominance to many players introduced through the potential games of Monderer and Shapley (1996). The answer is a different first-order condition for quality, in which every consumer's valuation and every possible number of buyers matter. This mission formalizes that condition, Proposition 5 of the paper, together with the chain of results in §3 that leads to it.

Setting

There are $n\ge 1$ consumers $N=\{1,\dots,n\}$ . Consumer $i$ has a valuation $v_i>0$ , labelled so that $v_1\ge\dots\ge v_n$ . The benefit $f(k,q)\ge 0$ of the good when $k$ consumers buy at quality $q$ is weakly increasing in $k$ and, in $q$ , weakly increasing and differentiable. The firm's cost of quality $c(q)\ge 0$ is weakly increasing and differentiable.

In stage 1 the firm chooses a price $p\ge 0$ and a quality $q\ge 0$ . In stage 2 consumers simultaneously decide whether to buy. If $B\subseteq N$ is the set of buyers, consumer $i$ receives the payoff (7)

u_i(B,p,q)=v_if(|B|,q)-p\ \text{ if } i\in B,\qquad u_i(B,p,q)=0\ \text{ if } i\notin B,

and the firm earns $|B|p-c(q)$ . A buyer set $B$ is a Nash equilibrium of stage 2 if no buyer gains by leaving and no non-buyer gains by joining. The market has strong network effects at $q$ when $v_if(i,q)$ is strictly increasing in $i$ .

The potential (10) of a buyer set is

\Phi(B,p,q)=\sum_{i=1}^{|B|}f(i,q)-p\sum_{i\in B}\frac1{v_i}.

A potential maximizer is a buyer set maximizing $\Phi(\cdot,p,q)$ over all subsets of $N$ . A firm that anticipates potential maximization earns $\Pi(p,q)=np-c(q)$ when all consumers buying is a potential maximizer, and $-c(q)$ otherwise. In Lean these objects are Market, Market.Standing, Market.StrongNE, Market.u, Market.IsNash, Market.pot, Market.IsPotMax and Market.profitPM in the namespace NetworkQuality.PotentialMax.

Formalization targets

Goal: Proposition 5 (p. 15)

Assume the standing assumptions and strong network effects at every $q\ge 0$ . If $(p^*,q^*)$ maximizes $\Pi$ over $p\ge 0$ , $q\ge 0$ and $q^*>0$ , then

c'(q^*)=n\Big(\frac1n\sum_{i=1}^n\frac1{v_i}\Big)^{-1}\frac1n\sum_{i=1}^n\frac{\partial f(i,q^*)}{\partial q}.

The statement is the necessary first-order condition. It fixes no functional form for $f$ or $c$ .

Milestones

(11), p. 13. For $i\notin B_{-i}$ : $u_i(B_{-i}\cup\{i\})-u_i(B_{-i})=v_i[\Phi(B_{-i}\cup\{i\})-\Phi(B_{-i})]$ , so stage 2 is a weighted potential game.
§3.5, p. 14. Every potential maximizer is a Nash equilibrium.
Proposition 1, p. 10. Under strong network effects the equilibria are exactly $\{N\}$ for $p<v_1f(1,q)$ , $\{\emptyset\}$ for $p>v_nf(n,q)$ , and $\{N,\emptyset\}$ in between.
(12), p. 14. Under strong network effects every potential maximizer is $N$ or $\emptyset$ , and $N$ is one iff $p\le\big(\frac1n\sum_i\frac1{v_i}\big)^{-1}\frac1n\sum_i f(i,q)=:p(q)$ .
(13), p. 14. $v_1f(1,q)\sum_i\frac1{v_i}\le\sum_i f(i,q)\le v_nf(n,q)\sum_i\frac1{v_i}$ .
(14), p. 15. At each quality the maximal profit over prices $p\ge0$ is $n\,p(q)-c(q)$ , attained at $p(q)$ .

Significance

The result. Proposition 5 replaces the Spence condition $c'(q)=n\,v_n\,\partial f(n,q)/\partial q$ (Proposition 4 of the paper) by one in which the marginal consumer's valuation $v_n$ is replaced by the harmonic mean of all valuations, and the equilibrium benefit $f(n,q)$ by its uniform average over the number of buyers. Comparing it with the social optimum (Proposition 3, arithmetic mean of valuations) shows that a firm worried about miscoordination underprovides quality relative to the planner, increasingly so as valuations become more dispersed, and that it tends to undersupply (oversupply) quality when the number of buyers and quality are complements (substitutes) in the benefit $f$ (p. 15).

Formalizing it. The paper's arguments are in the main text (§3.2 and §3.5) and are short; some steps are only sketched: Proposition 1's proof treats only buyer sets of the form $\{1,\dots,k\}$ , and (12) is derived only in the price range with two equilibria. A machine-checked development makes these steps complete, fixes the tie-breaking convention of the selection, and isolates exactly which assumptions the first-order condition uses (none of the convexity the paper assumes). No part of this result has a machine-checked proof at the time of writing.

Difficulty

The objects are finite and the algebra is elementary, so the difficulty lies in bookkeeping that the paper leaves implicit. The obvious reading of Proposition 1, "consumers $1$ to $k$ buy", is not forced when valuations tie; excluding an arbitrary buyer set of intermediate size needs a comparison between its weakest buyer and its strongest non-buyer, using the ordering of valuations and nonnegativity of $f$ . The characterization (12) is a statement about maximizers over all $2^n$ buyer sets, not just about the two candidates the text compares, so it rests on the reduction "potential maximizer ⇒ Nash equilibrium ⇒ $N$ or $\emptyset$ ". Finally the firm optimizes jointly over price and quality against a discontinuous profit function; the first-order condition only appears after the price has been optimized out at each quality, and it needs differentiability at an interior optimum.

Formalization scope

Consumers are Fin n; the paper's consumer $i$ is Lean index $i-1$ , while the first argument of $f$ is a number of buyers in ℕ, so $\sum_{i=1}^n f(i,q)$ is ∑ i : Fin n, M.f (i.val + 1) q. $v_1$ and $v_n$ are M.v ⟨0, _⟩ and M.v ⟨n - 1, _⟩. $f$ and $c$ are total functions on ℝ.

The standing assumptions (Market.Standing, pp. 4 and 9) are: $n\ge1$ ; $v_i>0$ and $v$ antitone; for $k\ge1$ and $q\ge0$ , $f(k,q)\ge0$ , $f$ weakly increasing in $k$ and in $q$ on $[0,\infty)$ , $f(k,\cdot)$ differentiable on $(0,\infty)$ ; $c\ge0$ on $[0,\infty)$ , weakly increasing there and differentiable on $(0,\infty)$ . Statements about a single quality add $q\ge0$ , the paper's domain.

Added hypotheses, each disclosed in the items: equilibria are pure (buyer sets); the goal assumes an interior quality $q^*>0$ and strong network effects at every $q\ge0$ ; the "sufficiently convex" cost of p. 4 is dropped, so the goal is the necessary condition only. The profit under potential maximization selects "all buy" at the tie $\Phi(N)=\Phi(\emptyset)$ , as the paper's "if and only if $p\le\dots$ " does.

The profit is defined through the selection (IsPotMax over all buyer sets), not as the reduced formula (14), and the goal's optimality hypothesis ranges over price and quality jointly; defining the profit by (14), or restricting maximizers to $\{N,\emptyset\}$ , would trivialize the mission and is ruled out. Derivatives are deriv, and the standing assumptions guarantee they are genuine at $q^*>0$ .

Everything needed beyond Mathlib (Finset, deriv, IsLocalMax) is in the single definition file. Proofs of the milestones in any order are welcome, as are proofs of the goal that use the milestones as stepping stones.

Selected references

L. T. Chan, Quality Strategies in Network Markets, Management Science, 2023. https://doi.org/10.1287/mnsc.2023.4792 (SSRN version of April 2023: https://ssrn.com/abstract=4203818)
D. Monderer and L. S. Shapley, Potential Games, Games and Economic Behavior 14 (1996), 124–143. https://doi.org/10.1006/game.1996.0044
A. M. Spence, Monopoly, Quality, and Regulation, Bell Journal of Economics 6 (1975), 417–429. https://www.jstor.org/stable/3003302

8 thms2 active usersReviewed

Completed

Economics Operations Research Optimization·Captain: mikedeng1

Marketplace Leakage 1: With Uniform Switching Costs the Equilibrium Fee Is min{μ, v − c}, Leakage Is Positive but Partial, and the Marketplace's Profit Increases in μResearch Paper

Motivation

Online marketplaces such as Airbnb, Amazon, eBay, Preply or Upwork earn most of their revenue from transaction fees: a seller who sells through the marketplace pays a fee on every sale. Many of these sellers also run their own sales channel, and a buyer who discovers a seller on the marketplace can often complete the purchase directly with that seller, avoiding the fee. This is marketplace leakage (also called disintermediation or showrooming of the platform). Marketplaces respond with measures the paper lists on its first pages: bundling transaction-related services, restricting buyer–seller communication before a transaction, and penalizing sellers caught taking clients off the platform.

Hagiu and Wright (Marketplace Leakage, Management Science, 2023) build a minimal model of this tension. Their baseline analysis answers the first question any of the later strategies depends on: if the marketplace can only choose its fee, what fee does it set, how much leakage remains in equilibrium, and how do these respond when buying directly becomes more costly for buyers? This mission formalizes that baseline result, Proposition 1 of the paper, for uniformly distributed switching costs.

Setting

There is one marketplace $M$ , one seller $S$ and a unit mass of buyers, each wanting one unit of $S$ 's product. Every buyer values the product at $v$ ; $S$ 's marginal cost is $c$ , with $c<v$ ; the outside option is worth $0$ .

$S$ can sell through $M$ , paying $M$ a fee $f$ per transaction, or through its direct channel, which carries no fee. It sets a price $p_m$ on $M$ and a direct price $p_d$ . A buyer who buys directly bears a switching cost $s$ ; in this mission $s$ is uniformly distributed on $[0,\mu]$ with $\mu>0$ , so its CDF is

G(s)=\min\Bigl\{\max\Bigl\{\frac s\mu,0\Bigr\},1\Bigr\}.

The timing is: $M$ sets $f$ ; observing $f$ , $S$ sets its prices; buyers then choose. The paper's Lemma 1 lets one fix $p_m=v$ , so $S$ only chooses $p_d\le v$ . A buyer buys directly iff $s\le v-p_d$ , so a share $G(v-p_d)$ of buyers — the leakage — buys directly. $S$ 's profit at fee $f$ is

\pi_f(p_d)=(p_d-c)\,G(v-p_d)+(v-c-f)\,\bigl(1-G(v-p_d)\bigr),

and $M$ earns $\Pi=f\,(1-G(v-p_d))$ . A direct price is seller-optimal at $f$ if it maximizes $\pi_f$ over $p_d\le v$ . An equilibrium outcome is a pair $(f,p_d)$ with $f\le v-c$ , $p_d$ seller-optimal at $f$ , such that no other fee $f'\le v-c$ , followed by a seller-optimal response, gives $M$ more.

Formalization targets

Goal: Proposition 1

For every $\mu>0$ an equilibrium outcome exists, and every equilibrium outcome $(f^*,p_d^*)$ satisfies

f^*(\mu)=\min\{\mu,v-c\},\qquad p_d^*(\mu)=v-\min\Bigl\{\frac\mu2,\frac{v-c}2\Bigr\},\qquad \Pi^*(\mu)=\begin{cases}\mu/2 & \mu\le v-c,\\ (v-c)\bigl(1-\frac{v-c}{2\mu}\bigr) & \mu\ge v-c,\end{cases}

with leakage $G(v-p_d^*)=\frac1\mu(v-p_d^*)\in(0,1)$ . As $\mu$ increases, the fee weakly increases, the direct price and the leakage weakly decrease, and the marketplace's profit strictly increases.

Milestones

(4): for every fee $f\ge0$ the seller's optimal direct price is unique and equals $v-f/2$ if $f\le2\mu$ and $v-\mu$ if $f\ge2\mu$ .
(5): at such a response the marketplace earns $f(1-f/(2\mu))$ if $f\le 2\mu$ and $0$ if $f\ge2\mu$ .
The optimal fee (proof of Proposition 1): $(f,p_d)$ is an equilibrium outcome iff $f=\min\{\mu,v-c\}$ and $p_d$ is seller-optimal at $f$ .
Equilibrium leakage (proof of Proposition 1): $G(v-p_d^*)=f^*/(2\mu)=\min\{1/2,(v-c)/(2\mu)\}$ .

Significance

Proposition 1 is the baseline against which the paper measures every anti-leakage strategy: investment in transaction benefits, communication bans, referral fees and price-parity clauses are each compared with the fee-only outcome $\Pi^*(\mu)$ , and Proposition 3 of the paper uses the closed form (6) directly. The result also has a substantive message: a fee-setting marketplace never eliminates leakage, but never lets it become total, and it gains from higher switching costs even though its own fee response offsets part of their effect on leakage.

The proposition is proved in the paper by elementary calculus. To our knowledge it has no machine-checked proof. Formalizing it produces a checked version of the baseline game, a verified statement of the seller's best response and the marketplace's value as functions of the fee, and a template that the companion missions on this paper reuse.

Difficulty

The seller's problem is not a smooth concave program: the clamped distribution $G$ creates a kink at $v-p_d=\mu$ , below which every buyer switches and the profit is linear in $p_d$ . The first-order condition $p_d=v-f/2$ is the optimum only while $f\le2\mu$ ; above that the optimum sits at the kink. The marketplace's objective inherits a kink at $f=2\mu$ , and its feasible set $f\le v-c$ adds a corner that binds exactly when $\mu>v-c$ . Negative fees are feasible and must be ruled out. The comparative statics compare equilibrium objects across two parameter values that may lie in different regimes, so the statement cannot be read off one formula.

Formalization scope

All parameters are real numbers, with the standing assumptions $c<v$ and $\mu>0$ as explicit hypotheses. $G$ is the clamped uniform CDF above. The statements use the reduced seller problem (1) with $p_m=v$ , as the paper does after Lemma 1; Lemma 1 itself, which concerns the full game in which $S$ also chooses $p_m$ , is not posed. Seller-optimality is an optimality predicate over $p_d\le v$ , and the equilibrium is an optimality predicate over feasible fees $f\le v-c$ (negative fees included); "max" is attained, not a supremum. The displays (4) and (5) are stated for $f\ge0$ , which is what they require; the paper's preface "Assuming $f\le v-c$ " is not needed and does not exclude $f<0$ .

Trivializing formalizations are ruled out: the seller's response and the marketplace's profit are not defined by the closed forms (4)–(5), the marketplace's value is not an unattained sSup, the equilibrium fee is not selected by Classical.choose, and the comparative statics are stated about equilibrium outcomes at two values of $\mu$ , not about the formulas alone.

The development needs only Mathlib's real arithmetic, min/max and order lemmas. A proof of the seller's best response for a clamped uniform distribution is reusable in the companion missions on transaction benefits, communication bans and price parity, which restate the same model. Proofs of any milestone are welcome independently.

Selected references

A. Hagiu and J. Wright, Marketplace Leakage, Management Science, 2023. https://doi.org/10.1287/mnsc.2023.4757 (formalized from the authors' manuscript dated March 2023; Proposition 1 on pp. 9–10, proof in §8.2, p. 34).

6 thms2 active usersReviewed

Algorithmic Game Theory

Missions

Improving Access to Rare Disease Treatments: Subsidy, Pricing, and Payment Schemes I: With Manufacturer Pricing, Subsidize Only the Manufacturer; Outcome-Based Pay Raises the Price iff B < k − 1/8Research Paper

Motivation

Setting

Formalization targets

Government policy under each payment scheme

Price comparison

Significance

Difficulty

Formalization scope

Selected references

Infinite-Dimensional Fisher Markets and Tractable Fair Division 2: For Linear Valuations on [0,1] the Feasible Utility Set Is a Projection of Linear and Parabolic ConstraintsResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Network Externalities and Market Dominance: Under In/Out Demand the Impulse Selects the Introspective Equilibrium by Its Position Relative to the Middle EquilibriumResearch Paper

Motivation

Setting

Formalization targets

Equilibrium structure

Selection rule

Significance

Difficulty

Formalization scope

Selected references

Personalized Pricing and Distribution Strategies II: With Personalized Pricing by the Manufacturer, Dual Distribution Is Optimal Iff β > β_PZ(α), and β_PU(α) > β_PP(α)Research Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

The Voice of Customers in Customization II: Under O-Learning, the Cheap-Signaling Separating Equilibrium Exists If and Only If θH/θL ≥ ΛResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 3 (p. 17)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Information Design for Congested Social Services: Optimal Need-Based Persuasion 3: Information Design Pareto-Dominates Full Information Exactly When Low-Need Arrivals Exceed a ThresholdResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 3(1)–(2)

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Voice of Customers in Customization I: Under A-Learning, Truthful Cheap-Talk Communication Is an Equilibrium If and Only If θH/θL ≥ ΔResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Softening Competition Through Unilateral Sharing of Customer Data: For Every Monotone-Hazard-Rate Distribution, Sharing Data on [z^N, b′] Makes Both Firms Strictly Better OffResearch Paper

Why a firm would hand customer data to a rival

Setting

Formalization targets

Goal: Proposition 1

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Voice of Customers in Customization IV: The A-Learning Threshold Δ Exceeds the O-Learning Threshold Λ If and Only If γ < max{2s/(2s+k), (√(s²+4sk) − s)/(2k)}Research Paper

Motivation

Setting

Formalization targets