Algorithmic Game Theory

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

Motivation

A seller with one good and one buyer whose valuation she does not know faces the simplest problem of mechanism design: choose a selling procedure, anticipating that the buyer will act in his own interest given what he knows. The textbook answer, "post the monopoly price", is usually derived by optimizing over prices alone. The question that opens Börgers' An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015, doi:10.1093/acprof:oso/9780199734023.001.0001) is whether the seller could do better with anything else: negotiation, lotteries, menus of price–probability pairs, or any extensive game she can commit to.

Chapter 2 answers this for one buyer, and in doing so introduces the tools the rest of the book, and most of auction theory, reuse: the revelation principle, the envelope characterization of incentive compatibility, payoff and revenue equivalence, and the virtual valuation. The book's exposition of §2.2 follows Manelli and Vincent (2007), and the nonlinear pricing model of §2.3 is due to Mussa and Rosen (1978, doi:10.1016/0022-0531(78)90085-6); both attributions are the book's own (§2.5, p.29).

Setting

The buyer's type $\theta$ is his valuation for the good. His utility is $\theta-t$ if he receives the good and pays $t$, and $-t$ if he only pays $t$. The seller's belief about $\theta$ is a cumulative distribution function $F$ with density $f$ on an interval $[\underline\theta,\bar\theta]$, $0\le\underline\theta<\bar\theta$, with $f(\theta)>0$ throughout and $F(\theta)=\int_{\underline\theta}^{\theta}f(x)\,dx$.

