Motivation

Classical Bayesian mechanism design assumes that the designer knows the agents' beliefs about each other: typically a commonly known prior over independent private values. Wilson's critique (1987) observed that mechanisms tuned to such a prior can depend on details that no designer knows, and a literature on robust mechanism design replaced the fixed prior by a large family of possible beliefs. Chapter 10 of Börgers, An Introduction to the Theory of Mechanism Design (OUP 2015), develops this programme in the framework of Bergemann and Morris (2001, 2005): agents' information is described by a type space, the designer is uncertain which beliefs agents hold, and mechanisms are compared across all type profiles at once.

Timeline of the results formalized here:

• 1980: Hylland shows that strategy-proof random mechanisms satisfying unanimity conditions are random dictatorships; Dutta, Peters and Sen (2007, 2008) give and correct the cardinal version used in the chapter.
• 1985: Mertens and Zamir construct the universal type space of belief hierarchies; the space of finite types is emphasized by Dekel, Fudenberg and Morris (2006).
• 1988: Crémer and McLean show that with correlated types satisfying a spanning condition, beliefs can be elicited at no cost (Proposition 6.4 of the book).
• 2001–2005: Bergemann and Morris introduce payoff and belief types and prove that on finite type spaces only incentive constraints between types with the same beliefs matter (their Proposition 4.5, the goal of this mission).
• 2010–2014: Smith, Börgers and Smith study the ranking of mechanisms without a common prior; random dictatorship with compromise comes from Börgers and Smith (2012, 2014).

Setting

There are finitely many agents $i \in I$, and agent $i$ has a set $\Theta_i$ of payoff types. An outcome $x$ gives agent $i$ the utility $u_i(x,\theta)$, which may depend on all payoff types. A type space $\mathcal T = (T_i,\hat\theta_i,\hat\beta_i)_{i\in I}$ consists of nonempty sets $T_i$ of types, a payoff type map $\hat\theta_i : T_i \to \Theta_i$ and a belief map $\hat\beta_i : T_i \to \Delta(T_{-i})$, where $T_{-i} = \prod_{j\ne i}T_j$. Different types may share a payoff type and differ only in their beliefs, and vice versa. A common prior is a distribution $\mu$ on $T$ from which every type's belief is obtained by conditioning. A type space has a large variety of certainties if for every $\theta_i$ and $\theta_{-i}$ some type with payoff type $\theta_i$ is certain that the others' payoff types are $\theta_{-i}$. The space of finite types $\mathcal T^+$ collects every infinite hierarchy of beliefs ("I believe that you believe that …") that is generated by a type of some finite type space.

A mechanism $(S_1,\dots,S_N,g)$ has strategy sets $S_i$ and an outcome rule $g : S \to \Delta(X)$. Strategies $\sigma_i : T_i \to \Delta(S_i)$ form a Bayesian equilibrium if each type maximizes expected utility under its own belief; it is belief-independent if types with equal payoff types play alike, and ex post if each type's choice stays optimal when it becomes certain of the others' types. A direct mechanism asks agents for their types, a reduced direct mechanism only for their payoff types. In the quasi-linear case outcomes are $(a,t_1,\dots,t_N)$ and $u_i = v_i(a,\theta) - t_i$, with $t_i$ paid by agent $i$; a direct mechanism is $(q,t)$.

Formalization targets

Goal: belief revelation on finite type spaces (Proposition 10.6)

On a finite type space with quasi-linear utilities, suppose that for every agent no belief in $\{\hat\beta_i(\tau_i) : \tau_i\in T_i\}$ is a convex combination of the others, and that in the direct mechanism $(q,t)$ no type wants to imitate another type with the same belief. Then there is a direct mechanism $(\tilde q,\tilde t)$ in which truth telling is a Bayesian equilibrium, with

$$\tilde q(\tau) = q(\tau)\ \ \forall \tau\in T,\qquad \sum_{\tau_{-i}}\hat\beta_i(\tau_i)(\tau_{-i})\,\tilde t_i(\tau) = \sum_{\tau_{-i}}\hat\beta_i(\tau_i)(\tau_{-i})\, t_i(\tau)\ \ \forall i,\tau_i.$$

The goal fixes neither the transfers $\tilde t$ nor any bound on them; it asserts the existence of a truthful mechanism with the same alternatives and the same interim payments.

Milestones

The other fourteen numbered results of the chapter: conditional independence of payoff types under a full-support common prior (10.1); three revelation principles (10.2–10.4); existence of Bayesian equilibria of finite mechanisms on $\mathcal T^+$ (10.5); betting between agents with inconsistent beliefs (10.7); ex post implementation of unique equilibrium outcomes and alternatives (10.8, 10.9); emptiness of the set of undominated auctions under interim Pareto welfare and under ex post revenue (10.10, 10.11); Hylland's characterization of random dictatorship (10.12); and three comparisons of random dictatorship with random dictatorship with compromise (10.13–10.15).

Significance

Proposition 10.6 reduces the design problem on a finite type space to incentive constraints among types with the same beliefs: belief types can always be elicited by side payments that leave interim utilities unchanged. With a common prior and Proposition 10.1 this yields optimal mechanisms by solving an independent-types problem for each profile of belief types (§10.8; Farinha Luz 2013 carries this out for auctions). Proposition 10.7 and its consequences 10.10–10.11 show why the same construction cannot be used without a common prior: inconsistent beliefs allow unbounded bets, so interim or revenue criteria admit no undominated mechanism. Propositions 10.12–10.15 show that relaxing belief independence escapes Hylland's impossibility result in the voting problem.

None of these results is formalized elsewhere to our knowledge. The book proves only some of them (10.1, 10.5, 10.8, 10.9, 10.13–10.15 are proved or outlined; 10.6 is sketched; the proofs of 10.2–10.4 are omitted as standard; 10.7 and 10.10–10.12 are stated without proof), so formalization also produces complete proofs of results the book leaves informal. Two printed statements are corrected (see Formalization scope).

Difficulty

The obvious approach to Proposition 10.6 applies the Crémer–McLean construction type by type. This fails because several types may share a belief: a side payment that depends on the reported belief cannot separate them, and the convex-independence condition concerns the set of distinct beliefs rather than the indexed family of types.

For the results on $\mathcal T^+$, a type is an infinite belief hierarchy, and a strategy must be one function on all finite types simultaneously. Existence (10.5) cannot be obtained by applying Nash's theorem to a single finite type space, because a type belongs to many finite type spaces and must play the same strategy in all of them. Hylland's theorem (10.12) requires a full characterization of strategy-proof random rules on a cardinal preference domain.

Formalization scope

• Distributions $\Delta(X)$ are countably supported (PMF X); expected utilities are sums. The book leaves the measure structure of type spaces unspecified (p.179, note 3); finite type spaces, $\mathcal T^+$ and point beliefs are covered exactly. A Bayesian equilibrium requires every type's expected utility to exist (absolute summability) under every mixed strategy.
• A type's belief is a distribution on $\prod_{j\ne i}T_j$. Beliefs in Proposition 10.6 are vectors in $\mathbb R^{T_{-i}}$, and condition (i) is stated with the convex hull of the other distinct beliefs.
• Quasi-linear direct mechanisms are deterministic, $q : T\to A$, $t_i : T\to\mathbb R$. Mixed misreports are allowed in every equilibrium notion.
• $\mathcal T^+$ is built from belief hierarchies encoded level by level ($L_0 = \Theta_i$, $L_{n+1} = \Theta_i\times\Delta(\prod_{j\ne i}L_{n,j})$) and the finite type spaces generating them. The universal type space (Definition 10.5) is not needed and not formalized.
• §10.11: two agents Fin 2, candidates $\{a,b,c\}$, strict private vNM utilities with every strict utility attained; mechanisms map to lotteries over candidates; rankings are bijections C ≃ Fin 3.
• Corrections of the page: in Proposition 10.7 the signs of the transfers in (v) are reversed on the page relative to the bet described on p.186 and are stated as described; Proposition 10.9 is false under a large variety of certainties alone and is stated under the common-certainty condition that its proof uses, on type spaces whose beliefs have finite support (with countably supported beliefs the reduced mechanism's expected utilities need not exist). Both are explained in the item notes.
• The goal is not trivialized by taking $(\tilde q,\tilde t) = (q,t)$: condition (ii) constrains only types with the same belief, so the original mechanism is in general not incentive-compatible, and the conclusion demands full Bayesian incentive compatibility.

Welcome contributions: a finite Farkas/separation lemma in the form needed for 10.6 (the platform has Polyhedral.farkas_lemma), basic API for PMF-valued type spaces (products of mixed strategies, conditioning), and the hierarchy map of finite type spaces, which all $\mathcal T^+$ milestones share.

Selected references

• T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Ch. 10. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
• D. Bergemann, S. Morris, Robust Mechanism Design, Cowles Foundation Discussion Paper 1421, 2001; Econometrica 73 (2005) 1771–1813. https://doi.org/10.1111/j.1468-0262.2005.00638.x
• J. Crémer, R. McLean, Full Extraction of the Surplus in Bayesian and Dominant Strategy Auctions, Econometrica 56 (1988) 1247–1257. https://doi.org/10.2307/1913096
• J.-F. Mertens, S. Zamir, Formulation of Bayesian Analysis for Games with Incomplete Information, International Journal of Game Theory 14 (1985) 1–29. https://doi.org/10.1007/BF01770224
• B. Dutta, H. Peters, A. Sen, Strategy-Proof Cardinal Decision Schemes, Social Choice and Welfare 28 (2007) 163–179. https://doi.org/10.1007/s00355-006-0152-4
• T. Börgers, D. Smith, Robust Mechanism Design and Dominant Strategy Voting Rules, Theoretical Economics 9 (2014) 339–360. https://doi.org/10.3982/TE1100

Motivation

Voting rules, committee procedures and any other method that turns individual rankings into one collective choice face the same question: can the rule be designed so that no participant ever gains by misreporting their ranking? The Gibbard–Satterthwaite theorem (Gibbard, 1973; Satterthwaite, 1975) answers no. When at least three alternatives can be chosen and all strict rankings are admissible, the only rules immune to manipulation are dictatorships. The result is the starting point of mechanism design without money. It explains why the positive results of the transferable-utility chapters of the book (Groves, VCG, posted prices) depend on quasi-linear preferences, and why research on voting turned to restricted preference domains and weaker solution concepts.

This mission formalizes Chapter 8 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), §§8.2–8.3. The book's route to the theorem follows Reny (2001). Strategy-proofness implies Maskin monotonicity, and every monotone rule with full range over at least three alternatives is dictatorial. The second step is the Muller–Satterthwaite theorem (Muller and Satterthwaite, 1977), which is stronger than Gibbard–Satterthwaite because monotonicity is weaker than strategy-proofness. The chapter closes with the classical escape route: on single-peaked preferences (Moulin, 1980) the median voting rule is strategy-proof and not dictatorial.

