Mechanism Design

Motivation

Data brokers sell information about consumers to firms that decide whom to target: a lender deciding whom to offer credit, a retailer deciding whom to mail. Two products dominate this market. A marketing list sells contact information together with an analysis, so that a firm cannot reach the consumer at all without buying. A data append adds information about consumers the firm already knows, so that the firm can act even without buying. Liang Guo's Selling Data to Marketers (Management Science, doi:10.1287/mnsc.2023.01350) studies how a monopoly data seller should design a menu of data products when the buyers' targeting costs are private, and shows that the answer differs sharply between the two products.

This mission formalizes the data-append result in the paper's base model with a binary targeting value: Proposition 3 (p. 13 of the author's manuscript). The companion missions of the series cover marketing lists and the general model with a rotation-ordered family of posterior distributions.

Setting

A marketer can take an action at cost $c>0$. The action yields a value $u\in\{\underline u,\bar u\}$, with $u=\bar u$ with prior probability $\varphi\in(0,1)$, so the prior mean is $\hat u=\varphi\bar u+(1-\varphi)\underline u$. Not acting yields $0$.

The seller can produce a signal $w\in\{w_h,w_l\}$ with $\Pr(w_h\mid\bar u)=\Pr(w_l\mid\underline u)=\alpha$, where the informativeness $\alpha$ is chosen from $[\underline\alpha,\bar\alpha]\subset(1/2,1)$. The signal probabilities are $\sigma_h(\alpha)=\varphi\alpha+(1-\varphi)(1-\alpha)$ and $\sigma_l(\alpha)=1-\sigma_h(\alpha)$, and the posterior means after $w_h$ and $w_l$ are $v_h(\alpha)$ and $v_l(\alpha)$, computed by Bayes' rule. The standing assumption $v_l(\underline\alpha)<c<v_h(\underline\alpha)$ makes acting worthwhile exactly after the high signal, so a marketer of cost $c$ values information $\alpha$ at $\sigma_h(\alpha)[v_h(\alpha)-c]$. Serving a marketer with informativeness $\alpha$ costs the seller $k(\alpha)$, with $k(\underline\alpha)=0$ and $k$ increasing.

Marketers have cost $c_H$ with probability $\theta$ and $c_L<c_H$ with probability $1-\theta$, privately known. The seller offers a menu of two plans $(T_H,\alpha_H)$ and $(T_L,\alpha_L)$ with fees $T_j\ge0$. Type $i$'s payoff from plan $j$ is

$$U_{ij}=-T_j+\sigma_h(\alpha_j)[v_h(\alpha_j)-c_i].$$

With data appends, a marketer who buys nothing can still act on the prior, so its outside option is $U_{i0}=\max\{\hat u-c_i,0\}$. The seller maximizes $\Pi=\sum_i\theta_i[T_i-k(\alpha_i)]$ subject to $U_{ii}\ge U_{i0}$ ($IR_i$) and $U_{ii}\ge U_{ii'}$ ($IC_{i,i'}$). An optimal menu solves this problem; its informativeness levels are $\alpha_H^*,\alpha_L^*$.

The benchmark is the seller's problem when costs are observable: for each type it maximizes $\Pi_i=\theta_i[\sigma_h(\alpha)[v_h(\alpha)-c_i]-k(\alpha)]$ over $[\underline\alpha,\bar\alpha]$. Any maximizer is an efficient informativeness $\alpha_i^e$.

Formalization targets

Goal: Proposition 3 (p. 13)

When $c_L<c_H<\hat u$:

$$\{\alpha_H^*\}=\{\alpha_H^e\},\qquad \varphi<\tfrac12\ \Rightarrow\ \alpha_L^*<\alpha_L^e,\qquad \varphi>\tfrac12\ \Rightarrow\ \alpha_L^*>\alpha_L^e .$$

The first claim is an equality of sets: the high-cost informativeness levels of optimal menus are exactly the efficient ones at $c_H$. The inequalities hold for every optimal menu and every efficient $\alpha_L^e$.

Milestones

1. Willingness to pay (§3.2, p. 13): for $c_L<c_H<\hat u$, $U_{ij}-U_{i0}=-T_j+\sigma_l(\alpha_j)[c_i-v_l(\alpha_j)]$, which is increasing in $c_i$.
2. Reduction (8) (p. 13): with $IR_L$ and $IC_{H,L}$ binding, the problem becomes the maximization over $(\alpha_H,\alpha_L)$ of

$$\theta\big[\sigma_h(\alpha_H)[v_h(\alpha_H)-c_H]-\sigma_h(\alpha_L)(c_L-c_H)-k(\alpha_H)\big]+(1-\theta)\big[\sigma_h(\alpha_L)[v_h(\alpha_L)-c_L]-k(\alpha_L)\big]-\hat u+c_L .$$