A direct mechanism is a pair $q:[\underline\theta,\bar\theta]\to[0,1]$, $t:[\underline\theta,\bar\theta]\to\mathbb R$: the buyer reports a type $\theta'$, receives the good with probability $q(\theta')$ and pays $t(\theta')$. Write $u(\theta)=\theta q(\theta)-t(\theta)$. The mechanism is incentive-compatible if $u(\theta)\ge\theta q(\theta')-t(\theta')$ for all $\theta,\theta'$, and individually rational if $u(\theta)\ge 0$ for all $\theta$. The seller's expected revenue is $\int_{\underline\theta}^{\bar\theta}t(\theta)f(\theta)\,d\theta$.

For the extreme-point argument, $\mathcal F$ denotes the space of functions on $[\underline\theta,\bar\theta]$ with the $L^1$ norm, and $M\subset\mathcal F$ the set of increasing functions with values in $[0,1]$. A point $x$ of a convex set $C$ is an extreme point if for every $y\neq 0$ at least one of $x+y$, $x-y$ lies outside $C$.

In the nonlinear pricing model of §2.3 the good is divisible, quantity $q\ge 0$ costs the seller $cq$ with $c>0$, and the buyer's utility is $\theta\nu(q)-t$, with $\nu(0)=0$, $\nu'>0$, $\nu''<0$, $\bar\theta\nu'(0)>c$ and $\lim_{q\to\infty}\bar\theta\nu'(q)<c$. The seller maximizes expected profit $\int(t-cq)f$. The distribution $F$ is regular if the virtual valuation $\theta-(1-F(\theta))/f(\theta)$ is increasing.

Formalization targets

Goal: Proposition 2.5, a posted price is optimal

If $p^*\in\arg\max_{p\in[\underline\theta,\bar\theta]}p(1-F(p))$, then the mechanism

$$q(\theta)=\begin{cases}1&\theta>p^*\\0&\theta<p^*\end{cases},\qquad t(\theta)=\begin{cases}p^*&\theta>p^*\\0&\theta<p^*\end{cases}$$

maximizes expected revenue among all incentive-compatible, individually rational direct mechanisms. The comparison class contains every randomized rule $q$ with values in $[0,1]$; the statement fixes no distribution and no constant.

Milestones on the way

1. Proposition 2.1: every mechanism and optimal buyer strategy can be replaced by a truthful direct mechanism with the same outcomes.
2. Lemmas 2.1–2.4: incentive compatibility forces $q$ increasing, $u$ increasing and convex with $u'=q$, and

$$u(\theta)=u(\underline\theta)+\int_{\underline\theta}^{\theta}q(x)\,dx,\qquad t(\theta)=t(\underline\theta)+\big(\theta q(\theta)-\underline\theta q(\underline\theta)\big)-\int_{\underline\theta}^{\theta}q(x)\,dx.$$

3. Propositions 2.2–2.3 and Lemma 2.5: these conditions characterize incentive compatibility; individual rationality reduces to $u(\underline\theta)\ge0$; at the optimum $t(\underline\theta)=\underline\theta q(\underline\theta)$.
4. Lemma 2.6, Proposition 2.4, Lemma 2.7: $M$ is compact and convex, a linear function continuous on a compact convex set attains its maximum at an extreme point, and the extreme points of $M$ are the $\{0,1\}$-valued functions.
5. Proposition 2.6: under regularity, $q(\theta)=0$ when $\nu'(0)\big(\theta-\tfrac{1-F(\theta)}{f(\theta)}\big)\le c$, otherwise $\nu'(q(\theta))\big(\theta-\tfrac{1-F(\theta)}{f(\theta)}\big)=c$, with $t(\theta)=\theta\nu(q(\theta))-\int_{\underline\theta}^{\theta}\nu(q(x))\,dx$, maximizes expected profit.

Significance

Proposition 2.5 says that the elementary monopoly price is not a restriction of the seller's options but the solution of the unrestricted design problem, including every lottery and every indirect procedure. Its one-buyer argument is the template for Myerson's optimal auction (Chapter 3 of the book), whose revenue formula is the multi-buyer form of Lemma 2.4. Proposition 2.6 exhibits the two standard features of screening, no distortion at the top and downward distortion below, which recur in regulation, insurance and contract theory.

All results of the chapter are classical and proved in the book. None of them is formalized on Prove2Me, and Mathlib has neither the revelation principle, the envelope lemma for incentive-compatible mechanisms, nor a maximum principle for linear functions on compact convex sets (Mathlib has the Krein–Milman lemma, IsCompact.extremePoints_nonempty, but not Bauer's maximum principle). The mission therefore produces the first machine-checked foundation for the one-agent screening model on which chapters 3, 4 and 11 of the book build.

Difficulty

The obvious argument for the goal compares the posted price with other posted prices; that comparison is one line and is not the theorem. The content is the comparison with randomized mechanisms: an arbitrary increasing $q$ with values in $[0,1]$ may do better than every deterministic threshold rule unless one shows that expected revenue is linear in $q$ and that its maximum over the infinite-dimensional set $M$ is attained at an extreme point. That step needs compactness of $M$ in $L^1$ and a maximum principle on compact convex sets in a normed space, neither of which is finite-dimensional linear programming. The envelope step (Lemma 2.3) needs absolute continuity of a convex function on a closed interval, including its endpoints, where $u$ need not be differentiable. For Proposition 2.6 the pointwise maximizer of the virtual surplus must be shown to be monotone and to satisfy incentive compatibility, which is where regularity enters.

Formalization scope

Types are real numbers; every function of the type is a total function $\mathbb R\to\mathbb R$ and every condition quantifies over $[\underline\theta,\bar\theta]$ only. "Increasing" means weakly increasing (the book's note 3). The distribution is a structure carrying the density $f$, positive and integrable on $[\underline\theta,\bar\theta]$ with total mass $1$, and $F$ tied to it by $F(\theta)=\int_{\underline\theta}^{\theta}f$. No measurability or integrability hypothesis is placed on mechanisms: incentive compatibility makes $q$ monotone and $t$ bounded and measurable, so every expected revenue is a genuine integral.

The explicit formulas are part of the statements: the posted-price mechanism of Proposition 2.5 with $p^*\in\arg\max p(1-F(p))$; the payment formulas of Lemmas 2.3–2.4 and Proposition 2.2; $t(\underline\theta)=\underline\theta q(\underline\theta)$ in Lemma 2.5; and in Proposition 2.6 the two-case rule for $q$ and the payment $t(\theta)=\theta\nu(q(\theta))-\int_{\underline\theta}^{\theta}\nu(q(x))\,dx$. The goal fixes $q(p^*)=1$, $t(p^*)=p^*$ for existence and quantifies over every incentive-compatible, individually rational completion at the tie.

The space $\mathcal F$ is $L^1([\underline\theta,\bar\theta])$ of almost-everywhere classes, because the book's $L^1$ "norm" on bounded functions vanishes on null functions; $M$ is the set of classes with an increasing $[0,1]$-valued representative, and Lemma 2.7 is an almost-everywhere statement, as the book's notes 4–6 already indicate. Proposition 2.4 is stated for a nonempty compact convex set in a real normed space and a linear map continuous on that set. The revelation principle models a general mechanism as the buyer's reduced strategy set, an arbitrary type, with a purchase probability and an expected payment for each strategy.

A goal that compared the posted price only with other posted prices, or only with deterministic mechanisms, would be trivial and is excluded: the competitors range over all incentive-compatible, individually rational direct mechanisms with $q$ valued in $[0,1]$.

Reusable beyond this mission: the one-agent envelope and revenue-equivalence lemmas (needed again in Chapters 3, 4 and 11), compactness of monotone functions in $L^1$, and the maximum principle for linear functions on compact convex sets. Contributions to any of these are 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. doi:10.1093/acprof:oso/9780199734023.001.0001
• M. Mussa and S. Rosen, "Monopoly and product quality", Journal of Economic Theory 18(2), 1978. doi:10.1016/0022-0531(78)90085-6
• E. A. Ok, Real Analysis with Economic Applications, Princeton University Press, 2007 (Extreme Point Theorem, p.658), cited by the book at p.16.

Motivation

Chapter IX of von Neumann and Morgenstern's Theory of Games and Economic Behavior asks when a game played by many participants is really several separate games played side by side. The authors' motivation (41.1) is methodological: the general theory of the $n$-person game becomes unmanageable as $n$ grows, and one way to gain insight into large games is to isolate classes of games that can be analysed exactly. The first such class consists of games whose players fall into groups that have no dealings with each other — the book's example is the internal economies of two countries whose connections are disregarded (41.2.4). Such a game is the composition of its constituents, and the question of the chapter is how to recognise a composite game from its characteristic function alone and how far a given game can be decomposed.

The answer (§43) is a structure theorem. The groups of players that can be split off form a Boolean algebra of sets; its atoms, the minimal splitting sets, form a partition of the set of players, the decomposition partition $\Pi_\Gamma$; and every splitting set is a union of blocks of $\Pi_\Gamma$. The book remarks (41.3.3) that the splitting condition (41:7) is exactly Carathéodory's criterion of measurability, transported from measures to characteristic functions. The mission formalizes §43, together with the criterion (42:G) of §42 on which it rests.

Setting

Let $I$ be a finite set of players. A characteristic function is a real number $v(S)$ for every subset $S \subseteq I$ (every coalition, including the empty set $\ominus$ and $I$). Write $-S = I - S$. From 42.4.1 on the book works in the domain of constant-sum games, whose characteristic functions are, by (42:D), exactly the functions satisfying

$$\text{(42:6:a)}\ v(\ominus) = 0,\qquad \text{(42:6:b)}\ v(S) + v(-S) = v(I),\qquad \text{(42:6:c)}\ v(S) + v(T) \leqq v(S \cup T)\ \text{ if } S \cap T = \ominus .$$

For $J \subseteq I$ with complement $K = I - J$, the game is decomposable with respect to $J$ and $K$ if there are constant-sum games $\Delta$ on the players $J$ and $\mathrm H$ on the players $K$ with $v(R) = v_\Delta(R \cap J) + v_{\mathrm H}(R \cap K)$ for all $R \subseteq I$ — formula (41:3). The $J$-constituent $\Delta$ is the game on $J$ with $v_\Delta(S) = v(S)$ for $S \subseteq J$ (41:4).

A splitting set (43.1) is a $J \subseteq I$ satisfying (41:6),

$$v(S \cup T) = v(S) + v(T) \quad \text{for } S \subseteq J,\ T \subseteq I - J .$$

The game is indecomposable if $\ominus$ and $I$ are its only splitting sets (43.3.1). A minimal splitting set is a splitting set $J \neq \ominus$ none of whose proper subsets $J' \neq \ominus$ is splitting (43.3.2), and $\Pi_\Gamma$ is the system of all minimal splitting sets. The game is inessential (42:F) if it is strategically equivalent to the zero game, i.e. $v(S) + \sum_{k \in S} \alpha^0_k = 0$ for all $S$, for some reals $\alpha^0_k$ (the transformation (42:5)).

Formalization targets

Goal: (43:F), (43:G), (43:H)

For every $v$ satisfying (42:6:a)–(42:6:c):

$$J_1 \neq J_2 \in \Pi_\Gamma \Rightarrow J_1 \cap J_2 = \ominus, \qquad \bigcup_{J \in \Pi_\Gamma} J = I, \qquad K \text{ splitting} \iff K = J_1 \cup \dots \cup J_p,\ J_i \in \Pi_\Gamma .$$

The goal combines the partition property and the characterization of all splitting sets; it is the book's own summary of §43.3 and does not presuppose that $\Pi_\Gamma$ is a partition.

Milestones

In attack order: the criterion (42:G) (decomposability $\iff$ (41:6) $\iff$ (41:7)); the closure properties (43:A) (complements), (43:B) ($\ominus$, $I$), (43:C) (intersections and unions); (43:D) (splitting sets of a constituent) and (43:E) (a constituent is indecomposable iff its set is minimal); (43:F), (43:G) separately; (43:I) (a minimal splitting set is disjoint from, or inside, any splitting set); the restatement (43:H*) ($K$ splits iff every block of $\Pi_\Gamma$ lies inside or outside $K$); and the two extreme cases (43:J) ($\Pi_\Gamma$ = all singletons iff the game is inessential) and (43:K) ($\Pi_\Gamma = \{I\}$ iff the game is indecomposable).

Significance

The decomposition partition is canonical: every constant-sum game splits uniquely into indecomposable constituents, and (43:E) identifies them as the constituents on the blocks of $\Pi_\Gamma$. The two extreme cases (43:J), (43:K) show that inessentiality and indecomposability are opposite ends of one scale. Chapter IX uses this structure in §§44–47, where solutions of decomposable games are related to solutions of their constituents ((46:A)–(46:I)); a formal decomposition partition is the prerequisite for that later work, and a candidate follow-up mission.

The results are classical and proved in the book. The mission's contribution is a machine-checked version: a formal definition layer for splitting sets of a set function on a finite set, the Boolean-algebra closure, and the atomic decomposition. The combinatorial core — that the sets satisfying a Carathéodory-type additivity condition form a Boolean algebra of a finite set, whose atoms partition it — is reusable outside game theory (for instance for finitely additive decompositions of set functions). No machine-checked version of these results is known to exist; they are formalized here for the first time as far as a search of the platform shows.

Difficulty

The individual steps are elementary, but the obvious argument for the key closure property (43:C) fails: to show that $J' \cup J''$ is splitting one cannot simply add the identities (41:6) for $J'$ and for $J''$, since a pair $S \subseteq J' \cup J''$, $T \subseteq I - (J' \cup J'')$ is not of the form those identities control, and $J' \cap J''$ may be nonempty — the book's footnote on p. 354 singles out overlapping splitting sets as the case its proof is really about. Likewise (43:D) is not a tautology: that a set self-contained within a self-contained set is self-contained in the whole game has to be proved (footnote 1, p. 355). Formally, the main work is bookkeeping of set identities and the passage between subsets of $J$ (players of the constituent) and subsets of $I$.

Formalization scope

• Players. The set of players $I$ is an arbitrary finite type ι with decidable equality (the book's $I = (1, \dots, n)$; in Chapter IX players are also named $1', \dots, k', 1'', \dots, l''$). Coalitions are Finset ι, $-S$ and $I - J$ are the complement Sᶜ in $I$, and $v$ is a function Finset ι → ℝ.
• Standing hypotheses. Every theorem assumes (42:6:a)–(42:6:c) (the structure IsConstantSum), the chapter's domain from 42.5.3 on ("in the remainder of this chapter we will continue to consider constant-sum games", p. 353). $v(I)$ is arbitrary: the statements are not restricted to zero-sum games, which would be a weaker special case. (43:K) additionally assumes $I$ nonempty ([Nonempty ι], the book's $n \geqq 1$); every other statement holds without it. (43:E) assumes $J \neq \ominus$, since the book's constituent is a game and has at least one player.
• Characteristic functions only. Games are represented by their characteristic functions, as the book does throughout §§42–43 by (42:D). Decomposability quantifies over constant-sum characteristic functions $v_\Delta$, $v_{\mathrm H}$ on the subtypes ↥J, ↥Jᶜ; the $J$-constituent is $v$ restricted to subsets of ↥J. Sums of sets are unions; "disjunct" is Disjoint.
• Π_Γ. decompositionPartition v is the set of minimal splitting sets; that it is a partition is proved, not assumed. An aggregate of minimal splitting sets is a finite family A, its sum A.sup id; the empty aggregate gives $\ominus$.
• No trivialization. A definition of splitting sets that quantified over $T \subseteq I$ instead of $T \subseteq I - J$, or complements taken in an ambient type larger than $I$, would change the theorems; here the complement is in the finite type of players itself. With $I$ empty all statements except (43:K) hold trivially, and (43:K) carries the nonemptiness hypothesis.
• Contributions welcome. Proofs of the milestones in the listed order; general Mathlib-style lemmas on Boolean subalgebras of Finset ι and their atoms, which would shorten (43:F)–(43:H).

Selected references

• J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (page-for-page reprint of the 3rd edition, 1953), Chapter IX, §§41–43, pp. 339–357. https://doi.org/10.1515/9781400829460
• C. Carathéodory, Vorlesungen über reelle Funktionen, Teubner, Leipzig–Berlin, 1918, Chapter V (the measurability criterion to which (41:7) corresponds, cited by the book on p. 343).

Motivation

Retailers hold point-of-sale data that their suppliers cannot observe, and large retailers sell access to it through data-sharing programs (Costco's CRX, Walmart's Retail Link and similar programs). When one retailer carries the substitutable products of two competing manufacturers, sharing its demand information is a strategic decision: a manufacturer who knows the demand signal sets his wholesale price in response to it, which changes the retailer's margin and the rival manufacturer's order uncertainty. Whether the retailer should sell the information, to how many manufacturers, and by which protocol, is the question of Shang, Ha and Tong (Management Science 62(1):245–263, 2016).

The paper belongs to the information-sharing literature of Li (2002), Li and Zhang (2008) and Ha, Tong and Zhang (2011), which studies competing supply chains or a single chain. The common-retailer structure differs: the retailer can price-discriminate between the manufacturers through the order in which she offers the information.

Setting

Two manufacturers $i \in \{1, 2\}$ sell substitutable products through one retailer. The demand for product $i$ is

$$q_i = a + \theta - (1+\phi)p_i + \phi p_j,$$

where $p_i$ is the retail price, $\phi > 0$ measures competition, and $\theta$ is a random shock with mean $0$ and variance $\sigma^2 > 0$. The retailer observes a demand signal $Y$ that is unbiased, $E[Y \mid \theta] = \theta$, and has linear expectation: $E[\theta \mid Y] = \beta Y$ for a weight $\beta$ (in the paper $\beta = t\sigma^2/(1+t\sigma^2)$, with $t$ the signal accuracy). The retailing cost is zero, and manufacturer $i$ produces $q$ units at cost $bq + c_d q^2$ with $b, c_d > 0$: a production diseconomy.

The game has four stages.

1. The retailer and the manufacturers contract on information sharing, which fixes each manufacturer's status $X_i \in \{I, U\}$ (informed or uninformed).
2. The retailer observes $Y$ and discloses it truthfully to the informed manufacturers.
3. The manufacturers set wholesale prices $w_i$ simultaneously, an informed one as a function of $Y$. The retailer then sets retail prices.
4. Demand realizes and payoffs are received.

The pricing stage is a Bayesian game. Its equilibrium ex ante profits are $\pi_M(n)$, $\pi_M^I(1)$, $\pi_M^U(1)$ for the manufacturers and $\pi_R(n)$ for the retailer, where $n$ is the number of informed manufacturers. They define a payoff table for the contracting stage.

Two contracting protocols are compared.

• Concurrent contracting: the retailer offers both manufacturers the same payment $T$, and they accept or reject simultaneously; a Pareto-optimal pure equilibrium is the outcome, and the retailer chooses $T$.
• Sequential contracting: the retailer offers one manufacturer $T_f$, he accepts or rejects, then the retailer offers the other $T_s$, and he decides having observed the first decision. The retailer cannot commit to $T_s = T_f$, and the solution is subgame perfect equilibrium.

Formalization targets

Goal: Proposition 4(d)

For every $\phi > 0$, $c_d > 0$ and every signal model, the pricing stage has an equilibrium; for every pricing equilibrium, both contracting games have equilibria; and for every concurrent outcome and every sequential subgame-perfect equilibrium (either first mover),

$$\Pi_R^{C} \le \Pi_R^{S}, \qquad \Pi_M^{S} \le \Pi_M^{C},$$

with both inequalities strict when $c_d > (\sqrt2 - 1)/(1+\phi)$. Here $\Pi_R$ is the retailer's profit after side payments and $\Pi_M$ the manufacturers' total profit net of them. The paper's word "higher" is read as $\ge$ because for small $c_d$ neither protocol sells information and all profits coincide.

Milestones

1. §4.1, Eq. (1): the retailer's best response $\hat p_i = \frac12(a + \beta Y + w_i)$ and the resulting demand.
2. Lemma 1: the pricing equilibrium exists, is unique, and is linear in $Y$.
3. §4.2: the closed forms of the seven ex ante profits.
4. Lemma 3: $\pi_M(2) > \pi_M^I(1) > \pi_M(0) > \pi_M^U(1)$, $\pi_R(0) > \pi_R(1) > \pi_R(2)$, $\pi_R(1) - \pi_R(2) > \pi_R(0) - \pi_R(1)$.
5. Proposition 1(b): without contracting, no information is shared.
6. Propositions 2 and 3: thresholds $c_d^C$ and $c_d^{S1}, c_d^{S2}$, depending only on $\phi$, at which the number of informed manufacturers changes under each protocol.
7. Proposition 4(a): $c_d^{S1} < c_d^C < c_d^{S2}$.

Significance

The result. Proposition 4(d) says that the order of the offers transfers surplus: selling information one manufacturer at a time lets the retailer exploit the manufacturers' fear of being the only uninformed firm, which raises her profit and lowers theirs. Propositions 2 and 3 show that concurrent contracting shares with both manufacturers or with neither, while sequential contracting can end with only one informed manufacturer. Together they give a complete map of the equilibrium sharing decisions in $(c_d, \phi)$ (Figure 1 of the paper).

Formalizing it. The results are proved in the paper, partly by "it can be shown" and "straightforward" steps: Lemma 3's proof is omitted, and so is the convexity of the function whose root is $c_d^{S2}$. No part of the paper has a machine-checked proof. A complete formalization would check every such step and make the equilibrium notions precise, in particular the Pareto selection and the tie-breaking at the thresholds, where the retailer is exactly indifferent.

Difficulty

Most of the work is in the contracting stage, not the algebra. The pricing stage must be solved over all square-integrable strategies measurable in the signal. Uniqueness is then almost sure and rests on the linear-expectation identities $E[\theta Y] = \sigma^2$ and $E[Y^2] = \sigma^2/\beta$. The concurrent game has multiple equilibria for intermediate payments, and the retailer's optimum lies at a payment where two equilibria coexist. The sequential game is a three-stage game with a continuum of offers: at each threshold the retailer is indifferent, and an SPE exists only if acceptance at indifference is chosen correctly. The threshold $c_d^{S2}$ has no closed form; it is the root of a convex rational function of $c_d$.

Formalization scope

The Lean development lives in the namespace InfoSharing.Diseconomy. Conventions:

• The probability space carries $\theta$ and $Y$ in $L^2$, with the two conditional-expectation identities holding almost everywhere. $\beta$ is a parameter fixed by $E[\theta \mid Y] = \beta Y$; Ericson's formula for $\beta$ is not formalized.
• Wholesale strategies are measurable, square-integrable functions of the signal value, and constants for an uninformed manufacturer. A pricing equilibrium is ex ante optimality over such strategies, which is equivalent to the paper's conditional optimization. The retailer's rule must be a best response at every wholesale-price pair.
• The payoff table is produced by an arbitrary pricing-equilibrium family, not by the §4.2 closed forms. A formalization that takes the closed forms as the definition of the profits would reduce the goal to algebra and a $2 \times 2$ game, and is ruled out.
• Payments are nonnegative, only pure strategies are used in the contracting games, and the concurrent outcome selects, among Pareto-optimal equilibria, the one best for the retailer.
• Threshold statements use two clauses: the printed value is attained on the closed region, and it is the only value on the region's interior. The thresholds depend only on $\phi$.
• Demands may be negative (θ is unbounded), as in the paper's formulas.

A complete development needs:

• the conditional-expectation algebra behind Lemma 1 and §4.2;
• rational-function inequalities for Lemma 3;
• a case analysis of the two contracting games.

The model layer is shared with the companion mission on production economy.

Selected references

• G. Shang, A. Y. Ha, S. Tong, Information Sharing in a Supply Chain with a Common Retailer, Management Science 62(1):245–263, 2016. https://doi.org/10.1287/mnsc.2014.2127
• W. A. Ericson, A note on the posterior mean of a population mean, Journal of the Royal Statistical Society B 31(2):332–334, 1969.
• L. Li, Information sharing in a supply chain with horizontal competition, Management Science 48(9):1196–1212, 2002. https://doi.org/10.1287/mnsc.48.9.1196.177
• L. Li, H. Zhang, Confidentiality and information sharing in supply chain coordination, Management Science 54(8):1467–1481, 2008. https://doi.org/10.1287/mnsc.1070.0851
• A. Y. Ha, S. Tong, H. Zhang, Sharing imperfect demand information in competing supply chains with production diseconomies, Management Science 57(3):566–581, 2011. https://doi.org/10.1287/mnsc.1100.1295
• X. Vives, Oligopoly Pricing: Old Ideas and New Tools, MIT Press, 1999.

Motivation

Algorithmic mechanism design asks for algorithms whose inputs are held by self-interested agents: the designer can pay the agents, and must choose payments so that each agent's own interest leads it to reveal what the algorithm needs. Nisan and Ronen introduced the framework with task scheduling on unrelated machines as the running example (Nisan–Ronen 2001). In the basic model, where payments depend only on what the agents declare, they showed that no truthful mechanism approximates the optimal make-span within a factor below 2, and that the natural mechanism only reaches a factor $n$.

Their Section 5 changes the information available: in a mechanism with verification the payments may also depend on the times in which the tasks were actually performed. With this extra information, an exact optimizer becomes a strongly truthful mechanism (Theorem 5.1, the Compensation-and-Bonus mechanism). Exact scheduling on unrelated machines is NP-hard, so the question is whether an approximation algorithm can take the optimizer's place. Theorem 5.6 of the paper shows that plugging a non-optimal algorithm into Compensation-and-Bonus destroys truthfulness in general. Theorem 5.9, the subject of this mission, shows that for the bounded problem a specific approximation scheme, the rounding algorithm of Horowitz and Sahni (1976), can be combined with a modified payment rule to give a truthful mechanism whose outcome is within a factor $1+\varepsilon$ of optimal.

Setting

There are $n$ agents and $k$ tasks. Agent $i$ needs time $t^i_j$ for task $j$; the vector $t = (t^i_j)$ is the type vector, and agent $i$ alone knows its row $t^i$. In the bounded scheduling problem (Definition 33) there are fixed numbers $0 < a < b$ with $a \le t^i_j \le b$ for all $i, j$, and every declaration lies in the same range. An allocation $x$ assigns each task to one agent; $x^i$ is the set of tasks of agent $i$.

A strategy of agent $i$ has two parts: a declaration $d^i \in [a,b]^k$, and an execution, which for each decision $x$ of the mechanism specifies the actual time $\tilde t_j \ge t^i_j$ in which agent $i$ performs each task $j \in x^i$. The mechanism chooses $x = x(d)$ from the declarations alone and afterwards observes the actual times $\tilde t$. The objective is the make-span with actual times,

$$g(x,\tilde t) = \max_i \sum_{j \in x^i} \tilde t_j .$$

Agent $i$ receives a payment $p^i$ and has utility $p^i - \sum_{j \in x^i} \tilde t_j$.

The corrected time vector of agent $i$ keeps agent $i$'s actual times on its own tasks and the other agents' declarations elsewhere: $\mathrm{corr}^i(x,d,\tilde t)_j = \tilde t_j$ for $j \in x^i$ and $d^l_j$ for $j \in x^l$, $l \ne i$. For a step $\delta > 0$, $\hat r = \delta\lceil r/\delta\rceil$ rounds $r$ up to a multiple of $\delta$, and $\hat g(x,\tau) = g(x,\hat\tau)$.

The rounding mechanism (Definition 34) allocates with an algorithm that exactly solves the problem with rounded declarations $\hat d$, and pays

$$p^i = \sum_{j\in x^i}\tilde t_j \;-\; \hat g\big(x, \mathrm{corr}^i(x, d, \tilde t)\big).$$

The first term, the compensation, uses exact actual times; the second, the bonus, uses rounded quantities.

A strategy is dominant if it is a best response to every declarations and executions of the others. The mechanism is truthful if every agent has a dominant strategy that declares its true type.

Formalization targets

Goal: Theorem 5.9 without running time

For every $\varepsilon > 0$, every $0 < \delta \le \varepsilon a$ and every allocation algorithm solving the rounded problem exactly, the rounding mechanism is truthful, and at every profile of dominant strategies from the class named in the proof (declarations with the true rounded values, executions whose rounded times equal the rounded true times),

$$g\big(x(d),\tilde t\big) \le (1+\varepsilon)\, g(y,t) \quad \text{for every allocation } y .$$

Milestones

1. The solution of the rounded problem is a $(1+\varepsilon)$-approximation: $g(x,\hat t) \le g(y,\hat t)\ \forall y$ implies $g(x,t) \le (1+\varepsilon) g(y,t)\ \forall y$.
2. After rounding, $\hat g$ is the make-span, $\hat g(x,\mathrm{corr}^*(x,d)) = g(x,\hat d)$, and each agent's utility equals its rounded bonus.
3. Every strategy with the true rounded values is dominant.
4. When all agents follow such strategies, the outcome is a $(1+\varepsilon)$-approximation.
5. Truth-telling with minimal execution is dominant; hence the mechanism is truthful.

Significance

The result shows that verification does more than make exact optimization truthful: it lets a polynomial-time approximation scheme be implemented in dominant strategies, provided the bonus is computed on the same rounded instance the algorithm optimizes. This contrasts with Theorem 5.6, where an arbitrary approximation algorithm inside Compensation-and-Bonus is not truthful, and with the factor-2 lower bound of the basic model. The principle it illustrates is that the payments must reward exactly the objective the algorithm optimizes.

The paper gives only a proof sketch. Formalizing it makes the argument's hypotheses explicit: which rounding step suffices, what the allocation algorithm must satisfy, and over which strategy profiles the approximation guarantee holds. No machine-checked version of this theorem or of the Compensation-and-Bonus argument is known to exist.

Difficulty

The sketch reduces the theorem to "arguments similar to those in 5.1", but the rounded setting departs from Theorem 5.1 in two ways. Rounding is many-to-one, so an agent's declaration and execution are pinned down only up to their rounded values, and the algorithm's optimality holds only for the rounded instance. Consequently the claim that the strategies with the true rounded values are the only dominant ones does not survive arbitrary tie-breaking: an agent that is always favoured on ties can overstate its rounded time by one step without ever losing, and two such lies at one profile can push the make-span above the $(1+\varepsilon)$ bound. The approximation guarantee therefore has to be stated for the strategy class the proof identifies, not derived from dominance alone. The remaining steps require exact bookkeeping of rounding across sums and of the corrected time vectors, which a proof sketch leaves implicit.

Formalization scope

• Agents are Fin n with [NeZero n], tasks Fin k; allocations are functions Fin k → Fin n; the make-span is a Finset.sup' over agents. Types and declarations satisfy a ≤ t i j ≤ b with 0 < a < b; actual times are only bounded below by the true times.
• roundUp δ r = δ * ⌈r / δ⌉. The statement holds for every $\delta \in (0,\varepsilon a]$, which covers the intended choice $\delta = \varepsilon a$; the paper leaves $\delta$ as "a function of $a$ and $\varepsilon$".
• The Horowitz–Sahni dynamic program is not formalized. The allocation algorithm is a parameter with the hypothesis that it solves the rounded problem exactly; ties are arbitrary, and the goal holds for every such algorithm. Running time ("polynomial time") is out of scope, and with it the role of the upper bound $b$, which is kept as part of the problem.
• An execution is a function of the decision (Definition 18). Dominance quantifies over all declarations in $[a,b]$ and all executions of the others.
• The payment uses the allocation $x(d)$ in the bonus. Definition 34 prints $x(\hat t)$; since the rounding algorithm rounds the declarations itself, $x(d)$ is the allocation actually computed. The hat on $\mathrm{corr}$ is absorbed by $\hat g$.
• The goal's approximation part is restricted to dominant profiles of the class named in the proof, because the unrestricted form (Definition 3, every dominant profile) is false for some tie-breaking rules; an explicit two-agent, one-task instance is recorded in the goal's Formalization Note.
• A formalization that measures the approximation with declared rather than actual times, lets the allocation read the true types, or states the approximation only at the truthful profile while claiming the general form, does not formalize this theorem.

Useful infrastructure: lemmas on Int.ceil rounding of finite sums and on Finset.sup' monotonicity, and a reusable model of mechanisms with verification. Proofs of the milestones in any order are welcome.

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• E. Horowitz, S. Sahni, Exact and Approximate Algorithms for Scheduling Nonidentical Processors, Journal of the ACM 23 (1976) 317–327. https://doi.org/10.1145/321941.321951

Motivation

Algorithmic mechanism design studies optimization problems whose inputs are held by self-interested agents: the algorithm must compute a good solution and, through payments, make it in each agent's interest to report its input honestly. Nisan and Ronen introduced the field with the problem of scheduling tasks on unrelated machines, where each machine is an agent that privately knows how long it needs for every task (Nisan–Ronen 2001).

The classical tool for truthfulness, the Vickrey–Groves–Clarke (VGC) family of mechanisms, requires the allocation to be exactly optimal. Exact optimization is often computationally out of reach: minimizing the make-span on unrelated machines is NP-hard, and even approximating it within a factor below 3/2 is NP-hard (Lenstra–Shmoys–Tardos 1990). A mechanism designer would therefore like to plug an approximation algorithm into a truthful mechanism and keep truthfulness. This mission formalizes a result showing that the simplest way of doing so fails in the model with verification, where the mechanism may pay after the tasks are performed and observes the actual execution times.

Timeline.

• 1999/2001: Nisan and Ronen define mechanisms with verification and the Compensation-and-Bonus mechanism, prove it strongly truthful when its allocation algorithm is optimal (their Theorem 5.1), and prove that replacing the optimal algorithm by a non-optimal approximation algorithm destroys truthfulness (Theorem 5.6, the goal here). They remark that a similar argument applies to VGC mechanisms.
• 2002: Lehmann, O'Callaghan and Shoham show the analogous failure for VGC payments with approximate allocation in combinatorial auctions (JACM 2002).
• 2007: Nisan and Ronen study which approximation algorithms can be made truthful within the VGC framework (JAIR 2007).

Setting

There are $n \ge 1$ agents and $k$ tasks. The type of agent $i$ is a vector $t^i = (t^i_1,\dots,t^i_k)$ of positive reals, $t^i_j$ being the minimum time agent $i$ needs for task $j$; a type vector is $t = (t^1,\dots,t^n)$. An allocation $x = (x^1,\dots,x^n)$ gives each task to one agent. The make-span is

$$g(x,t) = \max_i \sum_{j\in x^i} t^i_j,$$

and $x$ is optimal for $t$ if $g(x,t)\le g(y,t)$ for every allocation $y$.

In the model with verification, an agent's strategy has two parts: a declaration $d^i$ (any positive vector) and an execution plan that, for every allocation the mechanism may choose, fixes the actual time $\tilde t_j \ge t^i_j$ in which the agent performs each task $j$ it receives. An allocation algorithm $x(\cdot)$ maps the declarations to an allocation $x(d)$; the tasks are then executed, producing actual times $\tilde t$.

The Compensation-and-Bonus mechanism based on $x(\cdot)$ pays agent $i$

$$p^i(d,\tilde t) = \sum_{j\in x^i(d)} \tilde t_j \;-\; g\bigl(x(d), \operatorname{corr}^i(x(d),d,\tilde t)\bigr),$$

a compensation for the time actually spent plus a bonus equal to minus the make-span computed from agent $i$'s actual times on its own tasks and the other agents' declared times on theirs (the corrected time vector $\operatorname{corr}^i$). The agent's utility is its payment minus the time it spends. A strategy is dominant if it is at least as good as every alternative whatever the other agents declare and execute; the mechanism is truthful if every agent of every type has a dominant strategy that declares its true type.

Formalization targets

Goal: Theorem 5.6

Let $x(\cdot)$ be an allocation algorithm such that, for some real $c$,

$$g\bigl(x(t),t\bigr) \le c\, g(y,t)\quad\text{for every positive } t \text{ and every allocation } y,$$

and such that $g(y,t) < g(x(t),t)$ for some positive $t$ and some allocation $y$. Then the Compensation-and-Bonus mechanism based on $x(\cdot)$ is not truthful.

The ratio $c$ is arbitrary and existentially quantified: the theorem holds for every finite approximation ratio, so it is stated without a constant.

Milestones

• Claim 5.7. If the mechanism based on $x(\cdot)$ is truthful, $o$ is optimal for $t$ and $M$ is at least every entry of $t$, then replacing one agent's type by $t^i_j$ on $o^i$ and $M$ elsewhere gives a type vector $t'$ with $g(x(t'),t') \ge g(x(t),t)$.
• Corollary 5.8. Under the same assumptions, the type vector $s$ that makes this replacement for every agent satisfies $g(x(s),s) \ge g(x(t),t)$.
• Final step. $g(o,s) = g(o,t)$, $o$ is optimal for $s$, and every allocation $y\ne o$ has $g(y,s)\ge M$.

Significance

The result. Theorem 5.1 of the same paper shows that with an optimal algorithm the Compensation-and-Bonus mechanism is a strongly truthful implementation of make-span minimization. Theorem 5.6 shows that this guarantee is tied to exact optimization: it does not survive replacing the optimizer by any non-optimal approximation algorithm, whatever its ratio. It explains why the paper then turns to a restricted problem (bounded scheduling) and a mechanism designed around a specific rounding algorithm, and it is an early instance of the general tension between approximation and incentive compatibility.

Formalizing it. The result is proved in the paper; to the best of the platform's catalog it has not been formalized. The mission produces a machine-checked model of mechanisms with verification (declarations together with execution plans that may depend on the decision), the Compensation-and-Bonus payment rule for an arbitrary allocation algorithm, and Definition 19 truthfulness, together with a checked proof of the impossibility.

Difficulty

The argument is short on paper; the difficulty lies in the model. The paper's "$\infty$" is not a number, and a faithful statement must replace it by a finite value that is large enough to conflict with the approximation ratio yet keeps every type positive and entrywise above the true types; both requirements refer to data fixed earlier in the argument. The incentive step compares utilities in a mechanism where an agent's strategy is a declaration and an execution plan that may depend on the decision, and where the bonus mixes the agent's actual times with the other agents' declarations, so a naive reading in which only declarations matter (the direct-revelation model of §2) does not capture the claim. Finally, Corollary 5.8 concerns a type vector modified at every agent, while Claim 5.7 modifies one agent at a time, so the claim must be applicable at type vectors that are no longer the original one.

Formalization scope

• Agents are Fin n with [NeZero n], tasks Fin k, allocations are functions Fin k → Fin n, types and declarations are positive real vectors. Make-spans are Finset.sup' over the nonempty set of agents. With no agents no allocation algorithm meets the hypotheses, so requiring $n\ge 1$ loses nothing.
• An execution plan is a function of the allocation; feasibility is $\tilde t_j \ge t^i_j$ on the agent's own tasks. In the dominance quantifier the other agents' declarations are positive and their execution plans arbitrary; the agent's alternative declarations are positive and its alternative plans feasible for its true type.
• The allocation algorithm is an arbitrary function of the declarations; "approximation algorithm" is the hypothesis $\exists c$ above, "non-optimal" the hypothesis of one positive witness. The optimal allocation $\mathrm{opt}(t)$ in the milestones is any optimal allocation $o$, supplied as a parameter.
• The paper's $\infty$ is a real parameter $M$ with $M \ge t^l_j$ for all $l,j$; extended reals are not used.
• Claim 5.7 is stated for an arbitrary agent $i$, not only for agent 1, so that Corollary 5.8 can iterate it.
• Running time is not modelled; "algorithm" means function.
• Dropping the approximation hypothesis makes the statement false: an allocation rule that ignores the declarations is non-optimal, yet its Compensation-and-Bonus mechanism is truthful. Stating only "not strongly truthful", or proving the theorem for a fixed instance, would be a weaker claim.

Welcome contributions: proofs of the milestones and the goal, and reusable lemmas about the corrected time vector and the monotonicity of the make-span in the time vector.

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990) 259–271. https://doi.org/10.1007/BF01585745
• D. Lehmann, L. I. O'Callaghan, Y. Shoham, Truth revelation in approximately efficient combinatorial auctions, Journal of the ACM 49 (2002) 577–602. https://doi.org/10.1145/585265.585266
• N. Nisan, A. Ronen, Computationally Feasible VCG Mechanisms, Journal of Artificial Intelligence Research 29 (2007) 19–47. https://doi.org/10.1613/jair.2046
• E. Horowitz, S. Sahni, Exact and approximate algorithms for scheduling nonidentical processors, Journal of the ACM 23 (1976) 317–327. https://doi.org/10.1145/321941.321951