Timeline. Arrow (1951/1963) proved the impossibility of non-dictatorial preference aggregation under independence of irrelevant alternatives. Gibbard (1973) and Satterthwaite (1975) proved the manipulation version independently, and Satterthwaite showed the two theorems are equivalent. Muller and Satterthwaite (1977) showed that on the full domain strategy-proofness is equivalent to a monotonicity condition (strong positive association). Moulin (1980) characterized strategy-proof rules on single-peaked domains that depend only on reported peaks. Reny (2001) gave the short common proof of Arrow's and the Muller–Satterthwaite theorems that the book follows.

Setting

There is a finite set $I=\{1,\dots,N\}$ of agents and a finite set $A$ of alternatives. Each agent $i$ has a preference relation $R_i$ over $A$; $a\,R_i\,b$ reads "$a$ is weakly preferred to $b$". Every $R_i$ is a linear order: complete, transitive, and the only indifference is among identical alternatives. Its strict part is $P_i$. The set of all linear orders over $A$ is $\mathcal R$, and a profile is $R=(R_1,\dots,R_N)\in\mathcal R^N$. $(R_i',R_{-i})$ is the profile obtained from $R$ by replacing agent $i$'s preference with $R_i'$.

A direct mechanism is a function $f:\mathcal R^N\to A$ (Definition 8.1). It is

• dominant strategy incentive-compatible (DSIC) if $f(R_i,R_{-i})\,R_i\,f(R_i',R_{-i})$ for all $i$, $R$, $R_i'$ (Definition 8.2);
• dictatorial if some agent $i$ satisfies $f(R)\,R_i\,a$ for all profiles $R$ and all $a\in A$ (Definition 8.3);
• monotone if $f(R)=a$ and, for every $i$, $a\,R_i\,b\Rightarrow a\,R_i'\,b$ for all $b$, together imply $f(R')=a$ (Definition 8.4);
• set-monotone if $f(R)\in B$ and, for every $i$, $R_i'$ differs from $R_i$ only in the ranking of elements of $B$, together imply $f(R')\in B$ (Definition 8.5);
• unanimity-respecting if $f(R)=a$ whenever every agent ranks $a$ at the top (Definition 8.6).

"The range of $f$ is $A$" means that every alternative is chosen at some profile.

For §8.3 the alternatives are labelled $1,\dots,K$. A preference is single-peaked if it has a top alternative $k(i)$ and declines monotonically to the right and to the left of it. $\hat{\mathcal R}$ is the set of single-peaked preferences, and on the restricted domain $\hat{\mathcal R}^N$ DSIC and dictatorship are read with all profiles and deviations taken from $\hat{\mathcal R}$.

Formalization targets

Goal: Proposition 8.5 (Muller–Satterthwaite)

$$|A|\ge 3,\quad f(\mathcal R^N)=A,\quad f\ \text{monotone}\ \Longrightarrow\ \exists\, i\in I\ \ \forall R\in\mathcal R^N\ \forall a\in A:\ f(R)\,R_i\,a.$$

This is the book's own capstone ("the core of the proof", p.144). No constant needs to be fixed, and the statement is strictly stronger than the necessity half of Gibbard–Satterthwaite.

Milestones

• Proposition 8.2: DSIC $\Rightarrow$ monotone.
• Proposition 8.3: monotone $\Rightarrow$ set-monotone.
• Proposition 8.4: monotone and full range $\Rightarrow$ respects unanimity.
• Proposition 8.1 (Gibbard–Satterthwaite): for $|A|\ge3$ and full range, $f$ is DSIC $\iff$ $f$ is dictatorial.
• Proposition 8.6: for $|A|\ge3$ and at least two agents, there is a mechanism on $\hat{\mathcal R}^N$ with range $A$ that is DSIC on $\hat{\mathcal R}^N$ and not dictatorial on $\hat{\mathcal R}^N$.

Significance

The result itself. Proposition 8.5 turns an incentive question into a purely ordinal one: any full-range rule that is Maskin monotone is a dictatorship once three alternatives are available. With Proposition 8.2 it gives Gibbard–Satterthwaite. Proposition 8.6 marks the boundary of the impossibility: with a one-dimensional ordering of alternatives and single-peaked preferences, the median voter rule escapes it.

Formalizing it. All results are classical and proved. The platform already has a proved Gibbard–Satterthwaite theorem (AGT.gibbard_satterthwaite, Algorithmic Game Theory III), derived from Arrow's theorem in the alternative Mathlib environment c5ea0035…. It uses strict-order profiles and a one-agent-deviation monotonicity. This mission adds Maskin monotonicity, the Muller–Satterthwaite theorem, Reny's direct proof route, and the single-peaked possibility result, none of which is on the platform, all in the default environment.

Difficulty

Propositions 8.2–8.4 are short. The difficulty is in Proposition 8.5. Its proof moves one alternative up or down agents' rankings one agent at a time, and it has to keep the chosen alternative pinned at every step using only monotonicity, set-monotonicity and unanimity. It needs a pivotal agent, whose identity depends on the pair of alternatives, and then an argument that the pivots for different alternatives coincide. The argument uses a third alternative $c$ in an essential way. With two alternatives the conclusion is false (majority rule), so any argument that never uses $|A|\ge3$ cannot succeed. Formally, each "move $b$ just below $a$ in agent $j$'s ranking" is an explicit construction of a new linear order, together with a check that the monotonicity hypothesis applies. The figures on pp.146–149 describe these orders only partially ("the other alternatives in arbitrary order"). For Proposition 8.6, the obstacle is that DSIC must be checked against every single-peaked misreport, not only misreports of the peak.

Formalization scope

• A linear order is the structure LinPref A (relation rel, completeness, transitivity, antisymmetry). A profile is ι → LinPref A for a finite agent type ι, and a direct mechanism is (ι → LinPref A) → A. $A$ is a Fintype. "The range of $f$ is $A$" is Function.Surjective f, and $|A|\ge3$ is 3 ≤ Fintype.card A.
• Monotonicity is the book's Definition 8.4 for arbitrary pairs of profiles, with the lower-contour condition required for each agent separately. Dictatorship is ∃ i, ∀ R a, f R ≥_{R_i} a, with the agent chosen before the profile. A weaker monotonicity (one-agent deviations only) or a weaker dictatorship ("some agent's top is chosen at some profile") would trivialize the goal and is ruled out.
• §8.3: the labelling is lab : A ≃ Fin K (labels $0,\dots,K-1$). The restricted domain is a predicate on LinPref A, and DSIC, dictatorship and full range are relativized to profiles in the domain (IsDSICOn, IsDictatorialOn, HasFullRangeOn). Values of the mechanism off the domain are never consulted.
• Two corrections of the page. The left-hand clause of single-peakedness is printed as $(\ell-1)\,R_i\,\ell$ and is used as $\ell\,R_i\,(\ell-1)$ (the book's words "decline monotonically to the left"). Proposition 8.6 carries the added hypothesis $N\ge2$, since with one agent every onto strategy-proof rule is dictatorial.
• Proposition 8.6 is an existence statement. The median voting mechanism is the book's witness, but the statement does not fix it.
• Reusable beyond this mission: the linear-order profile model, Maskin monotonicity and the restricted-domain notions, which apply to Arrow-type results, implementation theory and Moulin's characterization. Proofs of any milestone, or an independent formal proof of Proposition 8.5, are welcome.

Selected references

• T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Ch. 8. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
• A. Gibbard, "Manipulation of voting schemes: a general result", Econometrica 41 (1973) 587–601. https://doi.org/10.2307/1914083
• M. A. Satterthwaite, "Strategy-proofness and Arrow's conditions", Journal of Economic Theory 10 (1975) 187–217. https://doi.org/10.1016/0022-0531(75)90050-2
• E. Muller and M. A. Satterthwaite, "The equivalence of strong positive association and strategy-proofness", Journal of Economic Theory 14 (1977) 412–418. https://doi.org/10.1016/0022-0531(77)90140-5
• 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
• H. Moulin, "On strategy-proofness and single peakedness", Public Choice 35 (1980) 437–455. https://doi.org/10.1007/BF00128122
• S. Barberà, "An introduction to strategy-proof social choice functions", Social Choice and Welfare 18 (2001) 619–653. https://doi.org/10.1007/s003550100151

Motivation

A group of agents must choose one alternative from a set $A$ (whether to build a public project, who receives an object, which of several policies to adopt). Each agent privately knows how much each alternative is worth to them, and money can be transferred. A designer who wants the welfare-maximizing alternative must ask the agents for their valuations, and must set payments so that no agent gains by misreporting, whatever the others report. This requirement, dominant strategy incentive compatibility, does not depend on what agents believe about one another, which is why it is the standard robustness benchmark in public economics, auction design and algorithmic game theory.

The Vickrey–Clarke–Groves (VCG) mechanisms solve this problem for every efficient decision rule. The central question of Chapter 7 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), is whether they are the only solution, and what can be implemented in dominant strategies at all.