3. The $\alpha_L$-derivatives (proof of Proposition 3, p. 32): the benchmark derivative $(1-\theta)[\varphi(\bar u-c_L)-(1-\varphi)(\underline u-c_L)-k'(\alpha_L)]$ and the derivative of (8), which adds $\theta(1-2\varphi)(c_L-c_H)$.

Significance

The result says that a data seller's distortion depends on the product's form. With marketing lists the low-cost marketers are the high type, their plan is efficient, and the high-cost plan is distorted (Proposition 2, p. 11). With data appends and costs below the prior mean, the outside option $\hat u-c_i$ falls with $c_i$ faster than the value of information does, so high-cost marketers have the larger willingness to pay. The roles of the types switch, the low-cost plan is distorted, and the direction of the distortion is reversed, giving the paper's "double mirror image" (p. 13). The direction is set by the skewness of the prior through the sign of $1-2\varphi$, not by an assumed single-crossing condition.

The result is proved in the paper, in an appendix argument of a few lines that invokes Topkis's monotonicity theorem. To our knowledge it has no machine-checked proof. Formalizing it makes explicit what the printed proof leaves to the reader: that the constraints dropped in (8) hold at its optimum, that the efficient and optimal informativeness need not be unique, and which regularity of $k$ the strict inequalities need.

Difficulty

The obvious argument substitutes the binding constraints, compares first-order conditions, and invokes Topkis's theorem. Three steps of it are not automatic. First, the reduction drops $IR_H$, $IC_{L,H}$ and the nonnegativity of fees; these must be shown to hold at every maximizer of (8), and $IC_{L,H}$ holds only because the maximizers of (8) are ordered in the right direction, which is itself a comparative-statics fact. Second, the reduction identifies the optimal menus only if (8) attains its maximum. Third, Topkis's theorem yields only weak inequalities, $\alpha_L^*\le\alpha_L^e$; strictness needs the efficient informativeness to be interior and $k$ to be differentiable there, which footnote 5 (p. 7) supplies. Without it, both optima can sit at the same corner $\underline\alpha$ or $\bar\alpha$.

Formalization scope

Everything is stated over $\mathbb R$ in the sub-namespace SellingData.AppendsBinary. The two types form an inductive type CostType with constructors H and L. A Model structure holds $\underline u<\bar u$, $\varphi\in(0,1)$, $1/2<\underline\alpha<\bar\alpha<1$, $\theta\in(0,1)$, $0<c_L<c_H$, $k(\underline\alpha)=0$, $k$ weakly increasing on $[\underline\alpha,\bar\alpha]$, and the standing assumption $v_l(\underline\alpha)<c_i<v_h(\underline\alpha)$ for both costs. The posteriors are defined with the divisions of the paper's (2). The outside option is the printed $\max\{\hat u-c_i,0\}$.

Optimality and efficiency are predicates on maximizers, never a chosen maximizer. The optimal menu is defined from the data-append screening problem itself; defining it through (8) would make the first claim of the goal trivial and is ruled out. The goal additionally assumes the part of footnote 5 that the strict inequalities need: $k$ continuous on $[\underline\alpha,\bar\alpha]$, differentiable on $(\underline\alpha,\bar\alpha)$, right derivative $0$ at $\underline\alpha$, and $k'(\alpha)\to+\infty$ as $\alpha\to\bar\alpha^-$. Convexity and twice differentiability, which the footnote also lists, are not assumed. The milestones carry only what they need: none for the willingness to pay, continuity of $k$ for one part of the reduction, and differentiability at the point for the derivative.

A complete development needs Bayes posteriors for a symmetric binary signal, elementary calculus (derivatives, the mean value theorem, extrema on compact intervals), and Topkis's monotonicity theorem, which is on the platform (Theorem 2.8.4) and is referenced by this mission. Proofs of the milestones and of the goal are welcome. Lemmas on the binary-signal posteriors (for instance the identity $\sigma_h(\alpha)v_h(\alpha)+\sigma_l(\alpha)v_l(\alpha)=\hat u$) are reusable by the companion mission on marketing lists.

Selected references

• Liang Guo, Selling Data to Marketers, Management Science, 2025, author's manuscript. doi:10.1287/mnsc.2023.01350
• Donald M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. doi:10.1515/9781400822539

Why sell information to marketers

Data brokers such as Acxiom, Nielsen and Oracle, and data generators such as Google and Facebook, sell processed consumer data to firms that use it to decide whom to target, whom to lend to, or which market to enter. The U.S. Federal Trade Commission's 2014 report on data brokers distinguishes two products: a marketing list, which carries contact information without which the buyer cannot act at all, and a data append, which enriches data the buyer already holds. Liang Guo's Selling Data to Marketers (Management Science, doi:10.1287/mnsc.2023.01350) asks how a seller should design a menu of data products of different informativeness when buyers differ in a privately known cost of acting.

The question belongs to the theory of optimal screening (Mussa and Rosen 1978; Maskin and Riley 1984), but with a twist: the buyer's marginal value of information is not a primitive. It is derived from the buyer's decision problem, so the direction of the single-crossing condition is itself an outcome of the model. This mission formalizes the paper's analysis of marketing lists in the base model with a binary value.

Setting

A marketer can take an action (target a consumer) at cost $c>0$. The action's value $u$ is $\bar u$ with prior probability $\phi\in(0,1)$ and $\underline u<\bar u$ otherwise. The seller can provide a binary signal $w\in\{w_h,w_l\}$ with $\Pr(w_h\mid\bar u)=\Pr(w_l\mid\underline u)=\alpha$, where the informativeness $\alpha$ lies in an interval $[\underline\alpha,\bar\alpha]\subset(1/2,1)$. The probability of the optimistic signal is $\sigma_h(\alpha)=\phi\alpha+(1-\phi)(1-\alpha)$, the posterior probability of $\bar u$ after it is $\phi_h(\alpha)=\phi\alpha/\sigma_h(\alpha)$, and the posterior mean is $v_h(\alpha)=\phi_h(\alpha)\bar u+[1-\phi_h(\alpha)]\underline u$; $\sigma_l,\phi_l,v_l$ are defined symmetrically. The paper assumes $v_l(\underline\alpha)<c<v_h(\underline\alpha)$, so a marketer acts exactly after $w_h$, and a marketer with cost $c$ who pays $T$ for a signal of informativeness $\alpha$ gets

$$U=-T+\sigma_h(\alpha)[v_h(\alpha)-c].$$

Serving a marketer at informativeness $\alpha$ costs the seller $k(\alpha)$, with $k(\underline\alpha)=0$ and $k$ increasing.

There are two cost types, $c_H>c_L>0$, with $\Pr(H)=\theta\in(0,1)$; write $\theta_H=\theta$, $\theta_L=1-\theta$. Under the benchmark with observable cost, the seller extracts all surplus and chooses $\alpha$ to maximize

$$\Pi_i(\alpha)=\theta_i\big[\sigma_h(\alpha)[v_h(\alpha)-c_i]-k(\alpha)\big],$$

whose maximizers are the efficient levels $\alpha^e_i$. With private costs the seller offers a menu $(T_H,\alpha_H),(T_L,\alpha_L)$ with $T_j\ge0$ and maximizes $\Pi=\sum_i\theta_i[T_i-k(\alpha_i)]$ subject to individual rationality $U_{ii}\ge0$ and incentive compatibility $U_{ii}\ge U_{ii'}$, where $U_{ij}=-T_j+\sigma_h(\alpha_j)[v_h(\alpha_j)-c_i]$. This is problem (6); its solutions are the optimal menus, with informativeness levels $\alpha^*_H,\alpha^*_L$.

Formalization targets

Goal: Proposition 2

Under the regularity of $k$ described below,

$$\alpha^*_L=\alpha^e_L,\qquad \alpha^*_H>\alpha^e_H\ \text{ if }\phi<\tfrac12,\qquad \alpha^*_H<\alpha^e_H\ \text{ if }\phi>\tfrac12.$$

The first claim is an equality of sets of maximizers; the inequalities compare every optimal menu with every efficient level.

Milestones

1. The derivative of the benchmark profit: $\partial\Pi_i/\partial\alpha_i=\theta_i[\phi(\bar u-c_i)-(1-\phi)(\underline u-c_i)-k'(\alpha_i)]$.
2. The cross derivative $\partial^2\Pi_i/\partial\alpha_i\partial c_i=\theta_i(1-2\phi)$, stated as a mixed second difference.
3. Proposition 1: $\alpha^e_i$ increases with $c_i$ if $\phi<1/2$ and decreases if $\phi>1/2$.
4. The reduction of (6) to the problem in $(\alpha_H,\alpha_L)$ alone,

$$\max_{\alpha_H,\alpha_L}\ \theta\big[\sigma_h(\alpha_H)[v_h(\alpha_H)-c_H]-k(\alpha_H)\big]+(1-\theta)\big[\sigma_h(\alpha_L)[v_h(\alpha_L)-c_L]-\sigma_h(\alpha_H)(c_H-c_L)-k(\alpha_L)\big],\qquad(7)$$

obtained by making IR$_H$ and IC$_{L,H}$ bind. 5. The derivative of (7) in $\alpha_H$: $\theta[\phi(\bar u-c_H)-(1-\phi)(\underline u-c_H)-k'(\alpha_H)]+(1-\theta)(1-2\phi)(c_H-c_L)$.

Significance

In textbook screening the low type's allocation is distorted downward to reduce the high type's rent. Here the low type of the screening problem is the high-cost marketer, and its information can be distorted in either direction: the rent $\sigma_h(\alpha_H)(c_H-c_L)$ conceded to low-cost marketers falls with $\alpha_H$ when $\phi<1/2$ and rises when $\phi>1/2$. Proposition 2 therefore says that a seller of marketing lists may supply socially excessive information to some buyers, a possibility absent from the data-appends literature the paper compares against, where provision can only be insufficient. Proposition 1 isolates the mechanism: the prior decides whether information mainly prevents wasteful targeting or restores profitable targeting, and the cost of acting amplifies one or the other.

The result is proved in the paper; nothing in it has been machine-checked. The mission produces a checked version of the two-type screening reduction (including the verification that the constraints dropped in (7) hold at its solutions, which the paper asserts as standard) and of the comparative statics with set-valued optima, since $k$ is not assumed convex and optima need not be unique.

Difficulty

The derivative computations are routine once $\sigma_h(\alpha)v_h(\alpha)$ is simplified to $\phi\alpha\bar u+(1-\phi)(1-\alpha)\underline u$. The work lies elsewhere. First, the reduction: "IR binds for the high-cost type and IC binds for the low-cost type" is the standard heuristic, but at a solution of (7) one still has to check the dropped constraint IC$_{H,L}$ and the nonnegativity $T_L\ge0$; both depend on the ordering of $\alpha_H$ and $\alpha_L$ at the optimum, which in turn depends on the sign of $1-2\phi$. Second, strictness: comparative statics through increasing differences give only weak inequalities between maximizer sets. Upgrading $\alpha^*_H\ge\alpha^e_H$ to $\alpha^*_H>\alpha^e_H$ requires ruling out a common maximizer, which needs the optimum to be interior and $k$ differentiable there; the naive argument by first-order conditions fails at the corners $\underline\alpha,\bar\alpha$. Third, $\alpha^*_L=\alpha^e_L$ as sets requires existence of optimal menus, hence attainment of the maximum of (7).

Formalization scope

Everything is over $\mathbb R$. The model is a structure Model (values, prior, informativeness interval, selling cost) extended by Screening (type probability and the two costs); the standing assumptions $\underline u<\bar u$, $0<\phi<1$, $1/2<\underline\alpha<\bar\alpha<1$, $k(\underline\alpha)=0$, $k$ increasing on $[\underline\alpha,\bar\alpha]$ (weakly), $0<\theta<1$, $0<c_L<c_H$, and $v_l(\underline\alpha)<c_i<v_h(\underline\alpha)$ for both types are fields. The posteriors are defined with the divisions printed in (2). Efficient levels and optimal menus are sets of maximizers, never chosen by Classical.choose or a first-order condition. Menus include $T_j\ge0$.

The goal additionally assumes the part of footnote 5 (p. 7) that makes optima interior: $k$ continuous on $[\underline\alpha,\bar\alpha]$, differentiable on $(\underline\alpha,\bar\alpha)$, with right derivative $k'(\underline\alpha)=0$ and $k'(\alpha)\to+\infty$ as $\alpha\to\bar\alpha^-$. Convexity and twice differentiability, also in the footnote, are not assumed. The milestones carry no regularity beyond differentiability at the point considered (milestones 1, 5) and continuity for the optimality characterization in milestone 4.

The optimal menu is a maximizer of (6) under all four constraints, not a maximizer of (7): defining it through (7) would make half of the goal immediate and skip the reduction.

The development needs the algebra of the binary posterior, the two-type screening reduction, and a strict version of monotone comparative statics; Topkis's theorem on strictly increasing differences (Theorem 2.8.4) is already proved on the platform and referenced. Proofs of any milestone, and alternative arguments for the strict inequalities, are welcome.

Selected references

• L. Guo, Selling Data to Marketers, Management Science, 2025 (author's manuscript). https://doi.org/10.1287/mnsc.2023.01350
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539
• M. Mussa and S. Rosen, Monopoly and Product Quality, Journal of Economic Theory 18(2), 1978. https://doi.org/10.1016/0022-0531(78)90085-6
• E. Maskin and J. Riley, Monopoly with Incomplete Information, RAND Journal of Economics 15(2), 1984. https://doi.org/10.2307/2555674
• Federal Trade Commission, Data Brokers: A Call for Transparency and Accountability, 2014. https://www.ftc.gov/reports/data-brokers-call-transparency-accountability-report-federal-trade-commission-may-2014

Motivation

Data brokers sell consumer data to firms that use it to decide whom to target, whom to lend to, or where to open a store. Two kinds of products are common: a marketing list, which supplies contact information without which the buyer cannot act at all, and a data append, which enriches information about consumers the buyer can already reach (Federal Trade Commission, Data Brokers, 2014). A seller who does not know a buyer's cost of acting must screen buyers with a menu of plans that differ in price and in how informative the data are.

Liang Guo's paper Selling Data to Marketers (Management Science, doi:10.1287/mnsc.2023.01350) characterizes the optimal menu, first for a binary-value model (§3) and then for a general information structure ordered by rotation (§4), following Johnson and Myatt (2006). This mission formalizes Proposition 7: data appends under the rotation order. It is the fourth mission of a series built from the same manuscript; the first three cover marketing lists and data appends in the binary model and marketing lists under the rotation order.

Setting

A marketer can take an action (target a consumer) at cost $c$; the action's value $u$ is uncertain with prior mean $\hat u$. A data service of informativeness $\alpha\in[\underline\alpha,\bar\alpha]\subset(0,1)$ produces a signal, and its information is summarized by the posterior mean $v$. For each $\alpha$, $v$ has cumulative distribution function $H(v,\alpha)$ on a support $[\underline v,\bar v]$, with a strictly positive density $h(v,\alpha)$ and mean $\hat u$ for every $\alpha$. The family is rotation ordered: there is a point $v^+\in(\underline v,\bar v)$ with

$$\frac{\partial H(v,\alpha)}{\partial\alpha}>0 \ (v<v^+),\qquad \frac{\partial H(v,\alpha)}{\partial\alpha}<0 \ (v>v^+).$$

A more informative service spreads the posterior mean away from $\hat u$.

A service plan $(T,\alpha)$ charges a fixed fee $T\ge0$. Serving a marketer with informativeness $\alpha$ costs the seller $k(\alpha)$, with $k(\underline\alpha)=0$ and $k$ increasing. A marketer targets exactly when $v>c$, so a marketer with cost $c_i$ who buys $(T_j,\alpha_j)$ earns

$$U_{ij}=-T_j+\int_{c_i}^{\bar v}(v-c_i)\,dH(v,\alpha_j).$$

Costs are $c_H$ with probability $\theta\in(0,1)$ and $c_L$ with probability $1-\theta$, $0<c_L<c_H$. A data-append buyer can act without the data, so its outside option is $U_{i0}=\max\{\hat u-c_i,0\}$.

The seller offers a menu $(T_H,\alpha_H),(T_L,\alpha_L)$ and maximizes $\Pi=\theta[T_H-k(\alpha_H)]+(1-\theta)[T_L-k(\alpha_L)]$ subject to individual rationality $U_{ii}\ge U_{i0}$ and incentive compatibility $U_{ii}\ge U_{ii'}$ for both types. Call any maximizer an optimal menu, with levels $\alpha^*_H,\alpha^*_L$. The benchmark with observable costs is

$$\max_{\alpha\in[\underline\alpha,\bar\alpha]}\ \theta_i\Big[\int_{c_i}^{\bar v}(v-c_i)\,dH(v,\alpha)-k(\alpha)\Big],$$

and its maximizers are the efficient levels $\alpha^e_i$.

Formalization targets

Goal: Proposition 7

Assume $c_L<c_H<\hat u$. If $c_L<c_H<v^+$, then

$$\alpha^*_H=\alpha^e_H,\qquad \alpha^*_L<\alpha^e_L ,$$

and if $v^+<c_L<c_H$, then

$$\alpha^*_H=\alpha^e_H,\qquad \alpha^*_L>\alpha^e_L .$$

Here $\alpha^*_H=\alpha^e_H$ means that the set of $\alpha_H$-levels of optimal menus equals the set of efficient levels, and each strict inequality holds for every optimal menu and every efficient level.

Milestones

1. The willingness to pay for a data append (p. 20): for $c\le\hat u$, $U_{ij}-U_{i0}=-T_j+\int_{\underline v}^{c_i}(c_i-v)\,dH(v,\alpha_j)$, which is increasing in $c_i$.
2. Its integrated form (proof of Proposition 8, p. 33): $U_{ij}-U_{i0}=-T_j+\int_{\underline v}^{c_i}H(v,\alpha_j)\,dv$.
3. The reduction (15) (p. 20): substituting the binding $IR_L$ and $IC_{H,L}$ turns the screening problem into a maximization over $(\alpha_H,\alpha_L)$.
4. (15) integrated by parts, and $\alpha^*_H=\alpha^e_H$ for it (p. 33).
5. The derivative $\partial\Pi/\partial\alpha_L$ of (15) compared with the benchmark's (p. 33).

Significance

Proposition 7 is the general-distribution form of a "double reversal". With marketing lists the low-cost marketers are the high type: they get efficient information, and the high-cost marketers' information is distorted (Proposition 5 of the paper). With data appends and costs below the prior mean, the outside option makes the high-cost marketers value data more. The roles of the types swap, and the direction of the distortion flips with the position of the costs relative to the rotation point. The result tells a data seller which customers to under- or over-supply, and shows that the answer depends on whether its data enable an action or only refine it.

The paper proves the result on a few pages, partly by phrases such as "it can be readily verified". No machine-checked version exists. A formalization makes explicit what the printed argument leaves implicit: that the dropped constraints hold at the reduced optimum, which regularity of $k$ and $H$ the strict inequalities need, and that statements about "the" optimum hold for every optimum when maximizers are not unique.

Difficulty

The obvious approach substitutes the binding constraints and compares first-order conditions. Two steps of it fail as stated. First, the reduction to (15) drops $IR_H$ and $IC_{L,H}$; $IC_{L,H}$ holds at a maximizer of (15) only when the two informativeness levels are ordered as the rotation order dictates. That ordering is available only when both costs lie on the same side of $v^+$. Second, first-order conditions say nothing at a corner of $[\underline\alpha,\bar\alpha]$. The strict comparison $\alpha^*_L\ne\alpha^e_L$ needs the efficient level to be interior, where the derivative of $k$ exists. That comes from the conditions of footnote 5 together with the mean-preserving property of the family. The selling cost need not be convex, so maximizers can be non-unique, and every comparison must hold for every pair of maximizers.

Formalization scope

• Information structure. A structure RotationFamily with a bounded support $\underline v<\bar v$ (the paper allows an unbounded one). $H(\cdot,\alpha)$ is continuous on $[\underline v,\bar v]$ with $H(\underline v,\alpha)=0$, $H(\bar v,\alpha)=1$ and derivative $h(\cdot,\alpha)>0$, continuous on the closed support. $\partial H/\partial\alpha$ exists on the closed support. The rotation order (9) holds on the open support, and the mean is $\hat u$ for every $\alpha\in(0,1)$. Condition (10) is not assumed; it follows.
• Model. Model extends it with $0<\underline\alpha<\bar\alpha<1$, $\theta\in(0,1)$, and $0<c_L<c_H$ with both costs in $(\underline v,\bar v)$ (a pin: the integrals $\int_{c_i}^{\bar v}$ presume it). It also fixes $k(\underline\alpha)=0$ with $k$ monotone on $[\underline\alpha,\bar\alpha]$. $dH$ is written as $h\,dv$.
• Objects of the goal. Optimal menus are maximizers of the full problem: fees $T\ge0$, levels in $[\underline\alpha,\bar\alpha]$, $IR_i$ with outside option $\max\{\hat u-c_i,0\}$, and both IC constraints. Efficient levels are maximizers of the benchmark (12). Neither is defined through (15) or a first-order condition. That would make the first half of the goal a restatement of milestone 4, and writing the outside option as $\hat u-c$ instead of the maximum would change the model.
• Pinned hypotheses. On the goal only: the part of footnote 5 the strict results use ($k$ continuous on $[\underline\alpha,\bar\alpha]$, differentiable inside, $k'(\underline\alpha)=0$ from the right, $k'(\alpha)\to+\infty$ as $\alpha\to\bar\alpha^-$) and joint continuity of $\partial H/\partial\alpha$ on $[\underline v,\bar v]\times(0,1)$. The derivative milestone uses only the latter. Convexity of $k$ is not assumed.
• Range restriction. The first sentence of Proposition 7 ($\alpha^*_H=\alpha^e_H$) is posed on the full problem only within the two ranges $c_H<v^+$ and $v^+<c_L$. For (15) it is posed without restriction in milestone 4. The branch $v^+<c_L<c_H<\hat u$ is empty when $v^+\ge\hat u$, for example for symmetric structures; non-symmetric rotation families with $v^+<\hat u$ inhabit it.
• Reuse. Topkis's monotonicity theorem (Theorem 2.8.4) is on the platform and is the tool the paper invokes. The integration-by-parts facts for distribution functions on a bounded support, and differentiation of $\int_c^{\bar v}H(v,\alpha)\,dv$ in $\alpha$, are reusable beyond this mission. Proofs of the milestones in any order are welcome.

Selected references

• Liang Guo, Selling Data to Marketers, Management Science, 2025 (author's manuscript used here). https://doi.org/10.1287/mnsc.2023.01350
• Justin P. Johnson and David P. Myatt, On the Simple Economics of Advertising, Marketing, and Product Design, American Economic Review 96(3), 2006. https://doi.org/10.1257/000282806777211946
• Donald M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539
• Federal Trade Commission, Data Brokers: A Call for Transparency and Accountability, 2014. https://www.ftc.gov/reports/data-brokers-call-transparency-accountability-report-federal-trade-commission-may-2014

Why this market matters

An intermediary such as a ride platform must attract buyers and sellers who arrive at different times. A buyer may wait for a seller; a seller may wait for a buyer. Both sides can choose when to request a match, so an ask price and a bid price affect participation as well as the intermediary's margin. Chen and Hu study whether a simple posted-price policy remains profitable despite this waiting and the uncertainty of arrivals. Their submitted manuscript proves a finite-market guarantee and an asymptotic rate for the policy used here. The proof appears in its Supplemental Note, while the model and theorem are in the main text.

Market and benchmarks

Buyers arrive during a horizon $[0,T]$ as a Poisson process of rate $\lambda^d>0$, and sellers arrive independently at rate $\lambda^s>0$. A buyer's valuation $v$ has density $f^d$ on $[\underline v,\overline v]$ and a seller's cost $c$ has density $f^s$ on $[\underline c,\overline c]$. Marks are independent of arrival times. A buyer and a seller each trade at most one unit. If they wait after arrival, they incur costs $b$ and $h$ per unit time, respectively. The paper assumes regularity: the buyer's virtual value $V^d(v)=v-\bar F^d(v)/f^d(v)$ and the seller's virtual cost $V^s(c)=c+F^s(c)/f^s(c)$ are weakly increasing on their supports. Here $\bar F^d=1-F^d$.

A clairvoyant assignment knows all arrivals through $T$. For each possible buyer–seller pair it assigns virtual surplus $V^d(v)-V^s(c)$ less the waiting cost determined by their arrival order. It chooses a partial matching with greatest total value, denoted $\bar J(H^T)$. A separate fluid program chooses a measurable, nonnegative pair of price trajectories that clears demand and supply at every time. Its optimal value is $\bar J^*$. These are different objects: $\bar J(H^T)$ is random and uses indivisible agents, whereas $\bar J^*$ is a deterministic continuous-flow optimum. Lemma 2 of the manuscript compares their values in expectation.

Let $\mu^*$ be the greatest volume in $[0,\min\{\lambda^dT,\lambda^sT\}]$ with nonnegative marginal virtual surplus. The buyer and seller prices $p^*,w^*$ are inverse-distribution prices at that volume. Proposition 1 states that these constant prices attain the fluid optimum and $\bar J^*=(p^*-w^*)\mu^*$.

Formalization targets

The greedy matching policy pairs requests first come, first served. Under the waiting-adjusted fixed-price policy, a buyer's posted ask is $p^*$ minus $b$ times a conditional expected wait per match probability; the seller's posted bid is $w^*$ plus the corresponding $h$ term. The buyer adjustment is conditioned on the observed pre-arrival inventory signal. Agents request immediately exactly when their valuation or cost crosses the base-price threshold. The policy's expected profit $J$ is computed from posted prices paid by successfully matched agents.

The first target is the paper's finite-market bound:

$$\frac{J}{\bar J^*}\ge 1-\left(1+\frac{2(b+h)T}{3(p^*-w^*)}\right)\frac{1}{\sqrt{\mu^*}}.$$

When $J\ge0$, the benchmark comparison also gives $J/\mathbb E[\bar J(H^T)]\ge J/\bar J^*$. For scaled systems with arrival rates $n^{\alpha_d}\lambda^d$ and $n^{\alpha_s}\lambda^s$, where both exponents are positive, the second target is a constant $C$ independent of $n$ such that

$$\frac{J^{(n)}}{\bar J^{*,(n)}}\ge 1-\frac{C}{\sqrt{n^{\min\{\alpha_d,\alpha_s\}}}}\qquad(n\ge1).$$

The milestone list follows the source's Proposition 1, Lagrangian relaxation, Lemma 2, Poisson request counts, policy profit identity, Gallego–van Ryzin moment bound, and Lemma S.5 on arrival-rate monotonicity. The last three supply the finite bound and its scaling statement in the Supplemental Note.

What the result gives

The finite bound quantifies the cost of using fixed base prices and greedy matching instead of the fluid ideal. Its two terms separate the loss from random mismatch and the extra waiting adjustment. The scaled bound says that, as both sides' arrival rates grow, the fraction of the fluid value lost by this policy vanishes at a rate governed by the slower-growing side. This offers a concrete reason to use a simple policy when the market is large, while keeping the smaller-market correction visible.

The paper already proves these claims. This mission asks for machine-checked proofs of their precise statements. The fluid optimizer, the clairvoyant matching problem, the marked Poisson arrival model, and the policy-profit identity are reusable mathematical objects beyond this theorem. The positive-part moment bound is an already published theorem and is referenced rather than posed again.

Where the argument is difficult

The obvious comparison between posted-price profit and fluid revenue misses the cost of requests that wait or never match. The price corrections themselves are conditional expectations divided by conditional match probabilities; their effect cannot be captured by simply subtracting a constant waiting charge. The proof must connect those corrections to the time integral of the queue imbalance, then control the imbalance of two Poisson request streams. A second difficulty is that the fluid optimum and the expected clairvoyant optimum are defined through different feasible sets, so their comparison needs a separate relaxation argument. These obstacles are visible in the source's proof of Lemma 2 and Theorem 2.

Formalization scope

The density and virtual-value environment is the published bilateral-trade definition, imported through a local name alias required by the frozen shared market module. Lean represents arrivals by independent Poisson counts and independent identically distributed time-and-value marks. This is equal in law to the paper's homogeneous marked Poisson processes on $[0,T]$. Arrival time marks are uniform probability laws, and valuation and cost marks use the source densities. Simultaneous requests are ordered by index; such ties have probability zero. The deterministic program ranges over measurable, nonnegative, market-clearing paths with interval-integrable objective terms. Its value is the supremum of their objectives, not a formula involving $p^*$ and $w^*$; Proposition 1 must establish that formula. The clairvoyant value uses the published partial-assignment-game worth, so negative-weight pairs may remain unmatched.

The density functions are continuous on their supports, an explicit addition needed for the inverse prices and maximum volume used by Proposition 1. The lower support endpoints are nonnegative so the constant prices belong to the nonnegative fluid price domain; this fills an implicit domain convention in the manuscript. For Theorem 2 the overlap condition is strict, $\underline c<\overline v$, ensuring positive $\mu^*$ and $p^*-w^*$. The printed chain comparing $J/\mathbb E[\bar J]$ and $J/\bar J^*$ is stated under $J\ge0$: when the numerator is negative, the claimed direction fails. Both expectations used as finite numbers are accompanied by integrability conclusions. Division by a zero match probability at the terminal time uses a zero convention on a set of arrival times with probability zero.

The policy model builds in the myopic request behavior that Theorem 1 identifies as an equilibrium; its strategic proof is outside this mission. The policy profit is the expectation of actual posted-price payments, and the waiting compensations are literal tagged-arrival conditional ratios. Contributions that prove the inverse-distribution properties, Poisson thinning, queue profit identity, fluid optimization, or final moment estimate all address parts of the stated target.

Selected references

• Y. Chen and M. Hu, Pricing and Matching with Forward-Looking Buyers and Sellers, Manufacturing & Service Operations Management 22(4), 2020; submitted manuscript, SSRN 2859864.

Motivation

In a labor market where firms hire sets of workers and salaries are negotiated pair by pair, the natural stability notion is the core: an assignment of workers to firms, with salaries, that no firm and group of workers can improve upon by agreeing among themselves. Kelso and Crawford (Econometrica 50 (1982) 1483–1504) proved that the core is nonempty, and that an ascending salary-adjustment process reaches it, when every firm regards workers as gross substitutes (GS): raising some workers' salaries never makes a firm withdraw an offer from a worker whose salary has not risen. The condition later became central to the theory of matching with contracts, combinatorial auctions and Walrasian equilibrium with indivisible goods (Gul and Stacchetti, J. Econ. Theory 87 (1999); Hatfield and Milgrom, Amer. Econ. Rev. 95 (2005)).

The question this mission addresses is whether (GS) is needed at all. Section 6 of the paper answers it with a concrete market with two firms and three workers in which every other assumption of the paper holds, each firm's technology is even subadditive, and the core is empty.

Setting

There are workers $i \in W$ and firms $j \in F$, both finite. Worker $i$'s utility of working for firm $j$ at salary $s$ is $u^i(j; s)$; firm $j$ produces $y^j(C)$ with the set of workers $C$, and its profit at the salary vector $s^j = (s_{ij})_i$ is

$$\pi^j(C; s^j) = y^j(C) - \sum_{i \in C} s_{ij}.$$

A set $C$ is demanded at $s^j$ if it maximizes $\pi^j(\cdot\,; s^j)$. Each pair has a reservation salary $\sigma_{ij}$.

An allocation assigns each worker $i$ to a firm $f(i)$ with salary $s_{if(i)}$; $C^j = f^{-1}(j)$. It is individually rational if $s_{if(i)} \ge \sigma_{if(i)}$ and $\pi^j(C^j; s^j) \ge 0$ for all $i$, $j$. A firm $j$ and a set $C$ of workers strictly improve upon it if some salaries $r_{ij}$ give every $i \in C$ strictly more utility than at the allocation and give firm $j$ strictly more profit than $\pi^j(C^j; s^j)$. A core allocation (definition D3 of the paper) is an individually rational allocation that no such coalition can strictly improve upon. When salaries vary continuously, the $r_{ij}$ range over $\mathbb{R}$.

The example. Workers $1, 2, 3$; firms $j, k$; $\sigma_{ij} = \sigma_{ik} = 0$; $u^i(j; s) = u^i(k; s) = s$ (equation (23)); and

$C$	$\emptyset$	$\{1\}$	$\{2\}$	$\{3\}$	$\{1,2\}$	$\{1,3\}$	$\{2,3\}$	$\{1,2,3\}$
$y^j(C)$	$0$	$4$	$4$	$4\tfrac14$	$7\tfrac12$	$7$	$7$	$9$
$y^k(C)$	$0$	$4\tfrac14$	$4$	$4$	$7$	$7$	$7\tfrac12$	$9$

Firm $k$ is firm $j$ with workers $1$ and $3$ interchanged. In Lean, noCoreMarket : Market (Fin 3) (Fin 2) is this market, techJ and techK are the two technologies, and Market.IsCore anySalary is D3 with real salaries.

Formalization targets

Goal: the example has no core allocation

$$\neg\,\exists A,\ A \text{ is a core allocation of the example with continuously variable salaries.}$$

Milestones, in the order the paper uses them

1. At $s^j = (3,3,3)$ firm $j$'s unique demanded set is $\{1,2\}$ (profit $1\tfrac12$); at $\tilde s^j = (3,4,3)$ it is $\{3\}$ (profit $1\tfrac14$).
2. Firm $j$'s technology is subadditive and satisfies (MP) and (NFL) with $\sigma_{ij} = 0$, but violates (GS).
3. In any market with $u^i(j; s) = s$ and $\sigma = 0$, every core allocation maximizes total product $\sum_j y^j(f^{-1}(j))$ over all assignments.
4. In the example the maximal total product is $11\tfrac12$, attained exactly by $j \leftarrow \{1\},\ k \leftarrow \{2,3\}$ and by $j \leftarrow \{1,2\},\ k \leftarrow \{3\}$.
5. For the first of these assignments, if the coalitions $(j;\{3\})$, $(j;\{1,2\})$, $(k;\{1\})$, $(k;\{3\})$ cannot strictly improve, inequalities (24)–(27) hold.
6. Hence the first assignment carries no core allocation ($s_{2k} = 3\tfrac12$ is forced and (24′), (26′) contradict each other).

The goal then follows by the symmetry of the example.

Significance

The paper's existence results (Theorems 1 and 2: the salary-adjustment process converges to a core allocation; a strict core allocation exists with continuous salaries) all assume (GS). This example shows that the assumption cannot simply be dropped, and that the weaker and more familiar condition of subadditivity does not replace it once there are three or more workers, although it does with two (p. 1500). It is the reason gross substitutes, rather than a convexity-like condition on technologies, became the standard hypothesis for existence of equilibrium with indivisibilities.

The result is proved in the paper by a short computation. It has not been machine-checked before: nothing of this paper was on Prove2Me before this series. The mission contributes a checked counterexample, a general efficiency lemma for core allocations with transferable utility (milestone 3), and the computational facts about firm $j$ that show (GS) fails. The paper's further remark that the example also has no competitive equilibrium relies on the core–equilibrium equivalence of p. 1487 and is not part of this mission.

This is mission 7 of a series on the same paper; missions 1–6 treat the salary-adjustment process (1), the continuous strict core (2), one-sided markets (3), the firm-optimal allocation (4), comparative statics (5) and the characterization of (GS) for identical workers (6). This mission does not depend on them.

Difficulty

The obstacle is the quantifier over all allocations with real salaries: emptiness of the core is a claim about infinitely many candidates, and checking finitely many salary vectors proves nothing. A direct attempt to find an improving coalition for each allocation by case analysis on salaries does not close, because which coalition improves depends on the salaries. The printed inequality (24) also carries a sign misprint ($\le$ in place of $\ge$), and copying it would break the contradiction.

Formalization scope

• Workers $1,2,3$ are 0, 1, 2 : Fin 3; firms $j, k$ are 0, 1 : Fin 2. $4\tfrac14 = 17/4$ and $7\tfrac12 = 15/2$.
• An allocation is a total function from workers to firms with each worker's salary at his or her own firm; every worker is employed, as in D1. Individual rationality is part of "core allocation".
• "Core" is D3 (no coalition can strictly improve), with real salaries ("when salaries can vary continuously"), not the strict core D2 and not a discrete grid.
• "Unique preferred set" is stated as: a set is profit-maximizing over all eight subsets iff it equals the named set.
• (GS) "fails" is the negation of (GS) for firm $j$ over all real salary vectors.
• Inequality (24) is formalized as $4 - s_{1j} + s_{3k} \ge 4\tfrac14$, the reading the paper's own (24′) requires; the milestone text keeps the printed version.
• Milestone 3 is stated for every finite market with $u^i(j; s) = s$ and $\sigma = 0$, the two properties the paper's sentence invokes.

A trivializing formalization is ruled out: the core includes individual rationality and real-valued coalition salaries, the technologies are the printed tables, milestones 1, 2 and 4 have no hypotheses, and the hypotheses of milestones 3 and 5 are each satisfiable.

Contributions welcome: proofs of each milestone, and a statement and proof of the symmetry (workers $1 \leftrightarrow 3$, firms $j \leftrightarrow k$) used to exclude the second efficient assignment.

Selected references

• A. S. Kelso, Jr. and V. P. Crawford, Job matching, coalition formation, and gross substitutes, Econometrica 50(6), 1982, 1483–1504. https://doi.org/10.2307/1913392
• V. P. Crawford and E. M. Knoer, Job matching with heterogeneous firms and workers, Econometrica 49(2), 1981, 437–450. https://doi.org/10.2307/1913320
• L. S. Shapley and M. Shubik, The assignment game I: the core, International Journal of Game Theory 1, 1971, 111–130. https://doi.org/10.1007/BF01753437
• F. Gul and E. Stacchetti, Walrasian equilibrium with gross substitutes, Journal of Economic Theory 87, 1999, 95–124. https://doi.org/10.1006/jeth.1999.2531
• J. W. Hatfield and P. R. Milgrom, Matching with contracts, American Economic Review 95(4), 2005, 913–935. https://doi.org/10.1257/0002828054825466

Motivation

A committee that chooses one alternative by voting would like a procedure under which nobody gains by misreporting their preferences. Gibbard (Econometrica 41, 1973) and Satterthwaite (J. Econ. Theory 10, 1975) showed that, once at least three outcomes are possible, the only voting procedures with this property are dictatorial. The theorem is the starting point of the theory of strategy-proof mechanisms and of implementation theory.

Most proofs, including the main argument of Satterthwaite's paper, assume strict ballots: no voter is indifferent between two distinct alternatives. Real ballots, and most economic models of preferences, allow indifference. The last section of Satterthwaite's paper carries the theorem over to ballots that are arbitrary weak orders, by decomposing a voting procedure into a tie-breaking function followed by a strict voting procedure. This mission formalizes that extension.

Timeline. Gibbard (1973) proved the impossibility for game forms; the 1974 discussion paper formalized here proved it for strict ballots by induction on the number of voters (Theorem 1), allowing the range of the procedure to be a proper subset of the alternatives, and extended it to weak orders (Theorem 1′). Later short proofs (Barberà 1983; Benoît 2000; Reny 2001) also treat strict ballots.

Setting

A committee is a finite set $I_n$ of $n$ individuals and a finite set $S_m$ of $m$ alternatives. A weak order $R$ on $S_m$ is a complete and transitive relation, with $x\,R\,y$ read "$x$ is preferred or indifferent to $y$"; its strict part is $x\,\bar R\,y$ iff $x\,R\,y$ and not $y\,R\,x$. The weak orders form $\pi_m$. A strong order is a weak order with no indifference between distinct alternatives; the strong orders form $\rho_m\subseteq\pi_m$. A ballot set is $B=(B_1,\dots,B_n)\in\pi_m^n$.

A voting procedure is a map $v:\pi_m^n\to S_m$. Its range is $T_p=v(\pi_m^n)$, with $p=|T_p|$. A strict voting procedure is a map $\nu:\rho_m^n\to S_m$.

$v$ is strategy-proof if there are no ballot set $B$, individual $i$ and ballot $B_i'\in\pi_m$ with

$$v(B_1,\dots,B_i',\dots,B_n)\ \bar B_i\ v(B_1,\dots,B_i,\dots,B_n).$$

For a strict procedure, ballot sets and substituted ballots are strong orders.

$v$ is dictatorial if some individual $i$ exists such that, for every ballot set $B$, the outcome $v(B)$ is among the $B_i$-maximal elements of $T_p$: $v(B)\,B_i\,y$ for all $y\in T_p$.

A tie-breaking function is a map $\alpha:\pi_m^n\to\rho_m^n$ that keeps every strict preference: if $C=\alpha(B)$ then $x\,\bar B_i\,y$ implies $x\,\bar C_i\,y$. It is regular if there are fixed strong orders $Q_1,\dots,Q_n$ such that every indifference $x\,B_i\,y$, $y\,B_i\,x$ is broken as $Q_i$ breaks it.

Formalization targets

Goal: Theorem 1′ (p. 43)

For $n\ge 2$ and $m\ge p\ge 3$, every strategy-proof voting procedure on weak-order ballots is dictatorial:

$$v \text{ strategy-proof},\ |T_p|\ge 3 \ \Longrightarrow\ \exists\, i\ \forall B\in\pi_m^n\ \forall y\in T_p:\ v(B)\,B_i\,y.$$

The converse fails once indifference is admissible: a dictator's ties may be broken by a manipulable rule, such as a Borda count of the other ballots (pp. 10–11). The goal is therefore a one-way implication.

Milestones

1. Theorem 1 (p. 11), the strict case: for $n\ge 1$ and $p\ge 3$, a strict voting procedure is strategy-proof if and only if it is dictatorial.
2. Lemma 9, first sentence (p. 41): if $v=\nu\circ\gamma$ with $\nu$ strict and strategy-proof and $\gamma$ a regular tie-breaking function, then $v$ is strategy-proof.
3. Lemma 9, second sentence (p. 41): every strategy-proof $v$ can be written $v=\nu\circ\alpha$ with $\nu$ strict and strategy-proof and $\alpha$ a tie-breaking function, not necessarily regular.

Significance

The result shows that allowing voters to express indifference does not escape the Gibbard–Satterthwaite impossibility: the dictatorial conclusion survives, and only the equivalence is lost. It is the form of the theorem most directly applicable to economic environments, where preference domains usually contain indifference, and the decomposition of Lemma 9 is the device by which strict-ballot results are transferred to weak-order ballots throughout §6 of the paper, including the weak-order version of Arrow's theorem.

The theorem is proved and classical. What is not yet available is a machine-checked proof of the weak-order version with a range that may be a proper subset of the alternatives. The strict, full-range case is proved on the platform (AGT.gibbard_satterthwaite, on strict total orders with a surjective rule); the strict case with an arbitrary range of size at least three is the goal of the companion mission on strict committees. This mission adds the decomposition of Lemma 9 and the extension to indifference.

Difficulty

The obvious route is to restrict a strategy-proof $v$ to strict ballot sets, apply the strict theorem, and conclude. Two steps fail. First, the restriction's range may a priori be smaller than $T_p$, so the hypothesis $p\ge 3$ need not transfer. Second, knowing that $v$ is dictatorial on strict ballot sets says nothing directly about ballot sets with indifference: one needs, for each $B$, a strict refinement $C$ of $B$ with $v(C)=v(B)$, and the refinement of one individual's ballot may depend on the others' ballots. Lemma 9's second sentence is exactly the existence of such refinements, and the tie-breaking function it produces is generally not regular.

Formalization scope

Lean commits to the following conventions, all in the definitions file StrategyProofArrow.WeakGS.Basic:

• Individuals and alternatives are finite types ι and A; $n$ and $m$ are their cardinalities. The theorems state $n\ge 1$ or $n\ge 2$ as printed, and $m\ge 3$ where the paper's standing committee assumption is all that applies (Lemma 9). $m\ge p$ is automatic.
• A weak order is a structure (relation, completeness, transitivity); strong orders are the subtype with no indifference between distinct alternatives, so a strict ballot is literally a weak ballot.
• Voting procedures are total functions on profiles of weak orders (resp. strong orders). There are no inadmissible inputs, and the range $T_p$ is Set.range v.
• Strategy-proofness compares outcomes by the strict part of the true ballot; the substituted ballot is any weak order (any strong order in the strict case).
• The paper defines dictatorship through a function $f^i_T$ that selects some $B_i$-maximal element of $T_p$ with an unspecified tie-break. Lean states the equivalent condition that $v(B)$ is $B_i$-maximal in $T_p$, without fixing a tie-break. Fixing one would make Theorem 1′ false.
• The tie-breaking condition is stated once for all $x,y$; the paper's two clauses are the same condition with $x,y$ renamed. $\alpha(B)_i$ may depend on all of $B$.
• In Lemma 9 the page prints the composition with a Latin $v$ on both sides; it is read as $\nu^{nm}[\gamma(B)]$, as the sentence and proof require.

A trivializing formalization would measure manipulation by the weak relation $B_i$ instead of its strict part, which makes "strategy-proof" nearly unsatisfiable and the goal vacuous; the definitions use the strict part, and a sorry-free check confirms that a strategy-proof procedure with range of size 3 exists.

A complete development needs the strict Gibbard–Satterthwaite theorem with partial range (milestone 1) and the refinement construction of Lemma 9. The weak-order and tie-breaking vocabulary is reusable for the weak-order Arrow theorem of the companion mission. Proofs of any milestone, and alternative proofs of the goal that bypass Lemma 9, are welcome.

Selected references

• M. A. Satterthwaite, Strategy-proofness and Arrow's Conditions: Existence and Correspondence Theorems for Voting Procedures and Social Welfare Functions, Northwestern University CMS-EMS Discussion Paper No. 122, rev. Dec. 12, 1974; J. Econ. Theory 10 (1975) 187–217. https://doi.org/10.1016/0022-0531(75)90050-2
• A. Gibbard, Manipulation of Voting Schemes: A General Result, Econometrica 41 (1973) 587–601. https://doi.org/10.2307/1914083
• S. Barberà, Strategy-Proofness and Pivotal Voters: A Direct Proof of the Gibbard–Satterthwaite Theorem, International Economic Review 24 (1983) 413–417. https://doi.org/10.2307/2648754
• J.-P. Benoît, The Gibbard–Satterthwaite Theorem: A Simple Proof, Economics Letters 69 (2000) 319–322. https://doi.org/10.1016/S0165-1765(00)00312-8
• P. J. Reny, Arrow's Theorem and the Gibbard–Satterthwaite Theorem: A Unified Approach, Economics Letters 70 (2001) 99–105. https://doi.org/10.1016/S0165-1765(00)00332-3

Motivation

An arbitrator who must choose among collective options for a group of players usually does not know the players' private characteristics. The arbitrator can only ask, and a player who expects to profit from a false answer may give one. Before designing any procedure, the arbitrator therefore needs to know which expected-payoff allocations can be reached at all once strategic misreporting is taken into account.

Myerson (1979) answers this for Bayesian collective choice problems with finitely many types. Restricting attention to mechanisms that simply ask each player for their type, and that make honest answers optimal, loses nothing: every expected-payoff allocation that any mechanism can produce in equilibrium is already produced honestly by such a direct mechanism, and conversely. This is the revelation principle in the form used throughout Bayesian mechanism design. It is what makes incentive-compatibility constraints the starting point for auction design, bilateral trade, and the bargaining solution in the second half of the same paper.

Timeline. Gibbard (1973) gave the dominant-strategy form of the principle. Rosenthal (Review of Economic Studies, 1978) studied arbitration of two-party disputes under uncertainty; Myerson notes that Theorem 2 could be derived as a corollary of Rosenthal's Theorem 3. Dasgupta, Hammond and Maskin (1979) gave general Bayesian implementation results in the same year. Myerson's Theorem 2 states the principle as an equality of interim payoff sets over all finite response sets. Myerson (1982) later extended it to principal–agent problems with moral hazard.

Setting

A Bayesian collective choice problem $(C,A_1,\dots,A_n,U_1,\dots,U_n,P)$ has a nonempty finite set of players $i$, a nonempty finite set $A_i$ of types for each player, a nonempty finite set $C$ of collective choices, utilities $U_i(c,\alpha)$ depending on the choice and on the true type profile $\alpha=(\alpha_1,\dots,\alpha_n)$, and a probability distribution $P$ on type profiles. With $R_i(a_i)=\sum_{\beta:\beta_i=a_i}P(\beta)$ the marginal of type $a_i$, a player of type $a_i$ assigns the conditional probability $P_i(\alpha\mid a_i)=P(\alpha)/R_i(a_i)$ to profiles with $\alpha_i=a_i$, and $0$ to the others.

A choice mechanism on response sets $S_1,\dots,S_n$ (nonempty finite sets of possible answers) is a function $\pi(c\mid s)\ge0$ with $\sum_{c}\pi(c\mid s)=1$ for every response profile $s$. On the standard response sets $S_i=A_i$, the payoff of type $a_i$ who reports $b_i$ while the others are honest is

$$Z_i(\pi,b_i\mid a_i)=\sum_\alpha\sum_{c}P_i(\alpha\mid a_i)\,\pi(c\mid\alpha_{-i},b_i)\,U_i(c,\alpha).$$

The mechanism is Bayesian incentive-compatible if $Z_i(\pi,a_i\mid a_i)\ge Z_i(\pi,b_i\mid a_i)$ for all $i,a_i,b_i$. Its honest allocation is the vector $V(\pi)$ with coordinates $V_i(\pi\mid a_i)=Z_i(\pi,a_i\mid a_i)$, indexed by the disjoint union of the $A_i$. The incentive-feasible set is

$$F^*=\{V(\pi):\pi\text{ a Bayesian incentive-compatible choice mechanism on the standard response sets}\}.$$

On general response sets, a response plan $\sigma_i(s_i\mid a_i)$ is a probability distribution over $S_i$ for each type $a_i$. Plans $\sigma=(\sigma_1,\dots,\sigma_n)$ give type $a_i$ the payoff

$$W_i(\pi,\sigma\mid a_i)=\sum_\alpha\sum_s\sum_c P_i(\alpha\mid a_i)\Big(\prod_{j}\sigma_j(s_j\mid\alpha_j)\Big)\pi(c\mid s)\,U_i(c,\alpha).$$

They form a response-plan equilibrium for $\pi$ if no type $a_i$ of any player gains by switching to any other response plan $\sigma_i'$. The equilibrium-feasible set $F^{**}$ collects $W(\pi,\sigma)$ over all choice mechanisms $\pi$, on all nonempty finite response sets, and all response-plan equilibria $\sigma$ for $\pi$.

Formalization targets

Goal: Theorem 2

$$F^{**}=F^*.$$

Both inclusions are asserted for every Bayesian collective choice problem. $F^{**}\subseteq F^*$ says equilibrium behaviour under any mechanism can be replicated honestly by an incentive-compatible direct mechanism. $F^*\subseteq F^{**}$ says honest reporting is itself an equilibrium of every incentive-compatible mechanism.

Milestones (the steps of the paper's proof)

1. For any choice mechanism $\pi$ and response plans $\sigma$, the induced direct mechanism $\pi'(c\mid\alpha)=\sum_s\pi(c\mid s)\prod_i\sigma_i(s_i\mid\alpha_i)$ is a choice mechanism and $V(\pi')=W(\pi,\sigma)$.
2. If $\sigma$ is a response-plan equilibrium for $\pi$, then $\pi'$ is Bayesian incentive-compatible.
3. If $\pi'$ is a Bayesian incentive-compatible choice mechanism, the honest plans $\sigma_i'(b_i\mid a_i)=\mathbf 1[b_i=a_i]$ form a response-plan equilibrium for $\pi'$, and $W(\pi',\sigma')=V(\pi')$.

Significance

The result. Theorem 2 reduces a search over all communication protocols, an unbounded family of response sets and mixed reporting behaviours, to a finite system of linear inequalities in $\pi$ on a fixed finite domain. Combined with Theorem 1 of the paper, which shows $F^*$ is a nonempty compact convex set, it justifies applying a bargaining solution to $F^*$ rather than to some larger, ill-defined set of attainable outcomes. The same reduction underlies the use of incentive constraints in optimal auctions, bilateral trade and correlated-type mechanism design.

Formalizing it. The result is classical and its proof is short, but it is a statement about all finite response sets at once, and the equality of two sets of payoff vectors is sensitive to the conventions: which plans are allowed as deviations, where the conditioning happens, and whether the induced mechanism is a genuine probability distribution. A machine-checked version pins these down. To our knowledge no formal proof of this finite Bayesian revelation principle exists. The platform has related, unproved items in other models: MechanismDesign.Robust.revelation_principle (Börgers, Prop. 10.2, on a countable Harsanyi type space with PMF lotteries; one inclusion, outcome equivalence) and single-agent, quasi-linear and dominant-strategy revelation principles from the same book. None of them is the statement here.

Difficulty

The mathematics consists of finite sums, but the bookkeeping is the obstacle. Milestone 1 requires exchanging a sum over response profiles with a product over players and using that each plan sums to one. Milestone 2 requires recognizing a lie $b_i$ in $\pi'$ as a particular whole response plan in $\pi$: the plan that, at every type, behaves as type $b_i$ would. Because $P_i(\alpha\mid a_i)$ vanishes off $\alpha_i=a_i$, only its value at $a_i$ matters. For milestone 3, a mixed deviation from honesty has to be bounded by the best pure misreport, a convex-combination argument over $A_i$. Identifying the $F^{**}$ side of the goal also needs instances on an existentially chosen family of types.

Formalization scope

All objects live in MyersonBargaining.Revelation. Players form a nonempty finite type ι; types A i, choices C and response sets S i are nonempty finite types in Type. Mechanisms and plans are real-valued functions with the probability constraints as predicates (IsChoiceMechanism, IsResponsePlan), event first and condition second: π c s, σ i s a. Allocation vectors are functions on Σ i, A i. The paper's loose phrases are read as follows:

• "probability distribution" means nonnegativity and sum one;
• (3) divides by $R_i(a_i)$, so the problem requires $R_i(a_i)>0$; individual profiles may have probability zero;
• the consistent (common-prior) reading of (3)–(4) is formalized, not the subjective reading the paper permits on p. 63;
• "for every possible alternative response plan" in (14) ranges over all mixed response plans, compared type by type;
• "$\pi$ is a choice mechanism" in (15) ranges over all nonempty finite response sets, with an explicit existential over the family S : ι → Type and its instances;
• "incentive-compatible mechanism" means a choice mechanism satisfying (6).

The product in (12) is printed with $\sigma_j(s_j\mid a_j)$; it is formalized with $\alpha_j$, as the paper's own induced mechanism on p. 66 uses. Milestone 1 is stated for arbitrary response plans, not only for equilibria. Section 6's numerical example is not formalized.

A trivializing formalization is ruled out explicitly: fixing $S_i=A_i$ in $F^{**}$, restricting deviations to pure plans, or stating only $F^{**}\subseteq F^*$ would each change the theorem, and none is done.

A complete development needs finite sums over dependent product types (Fintype.piFinset, Finset.prod_univ_sum), Function.update on dependent families, and nothing beyond Mathlib. The two definition modules (the model and the response-plan objects) are reusable by any finite Bayesian mechanism-design formalization. Proofs of any milestone, alternative proofs via Rosenthal's argument, and cleaner restatements as lemmas about stochastic matrices are welcome.

Selected references

• Roger B. Myerson, Incentive compatibility and the bargaining problem, Econometrica 47(1), 61–73, 1979. https://doi.org/10.2307/1912346
• Robert W. Rosenthal, Arbitration of two-party disputes under uncertainty, Review of Economic Studies 45(3), 1978 (cited in the source as reference [8], "forthcoming").
• Allan Gibbard, Manipulation of voting schemes: a general result, Econometrica 41(4), 587–601, 1973. https://doi.org/10.2307/1914083
• Partha Dasgupta, Peter Hammond, Eric Maskin, The implementation of social choice rules: some general results on incentive compatibility, Review of Economic Studies 46(2), 185–216, 1979. https://doi.org/10.2307/2297045
• Roger B. Myerson, Optimal coordination mechanisms in generalized principal–agent problems, Journal of Mathematical Economics 10(1), 67–81, 1982. https://doi.org/10.1016/0304-4068(82)90006-4