Timeline:

• 1961–1973: Vickrey (1961), Clarke (1971) and Groves (1973) introduce the payments that make efficient decisions dominant-strategy incentive-compatible.
• 1977: Green and Laffont (Econometrica 45) show that, when valuations range over a sufficiently rich connected domain, every efficient dominant-strategy mechanism has the Groves form.
• 1979: Holmström (Econometrica 47) extends the uniqueness result to smoothly connected domains. Roberts (1979) characterizes decision rules with positive association of differences on unrestricted domains as weighted welfare maximizers.
• 1987: Rochet (J. Math. Econ. 16) characterizes implementable decision rules by cyclical monotonicity, with no structure on alternatives or types.
• 2001: Krishna and Maenner (Econometrica 69) prove payoff equivalence for convex type sets and utilities convex in the type.
• 2009: Lavi, Mu'alem and Nisan (Soc. Choice Welf. 32) give two short proofs of Roberts' theorem.

Setting

There is a finite set $I$ of agents and a set $A$ of alternatives. Agent $i$ has a type $\theta_i$ from an abstract set $\Theta_i$. If alternative $a$ is chosen and agent $i$ pays $t_i$, agent $i$'s utility is $u_i(a,\theta_i) - t_i$. A type vector is $\theta \in \Theta = \prod_i \Theta_i$; $\theta_{-i} \in \Theta_{-i} = \prod_{j \ne i}\Theta_j$ omits agent $i$, and $(\theta_i', \theta_{-i})$ replaces agent $i$'s type by $\theta_i'$.

A direct mechanism $(q, t_1, \dots, t_N)$ consists of a decision rule $q : \Theta \to A$ and transfer rules $t_i : \Theta \to \mathbb R$. It is dominant strategy incentive-compatible (DSIC) if for all $\theta$, $i$ and $\theta_i'$,

$$u_i(q(\theta),\theta_i) - t_i(\theta) \ \ge\ u_i(q(\theta_i',\theta_{-i}),\theta_i) - t_i(\theta_i',\theta_{-i}).$$

A decision rule is efficient if $q(\theta)$ maximizes $\sum_i u_i(a,\theta_i)$ over $a \in A$ at every $\theta$. A mechanism is VCG if $q$ is efficient and every agent's transfer has the form

$$t_i(\theta) = -\sum_{j \ne i} u_j(q(\theta),\theta_j) + \tau_i(\theta_{-i})$$

for some function $\tau_i$ of the other agents' types. The chapter also uses positive association of differences (PAD: if $q(\theta) = a$ and every agent's utility advantage of $a$ over every other alternative strictly increases from $\theta$ to $\theta'$, then $q(\theta') = a$), flexibility (the range $q(\Theta)$ has at least three elements), ex post individual rationality and ex post budget balance ($\sum_i t_i(\theta) = 0$).

Formalization targets

Goal: uniqueness of VCG (Corollary 7.1, Green–Laffont–Holmström)

If every $\Theta_i$ is a convex subset of a Euclidean space $\mathbb R^{d_i}$ and every $u_i(a,\cdot)$ is convex and continuous on $\Theta_i$, then every DSIC mechanism $(q,t)$ with an efficient $q$ is a VCG mechanism: for each $i$ there is $\tau_i : \Theta_{-i} \to \mathbb R$ with

$$t_i(\theta) = -\sum_{j \ne i} u_j(q(\theta),\theta_j) + \tau_i(\theta_{-i}) \qquad \text{for all } \theta.$$

The goal leaves $A$, the number of agents and the dimensions $d_i$ free; it asserts only the form of the transfers.

Milestones

Every numbered result of Chapter 7 except Proposition 7.6 (see Formalization scope):

1. Proposition 7.1: implementability iff cyclical monotonicity in each agent's type (Rochet).
2. Proposition 7.2: on bounded, one-dimensional type sets, implementability iff monotonicity.
3. Proposition 7.3: under the goal's convexity hypotheses, the transfers implementing a given $q$ are unique up to $\tau_i(\theta_{-i})$.
4. Proposition 7.4: VCG mechanisms are DSIC.
5. Proposition 7.5: weak monotonicity in every $\theta_i$ implies PAD.
6. Proposition 7.7 (Roberts): on unrestricted domains with finite $A$, a flexible $q$ with range $q(\Theta) = A$ satisfies PAD iff there are $k_i \ge 0$, not all zero, and $F : A \to \mathbb R$ with $\sum_i k_i u_i(q(\theta),\theta_i) + F(q(\theta)) \ge \sum_i k_i u_i(a,\theta_i) + F(a)$ for all $a \in A$.
7. Proposition 7.8: affine maximizers with all $k_i > 0$ are implementable.
8. Proposition 7.9: ex post individual rationality holds iff it holds at the lowest type $\underline\theta_i$ with outside option $\underline a_i$.
9. Proposition 7.10: with $N \ge 2$, a budget-balanced VCG mechanism for efficient $q$ exists iff $\sum_i u_i(q(\theta),\theta_i) = \sum_i f_i(\theta_{-i})$ for some $f_i : \Theta_{-i} \to \mathbb R$.

Significance

Corollary 7.1 turns the VCG construction from one solution into the complete answer. Any question about efficient dominant-strategy mechanisms (revenue, budget balance, individual rationality) reduces to a question about the functions $\tau_i$. With Proposition 7.10 it gives a necessary and sufficient condition for efficient, budget-balanced dominant-strategy implementation. That condition fails in bilateral trade, and the failure does not use individual rationality. Roberts' theorem plays the same role for inefficient rules: on unrestricted domains, weighted welfare maximization is essentially all that can be implemented.

All of these results are proved in the literature, and none is formalized. The platform has VCG incentive compatibility and weak monotonicity for valuation-based types (the Algorithmic Game Theory IV mission). It has no uniqueness theorem, no revenue equivalence for multidimensional convex types, no Rochet theorem and no Roberts theorem. The book proves Corollary 7.1 from Proposition 7.3, but proves 7.3 itself only by reference to Krishna and Maenner. It states Roberts' theorem without proof.

Difficulty

The uniqueness claim does not follow from incentive compatibility alone. With finitely many types it is false, because any transfers inside the gaps left by the incentive constraints work (Börgers §5.8). The work lies in showing that, along every segment in the convex type set, an agent's equilibrium utility is pinned down by the decision rule. The equilibrium utility is a pointwise supremum of convex functions, one for each report, and the chosen alternative can change at uncountably many points of the segment. A differentiable envelope argument is therefore not directly available. At the boundary of the type set, convexity alone does not prevent upward jumps, which is why continuity is part of the hypotheses. Roberts' theorem needs a separate, combinatorial analysis of the sets of utility differences at which each alternative is chosen, and flexibility is essential there.

Formalization scope

Agents form a finite type ι with decidable equality. Types are arbitrary types Θ i, and utilities are u : ∀ i, A → Θ i → ℝ. The profile $(\theta_i',\theta_{-i})$ is Function.update θ i θ'. $\Theta_{-i}$ is the product Others Θ i over j ≠ i, so each $\tau_i$ and $f_i$ is a function of the others' types only; a constant or a function of the full profile would change the theorem. In the goal and Proposition 7.3, $\Theta_i$ is a convex set S i in EuclideanSpace ℝ (Fin (d i)).

Deviations from the page, each forced by a counterexample recorded in the item's natural-language statement:

• Corollary 7.1 and Proposition 7.3 add continuity of $u_i(a,\cdot)$ on $\Theta_i$. With convexity alone, a utility with a jump at the endpoint of $[0,1]$ admits a non-VCG DSIC mechanism.
• Proposition 7.7 is stated with $k_i \ge 0$, not all zero, instead of $k_i > 0$, and with the added hypothesis that $q$ is onto $A$ (the conclusion still ranges over all $a \in A$, as on the page). Dictatorships and affine maximizers over a proper subset of $A$ are counterexamples to the printed version.
• Proposition 7.6 (flexible PAD rules on unrestricted domains are implementable) is false as printed. It is not a milestone; the reason is in the mission's hard list.
• Proposition 7.10 adds $N \ge 2$, since its proof divides by $N-1$.

The trivializing formalization to avoid is proving Proposition 7.4 (VCG $\Rightarrow$ DSIC) in place of the goal (DSIC $+$ efficient $\Rightarrow$ VCG). A development that proves the goal needs reusable infrastructure: convex functions restricted to segments, absolute continuity of continuous convex functions on compact intervals, and an envelope theorem for suprema of convex functions. Proofs of Rochet's and Roberts' theorems in this abstract setting are also welcome.

Selected references

• T. Börgers (with D. Krähmer and R. Strausz), An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Chapter 7. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
• W. Vickrey, Counterspeculation, Auctions, and Competitive Sealed Tenders, Journal of Finance 16, 1961. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
• E. H. Clarke, Multipart Pricing of Public Goods, Public Choice 11, 1971. https://doi.org/10.1007/BF01726210
• T. Groves, Incentives in Teams, Econometrica 41, 1973. https://doi.org/10.2307/1914085
• J. Green and J.-J. Laffont, Characterization of Satisfactory Mechanisms for the Revelation of Preferences for Public Goods, Econometrica 45, 1977. https://doi.org/10.2307/1911219
• B. Holmström, Groves' Scheme on Restricted Domains, Econometrica 47, 1979. https://www.jstor.org/stable/1911954
• K. Roberts, The Characterization of Implementable Choice Rules, in J.-J. Laffont (ed.), Aggregation and Revelation of Preferences, North-Holland, 1979, pp. 321–348.
• J.-C. Rochet, A Necessary and Sufficient Condition for Rationalizability in a Quasi-Linear Context, Journal of Mathematical Economics 16, 1987. https://doi.org/10.1016/0304-4068(87)90007-3
• V. Krishna and E. Maenner, Convex Potentials with an Application to Mechanism Design, Econometrica 69, 2001. https://doi.org/10.1111/1468-0262.00233
• R. Lavi, A. Mu'alem and N. Nisan, Two Simplified Proofs for Roberts' Theorem, Social Choice and Welfare 32, 2009. https://doi.org/10.1007/s00355-008-0333-3
• P. Milgrom, Putting Auction Theory to Work, Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511813825

Motivation

Almost every screening, auction and regulation model asks the same preliminary question: which allocation rules can be made incentive-compatible by some choice of payments? In the one-dimensional models of auction theory and nonlinear pricing the answer is monotonicity: higher types must receive higher allocations. Many applications are not one-dimensional, though. Examples are multi-object auctions, multi-product pricing, and lotteries over several outcomes. For those, a characterization that uses no structure at all is needed. Rochet (1987) gave one: an allocation rule is implementable exactly when it is cyclically monotone, a condition that originates in Rockafellar's characterization of subdifferentials of convex functions. Later work on dominant-strategy implementation, the "weak monotonicity" literature of algorithmic mechanism design, and revenue equivalence all build on it.

This mission formalizes Chapter 5 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015): all nine numbered results of the chapter.

Timeline. Rockafellar (1970, Theorem 24.8) characterized the cyclically monotone maps between vector spaces as the subgradient selections of convex functions. Rochet (1987) extended the idea to arbitrary alternatives and types with quasi-linear utility and proved that implementability is exactly cyclical monotonicity. Krishna and Maenner (2001) proved revenue equivalence on convex type spaces with utilities convex in the type. Bikhchandani, Chatterji, Lavi, Mu'alem, Nisan and Sen (2006) showed that for finitely many alternatives, weak monotonicity (the two-type case of cyclical monotonicity) already suffices on rich, order-based domains. Saks and Yu (2005) proved the same on convex domains.

Setting

A designer and one agent choose an alternative $a$ from a set $A$. The agent has a type $\theta$ in a nonempty set $\Theta$. With utility function $u : A \times \Theta \to \mathbb R$, her payoff from $a$ when she pays $t$ is $u(a,\theta) - t$. Neither $A$ nor $\Theta$ carries any structure.

A direct mechanism is a decision rule $q : \Theta \to A$ and a transfer rule $t : \Theta \to \mathbb R$. It is incentive-compatible if $u(q(\theta),\theta) - t(\theta) \ge u(q(\theta'),\theta) - t(\theta')$ for all $\theta,\theta'$. A decision rule is implementable if some $t$ makes it incentive-compatible. It is weakly monotone if $u(q(\theta_1),\theta_1) - u(q(\theta_2),\theta_1) \ge u(q(\theta_1),\theta_2) - u(q(\theta_2),\theta_2)$ for all pairs of types. It is cyclically monotone if for every finite sequence of types $\theta^1,\dots,\theta^k$ with $\theta^k = \theta^1$,

$$\sum_{\kappa=1}^{k-1}\bigl(u(q(\theta^\kappa),\theta^{\kappa+1}) - u(q(\theta^\kappa),\theta^\kappa)\bigr) \le 0 .$$

A complete and transitive order $R$ of $A$ induces a partial order on types: $\theta \succ_R \theta'$ if $\theta$ values every $R$-higher alternative strictly more, relative to an $R$-lower one, than $\theta'$ does, and neither type distinguishes $R$-indifferent alternatives. The type set is one-dimensional if any two distinct types are $\succ_R$-comparable, and bounded if all utility differences lie in $(-c,c)$ for some $c > 0$. It is rich if, for some reflexive and transitive relation $R$, every function $v : A \to \mathbb R$ with $aRb \Rightarrow v(a) \ge v(b)$ is some type's utility function. A mechanism is individually rational with outside option $a$ if every type does at least as well as with $a$ and no payment.

Formalization targets

Goal: Proposition 5.2 (Rochet)

$$q \text{ implementable} \iff q \text{ cyclically monotone},$$

for arbitrary $A$, nonempty $\Theta$ and $u$.

Milestones

1. Proposition 5.1: implementable $\Rightarrow$ weakly monotone.
2. Proposition 5.3: for lotteries over finitely many outcomes, $\Theta \subseteq \mathbb R^\Omega$ convex and $u(p,\theta) = p\cdot\theta$, $q$ is implementable iff there is a convex $U$ on $\Theta$ with $U(\theta') \ge U(\theta) + q(\theta)\cdot(\theta'-\theta)$ for all $\theta,\theta'$.
3. Proposition 5.4: weakly monotone $\Rightarrow$ ($\theta \succ_R \theta' \Rightarrow q(\theta)\,R\,q(\theta')$), for every complete transitive $R$.
4. Proposition 5.5: on one-dimensional type sets, weak monotonicity $\iff$ monotonicity with respect to $R$.
5. Proposition 5.6: $A$ finite, $\Theta$ bounded and one-dimensional: monotone with respect to $R$ $\Rightarrow$ implementable.
6. Proposition 5.7 (Bikhchandani et al.): $A$ finite, rich and consistent domain: weakly monotone $\Rightarrow$ implementable.
7. Proposition 5.8 (revenue equivalence): on convex $\Theta \subseteq \mathbb R^n$ with $u(a,\cdot)$ convex and continuous, if $(q,t)$ is incentive-compatible then $(q,t')$ is iff $t' = t + \tau$ for a constant $\tau$.
8. Proposition 5.9: on one-dimensional type sets with a lowest type $\underline\theta$ and a worst alternative $\underline a$, an incentive-compatible mechanism is individually rational with outside option $\underline a$ iff $u(q(\underline\theta),\underline\theta) - t(\underline\theta) \ge u(\underline a,\underline\theta)$.

Significance

Rochet's theorem turns the existence of payments, an infinite system of linear inequalities in unknowns $t(\theta)$, into a condition on the decision rule alone. It underlies the characterization of implementable rules in multidimensional screening, the taxation principle, and the dominant-strategy characterizations of Chapter 7 (applied agent by agent). Propositions 5.4–5.6 recover the "monotone allocation" results of the one-dimensional chapters from it. Proposition 5.8 is the general form of the payoff-equivalence lemmas used for optimal auctions.

All results are classical and proved on paper, except Propositions 5.7 and 5.8, whose proofs the book omits and refers to the literature. None of them is formalized on Prove2Me. The platform's algorithmic-game-theory series has the weak-monotonicity half in a multi-agent valuation model (types are valuations $A \to \mathbb R$), not the abstract-type statement, and has no cyclical-monotonicity or Rochet result.

Difficulty

Necessity is a two-line telescoping argument. Sufficiency needs a transfer rule built from the decision rule, and the first idea fails: prices attached to alternatives chosen pair by pair (which weak monotonicity supplies) need not be globally consistent. Figure 5.1 of the book gives a three-type example that is weakly monotone but not implementable. The transfer must come from a supremum over all finite chains of types starting at a fixed type. The supremum is finite only because of cyclical monotonicity, and no finiteness, compactness or boundedness is available. Proposition 5.8 needs an envelope argument along segments in $\Theta$ without differentiability. Proposition 5.7 needs a combinatorial argument that uses richness of the domain.

Formalization scope

Alternatives and types are arbitrary Lean types A, Θ with Nonempty Θ, and the utility is u : A → Θ → ℝ. A cycle of length $k = m+1$ is a map Fin (m+1) → Θ with equal first and last entries, and its $m$ summands are indexed by Fin m. Relations are predicates A → A → Prop. For Propositions 5.3 and 5.8, types form a subset S of Ω → ℝ (resp. Fin n → ℝ) used as a subtype. Lotteries are stdSimplex ℝ Ω, and the subgradient inequality is required only at points of S.

The explicit statements are fixed as follows:

• Proposition 5.8's conclusion is the exact translation form $t'(\theta) = t(\theta) + \tau$ for one $\tau$ and all $\theta$.
• Proposition 5.9's condition is the single inequality at $\underline\theta$.
• Boundedness in Proposition 5.6 is Definition 5.9's strict two-sided bound with some $c > 0$.

Two statements are corrected from the page, each with a counterexample to the literal version recorded in its item:

• Proposition 5.7 adds Bikhchandani et al.'s requirement that every type's utility respects $R$.
• Proposition 5.8 adds continuity of $u(a,\cdot)$ on $\Theta$ (automatic in the relative interior).

Both directions of Rochet's theorem are required. The necessity half alone, or a version with finite $\Theta$, finite $A$ or bounded utilities, is a different and much weaker theorem and does not close the goal.

The development needs finite telescoping sums, suprema of sets of reals (sSup with an explicit bounded-above argument), convex functions on sets and one-dimensional convex analysis (Proposition 5.8). The definitions file is reusable for Chapters 6–8 of the series. Contributions of alternative proofs, for example Proposition 5.6 through Rochet's theorem, are welcome.

Selected references

• T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Chapter 5. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
• J.-C. Rochet, "A necessary and sufficient condition for rationalizability in a quasi-linear context," Journal of Mathematical Economics 16 (1987) 191–200. https://doi.org/10.1016/0304-4068(87)90007-3
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, Theorem 24.8.
• V. Krishna and E. Maenner, "Convex potentials with an application to mechanism design," Econometrica 69 (2001) 1113–1119. https://doi.org/10.1111/1468-0262.00233
• S. Bikhchandani, S. Chatterji, R. Lavi, A. Mu'alem, N. Nisan and A. Sen, "Weak monotonicity characterizes deterministic dominant-strategy implementation," Econometrica 74 (2006) 1109–1132. https://doi.org/10.1111/j.1468-0262.2006.00695.x
• M. Saks and L. Yu, "Weak monotonicity suffices for truthfulness on convex domains," Proceedings of the 6th ACM Conference on Electronic Commerce (2005) 286–293. https://doi.org/10.1145/1064009.1064039

Motivation

Bayesian mechanism design assumes that the designer knows a common prior from which every agent's beliefs about the others are derived. Chapter 4 of Börgers' An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015, DOI 10.1093/acprof:oso/9780199734023.001.0001) drops that assumption. The designer is unwilling to rely on anything about what agents believe about each other, and therefore requires that truth telling be optimal for every type whatever the other agents report (dominant strategy incentive compatibility) and that participation be worthwhile after all reports are known (ex post individual rationality). The chapter revisits the three examples of Chapter 3 (single unit auctions, public goods, bilateral trade) and asks which mechanisms survive these requirements.

The answer differs sharply between examples. In auctions nothing is lost: an expected-revenue-maximizing auction can be implemented in dominant strategies. With a budget constraint, the class collapses. For a public good shared by two agents, the only dominant-strategy, ex post individually rational mechanisms that exactly balance the budget are fixed cost shares; in bilateral trade they are fixed-price mechanisms. These results go back to the dominant-strategy literature on public goods (Serizawa 1999, Econometrica) and on bilateral trade (Hagerty and Rogerson 1987, Journal of Economic Theory), as the book's §4.5 records (p.93), and they explain why simple posted-price and cost-sharing rules are common in practice.

Setting

Every agent $i$ has a type $\theta_i$ in an interval. In the auction and the public good examples the interval is $[\underline\theta,\bar\theta]$ with $0 \le \underline\theta < \bar\theta$; $\Theta = [\underline\theta,\bar\theta]^I$ is the set of type vectors, and $\theta_{-i}$ is $\theta$ without its $i$-th entry. A direct mechanism asks every agent to report a type and maps the reports to an outcome.

• Auction (§4.2). A seller has one good. The mechanism consists of allocation probabilities $q_i(\theta) \ge 0$ with $\sum_i q_i(\theta) \le 1$ and payments $t_i(\theta)$; buyer $i$'s utility is $\theta_i q_i(\theta) - t_i(\theta)$.
• Public good (§4.3). A good costing $c > 0$ is produced ($q(\theta) = 1$) or not ($q(\theta) = 0$); agent $i$ pays $t_i(\theta)$ and has utility $\theta_i q(\theta) - t_i(\theta)$. Ex post budget balance is the equality $\sum_i t_i(\theta) = c\,q(\theta)$ for every $\theta$.
• Bilateral trade (§4.4). A seller with type $\theta_S \in [\underline\theta_S,\bar\theta_S]$ and a buyer with type $\theta_B \in [\underline\theta_B,\bar\theta_B]$; trade takes place ($q(\theta) = 1$) or not; the seller receives $t_S(\theta)$ and has utility $\theta_S(1-q(\theta)) + t_S(\theta)$; the buyer pays $t_B(\theta)$ and has utility $\theta_B q(\theta) - t_B(\theta)$. Ex post exact budget balance is $t_B = t_S$.

A mechanism is dominant strategy incentive-compatible if for every agent, every true type, every false report and every report profile of the others, truthful reporting yields at least as much utility. It is ex post individually rational if every type's utility at every type vector is at least its outside option: $0$ for buyers and public good agents, $\theta_S$ (keeping the good) for the seller. A canonical mechanism (Definitions 4.3–4.5) allocates according to strictly increasing continuous scores $\psi_i(\theta_i)$ and charges each agent the smallest report with which the outcome would have been the same.

Formalization targets

Goal: Proposition 4.8, fixed cost shares

For $N = 2$ and a decision rule whose production set $\{\theta \in \Theta \mid q(\theta) = 1\}$ is closed, a direct public good mechanism is dominant strategy incentive-compatible, ex post individually rational and ex post budget balanced if and only if there are $\tau_1, \tau_2 \in \mathbb R$ with $\tau_1 + \tau_2 = c$ and, for all $\theta \in \Theta$,

$$q(\theta) = 1,\ t_i(\theta) = \tau_i \ \text{ if } \theta_1 \ge \tau_1 \text{ and } \theta_2 \ge \tau_2; \qquad q(\theta) = 0,\ t_i(\theta) = 0 \ \text{ otherwise.}$$

Both directions are part of the goal; the "only if" direction is the content.

Milestones

• The revelation principle for dominant strategies (Proposition 4.1).
• Characterizations of dominant strategy incentive compatibility: monotone allocation with the envelope payment formula in auctions (Proposition 4.2), threshold rules with payment jump $\hat\tau_i - \tau_i = \hat\theta_i$ for public goods (Proposition 4.5) and bilateral trade (Proposition 4.9).
• Ex post individual rationality reduces to the lowest type, or to the highest seller type (Propositions 4.3, 4.6, 4.10).
• Canonical mechanisms are dominant strategy incentive-compatible and ex post individually rational, with zero rent for the lowest type (Propositions 4.4, 4.7, 4.11).
• The bilateral trade analogue of the goal (Proposition 4.12): the only such mechanisms with $t_B = t_S$ and closed trade set are no trade, or trade at a fixed price $\hat\theta$ exactly when $\theta_S \le \hat\theta \le \theta_B$.

Significance

Proposition 4.4 shows that the optimal auctions of Chapter 3 remain available without any assumption on beliefs, while Propositions 4.8 and 4.12 show that under exact budget balance, dominant strategy implementation forces rules that ignore reported valuations except through a yes/no participation decision. Together they mark the boundary between settings where the Bayesian and the belief-free approaches coincide and settings where the belief-free requirement is severe. This contrast motivates the robust mechanism design of Chapter 10.

These results are proved in the book: Propositions 4.5 and 4.8 in full, the others with proofs omitted or "analogous". No machine-checked proof of them appears on the platform or in Mathlib. The platform has a single-parameter characterization in a different model (AGT.single_parameter_characterization: valuation profiles, win sets, normalized losers' payments) and the second-price dominance fact; neither covers public goods, bilateral trade, budget balance or randomized allocations. The mission would add a machine-checked belief-free counterpart of Chapter 3, including the two characterization theorems whose printed proofs leave cases to the reader.

Difficulty

The characterizations (Propositions 4.2, 4.5, 4.9) are standard single-agent arguments applied to every profile of the others. The goal is harder. Proposition 4.5 describes each agent's incentives separately, for each report of the other agent, with thresholds and payments that may vary with that report. Budget balance couples the two agents' payments at every type vector. The step that fails when attempted naively is going from "a threshold for each $\theta_{-i}$" to "one fixed threshold for each agent": the thresholds may lie outside the type interval, several degenerate configurations occur (an agent whose report never matters, a good that is always or never produced), and the printed proof treats the degenerate cases by assuming $\underline\theta = 0$ and leaves one of them "analogous". The closedness hypothesis is what makes the relevant minimal types exist; without it the boundary of the production set is not determined. Proposition 4.12 has the same structure with the seller's orientation reversed.

Formalization scope

• Agents are a finite type with decidable equality (auctions, public goods), Fin 2 for the goal, and a pair (θS, θB) : ℝ × ℝ for bilateral trade. A deviation $(\theta_i', \theta_{-i})$ is Function.update θ i x for θ ∈ Θ; quantifying over θ ∈ Θ quantifies over $\theta_{-i}$.
• Decision and trading rules are real-valued and take values in $\{0,1\}$ on $\Theta$; auction allocations lie in $\Delta$ on $\Theta$. Values outside $\Theta$ play no role.
• Budget balance in §§4.3–4.4 is the equality $\sum_i t_i = c\,q$ (resp. $t_B = t_S$). The inequality of Definition 3.5 would make the goal false.
• Explicit formulas stated as in the book: the payment identity of Proposition 4.2, the relation $\hat\tau_i - \tau_i = \hat\theta_i$ (Propositions 4.5, 4.9), the canonical payments of Definitions 4.3–4.5 (with the $1/n$ tie-splitting of Definition 4.3), the cost shares with $\tau_1 + \tau_2 = c$ (Proposition 4.8) and the fixed price $\hat\theta$ with trade iff $\theta_S \le \hat\theta \le \theta_B$ (Proposition 4.12). Minima and maxima in the canonical payments are written as sInf/sSup of sets that are nonempty and closed whenever they are used.
• Thresholds $\hat\theta_i$ range over $\mathbb R$ and depend on $\theta_{-i}$; cost shares $\tau_i$ may be negative; the goal does not assume $\underline\theta = 0$.
• The general mechanism of Proposition 4.1 has arbitrary message sets and an outcome function to allocation probabilities and expected payments. Stating the revelation principle for a mechanism that is already direct would trivialize it and is ruled out.
• The goal must not be weakened to one direction, to the existence of some fixed-share mechanism, or to budget balance as an inequality.

Contributions welcome: proofs of the characterization milestones (4.2, 4.5, 4.9), which the goal and Proposition 4.12 use; a proof of the goal covering the degenerate cases the book leaves to the reader; and the three-agent counterexample of p.90 as a separate statement.

Selected references

• T. Börgers (with D. Krähmer and R. Strausz), An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Chapter 4. DOI 10.1093/acprof:oso/9780199734023.001.0001
• K. M. Hagerty and W. P. Rogerson, Robust trading mechanisms, Journal of Economic Theory 42 (1987) 94–107.
• S. Serizawa, Strategy-proof and symmetric social choice functions for public good economies, Econometrica 67 (1999) 121–145.
• D. Mookherjee and S. Reichelstein, Dominant strategy implementation of Bayesian incentive compatible allocation rules, Journal of Economic Theory 56 (1992) 378–399.

Motivation

Stock exchanges, commodity markets and trading platforms are institutions for trade between parties who each know something the other does not. The simplest version is bilateral trade: one seller, one buyer, one indivisible good, and each side privately knows its own value. The question is whether any trading institution can make the two trade exactly when trade is efficient, with both taking part voluntarily and without a subsidy from outside. Myerson and Satterthwaite (1983) showed that, apart from trivial cases, none can. The result is one of the basic impossibility theorems of economic theory. It explains why bargaining under private information is inefficient, and it is the benchmark every later analysis of double auctions and market design compares against.

This mission formalizes Section 3.4 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015): the impossibility theorem, the pivot-mechanism argument that proves it, the second-best and profit-maximizing trading mechanisms, and the uniform example.

Timeline. Vickrey (1961) noted the tension between efficiency and budget balance in markets with private values. Chatterjee and Samuelson (1983) studied the sealed-offer double auction and its linear equilibrium for uniform values. Myerson and Satterthwaite (1983) proved the impossibility for general independent distributions with overlapping supports, and computed the second-best mechanism; for uniform values it coincides with the Chatterjee–Samuelson linear equilibrium. Börgers (2015) gives the pivot-mechanism proof formalized here.

Setting

A seller $S$ owns one indivisible good; a buyer $B$ may buy it. The seller's value $\theta_S$ has distribution $F_S$ with density $f_S > 0$ on $[\underline\theta_S, \overline\theta_S]$; the buyer's value $\theta_B$ has distribution $F_B$ with density $f_B > 0$ on $[\underline\theta_B, \overline\theta_B]$. The two intervals are nondegenerate and may differ, and the values are independent. The seller's utility is $t$ if she sells for $t$ and $\theta_S + t$ if she keeps the good and receives $t$; the buyer's is $\theta_B - t$ if he buys and pays $t$, and $-t$ otherwise.

A direct mechanism is a trading rule $q : \Theta \to \{0,1\}$ on $\Theta = [\underline\theta_S, \overline\theta_S] \times [\underline\theta_B, \overline\theta_B]$ and transfers $t_S$ (received by the seller) and $t_B$ (paid by the buyer). Conditioning on one agent's type gives the interim trade probabilities $Q_S, Q_B$, the interim transfers $T_S, T_B$, and the interim utilities $U_S(\theta_S) = T_S(\theta_S) + (1 - Q_S(\theta_S))\theta_S$ and $U_B(\theta_B) = Q_B(\theta_B)\theta_B - T_B(\theta_B)$. The mechanism is incentive-compatible if truthful reporting is a Bayesian equilibrium, individually rational if $U_S(\theta_S) \ge \theta_S$ and $U_B(\theta_B) \ge 0$ for all types, ex post budget balanced if $t_S(\theta) = t_B(\theta)$ for every $\theta$, and ex ante budget balanced if $\mathbb E[t_S] = \mathbb E[t_B]$. A first-best trading rule trades when $\theta_B > \theta_S$ and not when $\theta_B < \theta_S$, with any choice at ties. The seller's virtual cost is $\psi_S = \theta_S + F_S/f_S$ and the buyer's virtual valuation is $\psi_B = \theta_B - (1 - F_B)/f_B$; the distributions are regular if both are increasing.

Formalization targets

Goal: Proposition 3.12 (Myerson–Satterthwaite)

An incentive-compatible, individually rational and ex post budget balanced direct mechanism with a first-best trading rule exists if and only if

$$\underline\theta_B \ge \overline\theta_S \quad\text{or}\quad \underline\theta_S \ge \overline\theta_B .$$

Milestones

• Lemmas 3.9–3.11. The pivot mechanism is incentive-compatible and individually rational. Among all such mechanisms that implement a first-best rule, it maximizes $\mathbb E[t_B - t_S]$. That quantity is negative whenever $\underline\theta_B < \overline\theta_S$ and $\overline\theta_B > \underline\theta_S$.
• Proposition 3.13 (second best). With overlapping supports and regular distributions, the welfare-maximizing incentive-compatible, individually rational, ex ante budget balanced mechanisms are characterized by the trading rule

$$q(\theta) = 1 \iff \theta_B - \tfrac{\lambda}{1+\lambda}\tfrac{1 - F_B(\theta_B)}{f_B(\theta_B)} \ge \theta_S + \tfrac{\lambda}{1+\lambda}\tfrac{F_S(\theta_S)}{f_S(\theta_S)}$$

for some $\lambda > 0$, exact budget balance $\int q\,(\psi_B - \psi_S)\,f = \overline\theta_S - \int \psi_S f$, and the incentive-compatible payments with binding participation of $\overline\theta_S$ and $\underline\theta_B$.

• Proposition 3.14 (profit maximization). Profit $\mathbb E[t_B - t_S]$ is maximized by trading iff $\psi_B(\theta_B) > \psi_S(\theta_S)$, with the same payment formulas.
• Propositions 3.15–3.16 (uniform values on $[0,1]$). The second best trades iff $\theta_B - \theta_S > 1/4$; the profit maximizer trades iff $\theta_B - \theta_S > 1/2$.

Significance

The theorem locates the source of inefficiency in bilateral bargaining in private information itself, not in any particular bargaining protocol: no mechanism, however clever, achieves efficient voluntary trade without a subsidy. It is the reason efficiency in markets is studied as a limit (large double auctions approach efficiency as the number of traders grows), and why a trading platform's fee structure is analyzed as a second-best problem. The pivot-mechanism argument is the same one that proves the impossibility of first-best public-goods provision (Proposition 3.7), so the two formalizations share their structure.

All results of this section are classical and proved on paper. None is formalized on Prove2Me, and Mathlib has no mechanism-design library. The platform has the Chatterjee–Samuelson linear equilibrium as an open statement about one particular game; this mission states results about all mechanisms. A complete development yields a reusable one-dimensional envelope/payoff-equivalence library for two agents with differently oriented types (the seller's incentive constraint runs from high types down), and the Lagrangian optimality argument for a linear objective under a single linear constraint.

Difficulty

The obvious attempt to prove impossibility looks for a contradiction between incentive compatibility and budget balance state by state. That fails: incentive compatibility and participation are interim constraints, so any single state admits budget-balanced transfers consistent with them, and the contradiction exists only after integrating over the prior. Two points need care. The seller's orientation is reversed: her trade probability is decreasing and her participation constraint binds at the highest type. And the deficit of the pivot mechanism must be shown to have positive probability, which uses that the supports overlap in a set with nonempty interior. The optimal-mechanism results additionally need that the trading rule implied by a Lagrange multiplier satisfies the monotonicity constraint, which is where regularity enters, and that a multiplier exists which makes the budget constraint bind.

Formalization scope

A type vector is a pair θ : ℝ × ℝ with θ.1 the seller's and θ.2 the buyer's value. The prior is Lebesgue measure on $\Theta$ with density $f_S(\theta_S) f_B(\theta_B)$. Densities are measurable, strictly positive on the closed supports and integrate to one; nothing else, such as continuity, is assumed. The trading rule is real-valued with values in $\{0,1\}$ on $\Theta$ (deterministic, as in Definition 3.9). The measurability the book omits (Ch. 2 note 2) is built into the admissible class: $q$, $t_S$, $t_B$ are measurable with integrable transfers. "Increasing" is weak monotonicity, the book's convention.

Explicit formulas the statements carry: the first-best rule (3.61) with free tie rule, the pivot transfers of Definition 3.10, the rule (3.70) with parameter $\lambda > 0$, the exact budget equation of Proposition 3.13 (ii), the payment formulas $T_B(\theta_B) = \theta_B Q_B(\theta_B) - \int_{\underline\theta_B}^{\theta_B} Q_B$ and $T_S(\theta_S) = \overline\theta_S - (1 - Q_S(\theta_S))\theta_S - \int_{\theta_S}^{\overline\theta_S}(1 - Q_S)$, the profit rule $\psi_B > \psi_S$, and the thresholds $1/4$ and $1/2$.

The goal quantifies over every first-best trading rule and imposes budget balance as the ex post equality $t_S = t_B$. Dropping budget balance, weakening it to $t_S \le t_B$, or fixing one tie rule would give a different, and in the first case false, statement. The pointwise "if and only if … for all $\theta$" characterizations of Propositions 3.13–3.16 are stated with necessity almost everywhere, since an optimal trading rule is determined only up to null sets. For Proposition 3.14 necessity is also restricted to $\{\psi_B \ne \psi_S\}$: under weak regularity that tie set can have positive probability, and profit does not depend on the trading rule there.

Contributions welcome: proofs of the milestones, a two-agent payoff-equivalence lemma for the seller's reversed orientation, and a sorry-free construction of the pivot mechanism's integrability facts.

Selected references

• R. B. Myerson and M. A. Satterthwaite, Efficient mechanisms for bilateral trading, Journal of Economic Theory 29 (1983) 265–281. https://doi.org/10.1016/0022-0531(83)90048-0
• K. Chatterjee and W. Samuelson, Bargaining under incomplete information, Operations Research 31 (1983) 835–851. https://doi.org/10.1287/opre.31.5.835
• W. Vickrey, Counterspeculation, auctions, and competitive sealed tenders, Journal of Finance 16 (1961) 8–37. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
• T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, §3.4. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001

Motivation

Whether a community can finance a shared project out of voluntary contributions, when each member knows only her own benefit from it, is one of the founding questions of mechanism design. Bayesian mechanism design began with mechanisms for the provision of public goods: d'Aspremont and Gérard-Varet (1979) and Arrow (1979) showed that the efficient decision can be made Bayesian incentive compatible with a budget that balances in every state, provided agents cannot opt out. Once participation is voluntary, this is no longer possible, and Güth and Hellwig (1986) studied the best mechanism under that constraint. The same tension between efficiency, incentives, voluntary participation and budget balance drives the Myerson–Satterthwaite theorem for bilateral trade, which the next mission of this series formalizes.

This mission formalizes Section 3.3 of Tilman Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), which treats the public goods problem in the independent private values model with a continuum of types. The section proves an impossibility theorem for first best provision and then characterizes the best mechanisms that respect the budget: the welfare-maximizing (second best) mechanism and the profit-maximizing one, with a worked two-agent uniform example.

Setting

A community of agents $I = \{1, \dots, N\}$, $N \ge 2$, decides whether to produce an indivisible, nonexcludable public good, $g \in \{0,1\}$, at cost $c > 0$. Agent $i$ pays a transfer $t_i$ and obtains utility $\theta_i g - t_i$. Her type $\theta_i$ is private information, drawn independently across agents from a distribution $F_i$ with density $f_i$, strictly positive on the common support $[\underline\theta, \bar\theta]$, $0 \le \underline\theta < \bar\theta$. The type space is $\Theta = [\underline\theta, \bar\theta]^N$ and $f(\theta) = \prod_i f_i(\theta_i)$.

A direct mechanism is a decision rule $q : \Theta \to \{0,1\}$ and transfer rules $t_i : \Theta \to \mathbb R$. For agent $i$ reporting $\theta_i$, $Q_i(\theta_i)$ is the probability of production and $T_i(\theta_i)$ the expected transfer, taken over the other agents' types, and $U_i(\theta_i) = Q_i(\theta_i)\theta_i - T_i(\theta_i)$. The mechanism is incentive compatible (IC) if $\theta_i Q_i(\theta_i) - T_i(\theta_i) \ge \theta_i Q_i(\theta_i') - T_i(\theta_i')$ for all $i, \theta_i, \theta_i'$, and individually rational (IR) if $U_i(\theta_i) \ge 0$ for all $i, \theta_i$. It is ex post budget balanced if $\sum_i t_i(\theta) \ge c\,q(\theta)$ for every $\theta$, and ex ante budget balanced if this inequality holds after integrating both sides against $f$.

Welfare is $(\sum_i \theta_i)\, g - \sum_i t_i$. The first best decision rule is $q^*(\theta) = 1$ if $\sum_i \theta_i \ge c$ and $0$ otherwise; a first best mechanism uses $q^*$ and transfers that add up to exactly $c\,q^*(\theta)$ in every state. The pivot mechanism uses $q^*$ and

$$t_i(\theta) = \underline\theta\, q^*(\underline\theta,\theta_{-i}) + \big(q^*(\theta) - q^*(\underline\theta,\theta_{-i})\big)\Big(c - \sum_{j\ne i}\theta_j\Big).$$

The virtual valuation is $\psi_i(\theta_i) = \theta_i - (1-F_i(\theta_i))/f_i(\theta_i)$, and $F_i$ is regular if $\psi_i$ is strictly increasing.

Formalization targets

Goal: Proposition 3.7

$$\exists\ \text{an IC and IR first best mechanism} \iff N\underline\theta \ge c \ \text{ or }\ N\bar\theta \le c .$$

In the two cases on the right, producing is efficient for every type vector or for none; in every other case efficient provision cannot be financed voluntarily.

Milestones

1. Proposition 3.6: every ex ante budget balanced mechanism has an equivalent ex post budget balanced one.
2. Lemma 3.6: the pivot mechanism is IC and IR.
3. Lemma 3.7: among IC and IR mechanisms with decision rule $q^*$, the pivot mechanism has the largest expected budget surplus.
4. Lemma 3.8: if $N\underline\theta < c < N\bar\theta$, the pivot mechanism's expected budget surplus is negative.
5. Proposition 3.8 (second best): under regularity and $N\underline\theta < c < N\bar\theta$, an IC, IR, ex ante budget balanced mechanism maximizes expected welfare among such mechanisms iff for some $\lambda > 0$

$$q(\theta) = 1 \iff \sum_i \theta_i > c + \sum_i \frac{\lambda}{1+\lambda}\,\frac{1-F_i(\theta_i)}{f_i(\theta_i)},$$

the budget binds, $\int_\Theta q(\theta)\big[\sum_i \psi_i(\theta_i) - c\big] f(\theta)\,d\theta = 0$, and $T_i(\theta_i) = \theta_i Q_i(\theta_i) - \int_{\underline\theta}^{\theta_i} Q_i(x)\,dx$. 6. Proposition 3.9 (profit maximization): under regularity, the profit-maximizing IC and IR mechanism produces iff $\sum_i \theta_i > c + \sum_i (1-F_i(\theta_i))/f_i(\theta_i)$, with the same formula for $T_i$. 7. Proposition 3.10 (Example 3.3: $N=2$, uniform types on $[0,1]$, $0<c<2$): the second best produces iff $\theta_1+\theta_2 > s$, where $s$ is the unique root in $[0,1]$ of $-\tfrac23 s^3 + s^2 - (1-\tfrac12 s^2)c = 0$ if $c < 2/3$, and $s = \tfrac12 + \tfrac34 c$ if $c \ge 2/3$. 8. Proposition 3.11 (same example): the profit maximizer produces iff $\theta_1+\theta_2 > 1 + \tfrac12 c$.

Significance

Proposition 3.7 says that with voluntary participation no mechanism both takes efficient production decisions and pays for them, outside the degenerate cases. It is the reason the rest of the section, and much of the applied literature on public goods, studies constrained optimum mechanisms: Proposition 3.8 describes what the best budget-respecting mechanism gives up (it undersupplies the good, producing only when valuations exceed a bound strictly above the cost), and Proposition 3.9 quantifies the further distortion under a monopoly supplier. The example makes the three thresholds explicit and comparable.

All results of the section are classical and proved in the book, several of them only sketched there (Proposition 3.9 is stated without proof; Proposition 3.8 invokes an infinite-dimensional Kuhn–Tucker theorem whose applicability is not checked). None of them is formalized in Lean. The mission produces a machine-checked account of the envelope and revenue-equivalence arguments with interim expectations over independent types, a checked pivot-mechanism deficit computation, and a checked Lagrangian characterization; the uniform example additionally certifies the book's arithmetic.

Difficulty

The naive argument for the goal fails at the first step: a mechanism that implements $q^*$ with a balanced budget in every state is not obviously comparable to one that is only IC and IR, because IC constrains interim expectations while budget balance is ex post. The impossibility needs a reduction of the whole class of IC, IR mechanisms with rule $q^*$ to a single extremal one, which requires the payoff equivalence formula for interim utilities and an exact integral identity for expected revenue in terms of virtual valuations. The strict deficit of the pivot mechanism then needs a case analysis over which agents are pivotal and a positive-probability argument. For Proposition 3.8, pointwise maximization of a Lagrangian is not enough: one must show the multiplier exists and is positive, that the maximizer satisfies the monotonicity constraint, and that uniqueness holds only up to null sets.

Formalization scope

Agents are Fin N with $N \ge 2$; types are vectors in Fin N → ℝ; the type distribution is the product of the marginal measures $f_i(x)\,dx$ on $[\underline\theta,\bar\theta]$, which encodes independence. $Q_i$ and $T_i$ integrate the decision and transfer rules against this distribution with agent $i$'s coordinate overwritten by her report. Decision rules are deterministic, with values in $\{0,1\}$ on $\Theta$, as in Definition 3.4. Ties in the first best rule produce, as in the book's note 2 to Chapter 3; the second best and profit-maximizing rules use strict inequalities, as printed.

The book omits measurability and the existence of conditional expectations; the class of direct mechanisms here requires $q$ and each $t_i$ to be Borel measurable, each $t_i$ integrable, and each conditional expectation of $t_i$ given one agent's type to exist. The characterizations in Propositions 3.8–3.11 are stated in two directions: the stated rule, for every $\theta$, is sufficient; necessity holds for almost every $\theta$, since changing $q$ on a null set of type vectors changes nothing that is optimized. The explicit formulas the mission commits to are: the pivot transfers above; the second best rule with multiplier $\lambda > 0$ and the binding budget identity; $T_i(\theta_i) = \theta_i Q_i(\theta_i) - \int_{\underline\theta}^{\theta_i} Q_i$; the cubic $-\tfrac23 s^3 + s^2 - (1-\tfrac12 s^2)c = 0$ for $c < 2/3$; $s = \tfrac12 + \tfrac34 c$ for $c \ge 2/3$; and $s = 1 + \tfrac12 c$ for the profit maximizer.

A trivializing formalization of the goal takes "first best" to mean only the decision rule $q^*$; the pivot mechanism would then be a witness in every case, so first best here also requires transfers adding up to exactly $c\,q^*(\theta)$ in every state.

Reusable infrastructure includes interim expectations over independent product distributions, the payoff and revenue equivalence lemmas for IC mechanisms, and the virtual-valuation identity for expected revenue; these are shared with the auction and bilateral trade chapters of the series. Contributions to any milestone, and to general lemmas about product measures with densities on boxes, are welcome.

Selected references

• T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, §3.3. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
• C. d'Aspremont and L.-A. Gérard-Varet, Incentives and incomplete information, Journal of Public Economics 11 (1979) 25–45. https://doi.org/10.1016/0047-2727(79)90043-4
• W. Güth and M. Hellwig, The private supply of a public good, Zeitschrift für Nationalökonomie, Supplement 5 (1986) 121–159.
• R. B. Myerson and M. A. Satterthwaite, Efficient mechanisms for bilateral trading, Journal of Economic Theory 29 (1983) 265–281. https://doi.org/10.1016/0022-0531(83)90048-0
• D. G. Luenberger, Optimization by Vector Space Methods, Wiley, 1969.

Why revenue-maximizing auctions matter

A seller with one indivisible good and several potential buyers, each of whom privately knows how much the good is worth to them, has to choose a selling procedure: a posted price, an English auction, a sealed-bid auction with a reserve price, or something more elaborate. Which procedure raises the most expected revenue? Myerson's answer (Myerson 1981) is the foundation of optimal auction design. It underlies reserve-price setting in practice, the analysis of sponsored-search and ad-exchange auctions, and the modern algorithmic mechanism design literature, which treats Myerson's auction as the benchmark against which simple and approximately optimal auctions are measured.

This mission formalizes Section 3.2 of Tilman Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), the textbook treatment of Myerson's result in the independent private values model with Bayesian incentive compatibility. It is the second mission of a series covering the book.

Timeline. Vickrey (1961) showed that the second-price auction makes truthful bidding a dominant strategy and compared auction formats. Myerson (1981) characterized the revenue-maximizing mechanism for independent private values with possibly asymmetric distributions; Riley and Samuelson (1981) obtained the symmetric case and the optimal reserve price independently. The revelation principle in the Bayesian form used here goes back to Myerson (1979) and Dasgupta, Hammond and Maskin (1979).

Setting

There are $N \ge 2$ potential buyers $i \in I = \{1,\dots,N\}$. Buyer $i$ values the good at $\theta_i$; if he receives it and pays $t_i$ his utility is $\theta_i - t_i$, and otherwise $-t_i$. The seller's utility is $\sum_i t_i$. The valuations $\theta_1,\dots,\theta_N$ are independent; $\theta_i$ has cumulative distribution function $F_i$ and density $f_i$ with $f_i(\theta_i) > 0$ on the common support $[\underline\theta, \bar\theta]$, where $0 \le \underline\theta < \bar\theta$. The type space is $\Theta = [\underline\theta,\bar\theta]^N$ and the joint density is $f(\theta) = \prod_i f_i(\theta_i)$.

A direct mechanism asks buyers to report their types and consists of an allocation rule $q : \Theta \to \Delta$, where $\Delta = \{(q_1,\dots,q_N) : 0 \le q_i \le 1,\ \sum_i q_i \le 1\}$, and payment rules $t_i : \Theta \to \mathbb R$. Its interim quantities are the expected allocation probability, payment and utility of buyer $i$ conditional on his own type:

$$Q_i(\theta_i) = \int_{\Theta_{-i}} q_i(\theta_i,\theta_{-i}) f_{-i}(\theta_{-i})\,d\theta_{-i},\quad T_i(\theta_i) = \int_{\Theta_{-i}} t_i(\theta_i,\theta_{-i}) f_{-i}(\theta_{-i})\,d\theta_{-i},\quad U_i = \theta_i Q_i - T_i.$$

The mechanism is incentive-compatible if $\theta_i Q_i(\theta_i) - T_i(\theta_i) \ge \theta_i Q_i(\theta_i') - T_i(\theta_i')$ for all $i,\theta_i,\theta_i'$ (truth-telling is a Bayesian Nash equilibrium) and individually rational if $U_i(\theta_i) \ge 0$ for all $i,\theta_i$. The virtual valuation of buyer $i$ is

$$\psi_i(\theta_i) = \theta_i - \frac{1 - F_i(\theta_i)}{f_i(\theta_i)},$$

and the distribution $F_i$ is regular if $\psi_i$ is strictly increasing.

Formalization targets

Goal: Myerson's optimal auction (Proposition 3.4)

Under regularity, among all incentive-compatible and individually rational direct mechanisms, a mechanism maximizes the seller's expected revenue $\mathbb E[\sum_i t_i(\theta)]$ exactly when, for every buyer $i$,

$$q_i(\theta) = \begin{cases}1 & \text{if } \psi_i(\theta_i) > 0 \text{ and } \psi_i(\theta_i) > \psi_j(\theta_j) \text{ for all } j \ne i,\\ 0&\text{otherwise,}\end{cases}\qquad T_i(\theta_i) = \theta_i Q_i(\theta_i) - \int_{\underline\theta}^{\theta_i} Q_i(x)\,dx,$$

the allocation identity holding for almost every $\theta$; and such a mechanism exists.

Milestones

1. Proposition 3.1, the revelation principle: every Bayesian Nash equilibrium of every mechanism is replicated by truth-telling in an incentive-compatible direct mechanism.
2. Lemmas 3.1–3.4: incentive compatibility makes $Q_i$ increasing and $U_i$ convex with $U_i' = Q_i$; payoff equivalence $U_i(\theta_i) = U_i(\underline\theta) + \int_{\underline\theta}^{\theta_i} Q_i$; revenue equivalence for $T_i$.
3. Proposition 3.2: incentive compatibility holds if and only if every $Q_i$ is increasing and the revenue-equivalence formula holds.
4. Proposition 3.3: under incentive compatibility, individual rationality is equivalent to $T_i(\underline\theta) \le \underline\theta Q_i(\underline\theta)$.
5. Lemma 3.5: an optimal mechanism has $T_i(\underline\theta) = \underline\theta Q_i(\underline\theta)$.
6. Eqs. (3.4)–(3.5): expected revenue equals expected virtual surplus $\sum_i \int_\Theta q_i(\theta)\psi_i(\theta_i) f(\theta)\,d\theta$.
7. Proposition 3.5: a mechanism maximizes expected welfare $\mathbb E[\sum_i q_i(\theta)\theta_i]$ among incentive-compatible, individually rational mechanisms if and only if it gives the good to the highest value (almost everywhere) and $T_i(\theta_i) \le \theta_i Q_i(\theta_i) - \int_{\underline\theta}^{\theta_i}Q_i$.

Significance

The theorem identifies the revenue-maximizing selling procedure among all procedures, not among a parametric family: by the revelation principle, no auction format, however elaborate, and no equilibrium of it can beat the mechanism of Proposition 3.4. Its consequences include the optimality of first- and second-price auctions with reserve price $\psi^{-1}(0)$ when buyers are symmetric, the revenue equivalence of standard auction formats, the fact that an asymmetric optimal auction may sell to a buyer without the highest value, and the monopoly inefficiency that the optimal seller sometimes withholds the good. The envelope characterization of Bayesian incentive compatibility (Proposition 3.2) is the tool reused throughout the rest of the book, in public goods provision, bilateral trade and dynamic screening.

The result is classical and fully proved in the literature. What is missing is a machine-checked version at this generality: asymmetric distributions, an arbitrary lower support end $\underline\theta \ge 0$, Bayesian (interim) rather than dominant-strategy constraints, and optimality over all incentive-compatible and individually rational mechanisms. Existing formalizations on the platform treat the i.i.d. case with values on $[0,\bar v]$.

Difficulty

The obvious argument maximizes the virtual surplus $\sum_i q_i(\theta)\psi_i(\theta_i)$ pointwise and declares victory, but this ignores that the seller's feasible set is constrained by monotonicity of every $Q_i$; the pointwise maximizer is feasible only because regularity makes $\psi_i$ increasing, and that has to be proved for the interim probabilities, which integrate over the other buyers' types. The revenue identity links interim payments, which integrate over the other buyers' types, to an integral over the whole type space weighted by the virtual valuation, and it is only valid for mechanisms whose lowest types' payments are pinned down. The necessity direction requires showing that ties and zero virtual values are null events, which rests on strict monotonicity of every $\psi_i$ and on the absolute continuity of the type distribution. Finally, the envelope step requires convexity and almost-everywhere differentiability of $U_i$, with care at the endpoints of the type interval.

Formalization scope

Buyers form a finite type with at least two elements. The prior is the measure on $\mathbb R^N$ with density $\prod_i f_i(\theta_i)$ on $\Theta$ and no mass outside it; each $f_i$ is measurable, strictly positive on $[\underline\theta,\bar\theta]$ and integrates to $1$; $F_i(\theta_i) = \int_{\underline\theta}^{\theta_i} f_i$. Allocation and payment rules are total functions whose values on $\Theta$ are constrained, and $Q_i$, $T_i$ are prior expectations with the $i$-th coordinate fixed. "Increasing" is weak monotonicity, as in the book; regularity is strict monotonicity of $\psi_i$ on $[\underline\theta,\bar\theta]$ (Assumption 3.1).

The following conventions are committed to:

• Measurability. The book omits measurability throughout. The comparison class for optimality consists of mechanisms with measurable $q_i, t_i$, integrable $t_i$, and integrable sections $\theta_{-i}\mapsto t_i(\theta_i,\theta_{-i})$. Without these hypotheses the Lean integrals would be $0$ and revenue comparisons would be meaningless.
• Almost-everywhere characterizations. Propositions 3.4 and 3.5 are printed with "for all $\theta \in \Theta$". Changing $q$ on a null set of type vectors changes neither incentives nor revenue nor welfare, so the "only if" directions hold only almost everywhere; they are stated for almost every $\theta$, and the existence of a mechanism satisfying the allocation rule at every $\theta$ is stated separately. The payment conditions hold for every $\theta_i$.
• Explicit formulas. The goal states Myerson's allocation rule and the payment formula $T_i(\theta_i) = \theta_i Q_i(\theta_i) - \int_{\underline\theta}^{\theta_i} Q_i(x)\,dx$ explicitly. Proposition 3.5 states the efficient rule $q_i(\theta) = 1$ iff $\theta_i > \theta_j$ for all $j \ne i$, and the payment inequality. A statement asserting only that some optimal mechanism exists, or only that the optimal auction is efficient, would not be this theorem.
• Revelation principle. A general mechanism has arbitrary measurable message sets and an outcome function giving allocation probabilities in $\Delta$ and expected transfers; equilibria are in pure type-contingent strategies. A version in which the mechanism is already direct would be trivial and is not the statement.
• Interim constraints. Incentive compatibility and individual rationality are Bayesian and interim, not dominant-strategy or ex post; the latter are the subject of a later mission.
• Endpoints in Lemma 3.2. Differentiability of $U_i$ and $U_i' = Q_i$ are stated at interior points of $[\underline\theta,\bar\theta]$.

The envelope and payoff-equivalence lemmas, and the revenue identity, are reused in later missions of this series, so proofs of the milestones are welcome independently of the goal.

Selected references

• Tilman Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, §3.2, pp. 31–45. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
• Roger B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 58–73, 1981. https://doi.org/10.1287/moor.6.1.58
• John G. Riley and William F. Samuelson, Optimal Auctions, American Economic Review 71(3), 381–392, 1981. https://www.jstor.org/stable/1802786
• William Vickrey, Counterspeculation, Auctions, and Competitive Sealed Tenders, Journal of Finance 16(1), 8–37, 1961. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
• Roger B. Myerson, Incentive Compatibility and the Bargaining Problem, Econometrica 47(1), 61–73, 1979. https://doi.org/10.2307/1912346
• Partha Dasgupta, Peter Hammond and 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