Motivation

A buyer and a seller negotiate over one indivisible good. Each knows the good's worth to themselves but not to the other side, so each shades their offer to exploit the other's uncertainty, and some mutually profitable trades fail. Chatterjee and Samuelson (Bargaining under Incomplete Information, Operations Research 31(5), 1983) modelled this as a one-shot game of simultaneous sealed offers and computed its equilibria in closed form for uniformly distributed values.

That closed-form equilibrium became the reference example of bilateral trade with two-sided private information. Myerson and Satterthwaite (J. Econ. Theory 29, 1983) proved that no mechanism can guarantee efficient trade in this setting and showed that, for uniform values, the equilibrium of the sealed-offer game with $k = 1/2$ attains the largest expected gains from trade of any incentive-compatible, individually rational mechanism. The later literature on the $k$-double auction (Satterthwaite and Williams, J. Econ. Theory 48, 1989; Leininger, Linhart and Radner, J. Econ. Theory 48, 1989) studies the same game and uses the linear equilibrium as its benchmark.

Setting

A seller has reservation price $v_s$ and a buyer has reservation price $v_b$, both in $[0, \bar v]$ with $\bar v > 0$. Each knows their own value. Each believes the other's value is uniformly distributed on $[0, \bar v]$: the distribution functions are $F_s(v) = F_b(v) = v/\bar v$ on $[0, \bar v]$. In Lean this belief is the measure unif v̄, Lebesgue measure conditioned on $[0, \bar v]$.

Under the Bargaining Rule, the seller asks $s$ and the buyer offers $b$ simultaneously. If $b \ge s$ the good is sold at $P = kb + (1-k)s$ for a fixed $k \in [0, 1]$; if $b < s$ there is no sale. On a sale the seller earns $P - v_s$ and the buyer $v_b - P$; otherwise both earn zero. The case $k = 1$ gives the buyer the right to make a take-it-or-leave-it offer, $k = 0$ gives it to the seller, and $k = 1/2$ splits the difference.

An offer strategy maps values to offers: $S$ for the seller, $B$ for the buyer. Against $S$, a buyer with value $v$ who offers $b$ earns in expectation

$$\pi_b(b, v) = \int \mathbf 1\{S(v_s) \le b\}\,\bigl(v - kb - (1-k)S(v_s)\bigr)\,d\,\mathrm{unif}_{\bar v}(v_s),$$

and against $B$ a seller with value $v$ asking $s$ earns $\pi_s(s, v) = \int \mathbf 1\{s \le B(v_b)\}\,(kB(v_b) + (1-k)s - v)\,d\,\mathrm{unif}_{\bar v}(v_b)$. These are buyerProfit and sellerProfit. The pair $(S, B)$ is an equilibrium (IsEquilibrium) if, for every value in $[0, \bar v]$, each player's prescribed offer maximises their expected profit over all real offers.

Formalization targets

Goal: Example 1(a)

Write $S_{\mathrm{lin}}(v) = \frac{v}{2-k} + \frac{1-k}{2}\bar v$ and $B_{\mathrm{lin}}(v) = \frac{v}{1+k} + \frac{k(1-k)}{2(1+k)}\bar v$. If $S$ and $B$ are measurable and

$$\begin{aligned} S(v_s) &= S_{\mathrm{lin}}(v_s) && \text{for } 0 \le v_s \le \tfrac{2-k}{2}\bar v, &\qquad S(v_s) &\ge S_{\mathrm{lin}}(v_s) && \text{for } \tfrac{2-k}{2}\bar v < v_s \le \bar v,\\ B(v_b) &\le B_{\mathrm{lin}}(v_b) && \text{for } 0 \le v_b < \tfrac{1-k}{2}\bar v, &\qquad B(v_b) &= B_{\mathrm{lin}}(v_b) && \text{for } \tfrac{1-k}{2}\bar v \le v_b \le \bar v, \end{aligned}$$

then $(S, B)$ is an equilibrium. The statement leaves the no-trade branches free, as the paper does: a seller whose value exceeds every serious bid may ask anything at least $S_{\mathrm{lin}}$, and a buyer whose value is below every serious ask may bid anything at most $B_{\mathrm{lin}}$.

Milestones

1. The linear rules solve (3a)–(3b). The paper's own justification of Example 1(a): with $F_b = F_s = v/\bar v$ and densities $1/\bar v$, the pair $(S_{\mathrm{lin}}, B_{\mathrm{lin}})$ satisfies the linked differential equations of the paper's Theorem 2, $kF_b(y)S'(y) + f_b(y)S(y) = B^{-1}(S(y))f_b(y)$ and $(1-k)(1 - F_s(x))B'(x) - f_s(x)B(x) = -S^{-1}(B(x))f_s(x)$.
2. Seller half. For every seller value $v \in [0, \bar v]$ and every real ask $s$, $\pi_s(s, v) \le \pi_s(S(v), v)$.
3. Buyer half. For every buyer value $v \in [0, \bar v]$ and every real offer $b$, $\pi_b(b, v) \le \pi_b(B(v), v)$.

The goal is the conjunction of milestones 2 and 3, by definition of equilibrium. Milestone 1 is the step the paper actually writes down; it records the necessary first-order conditions and does not by itself give the global best-response property.

Significance

The result. Example 1(a) is the explicit equilibrium from which the paper derives the probability of trade, $(-k^2 + k + 2)/8$, and each party's ex ante profit as a function of $k$ (Example 1(b)–(c)). It is the equilibrium shown by Myerson and Satterthwaite to be second-best efficient at $k = 1/2$, and it is the standard test case against which other double-auction equilibria and mechanisms for bilateral trade are compared.

Formalizing it. The result is proved in the literature but, to our knowledge, has not been machine-checked. The paper itself only observes that the linear branches satisfy the first-order conditions; the global statement (no deviation to any real offer is profitable, including deviations that reach the other side's no-trade types) is left to the reader. A formal proof closes that gap and yields reusable facts about expected profits under uniform beliefs. The two companion missions of this series formalize the paper's Theorem 2 (the linked differential equations in general) and Example 1(b)–(c) (trade probability and expected profits).

Difficulty

First-order conditions do not suffice. A seller can ask below the lowest serious ask $\frac{1-k}{2}\bar v$ and trade with buyers on the free lower branch, whose bids are only bounded above; a buyer can bid above $\frac{2-k}{2}\bar v$ and meet sellers on the free upper branch, whose asks are only bounded below. The best-response inequality must hold for every such deviation and for every admissible choice of the free branches, so it cannot be read off from the linear strategies alone. The expected profit is a piecewise function of the offer, with the pieces determined by where the offer meets the opponent's linear branch and the free branches, and the inequality must be shown on each piece and at the boundaries, uniformly in $k \in [0, 1]$ including the endpoints $k = 0$ and $k = 1$, where one of the free ranges is empty.

Formalization scope

Values and offers are real numbers; strategies are functions $\mathbb R \to \mathbb R$, and their values outside $[0, \bar v]$ are irrelevant because the beliefs give that set measure zero. Beliefs are the probability measure unif v̄ = volume[|Icc 0 v̄]; expected profits are Bochner integrals against it, written over the opponent's value rather than against an offer density. The value intervals are closed; ties $b = s$ trade; deviations range over all of $\mathbb R$; $k$ ranges over the closed interval $[0, 1]$.

The strategies $S$ and $B$ are assumed measurable. Without this a deviation's expected profit could be the junk value $0$ of a non-integrable Bochner integral; with it, all integrands are bounded on the trade event. The inline coefficient $(k(1-k)/2(1+k))\bar v$ of the page is read as $\frac{k(1-k)}{2(1+k)}\bar v$, the reading under which the buyer's lowest serious bid equals the seller's lowest serious ask, as in the paper's Figure 1.

The claim is the sufficiency direction only; the paper states that other equilibria exist, and a statement that every equilibrium has the linear form would be false. The canonical linear pair satisfies all hypotheses, so the goal is not vacuous.

Useful infrastructure includes integrals of piecewise-affine functions against the uniform measure on an interval and the distribution function of volume[|Icc 0 v̄]. Contributions welcome: proofs of the milestones, and lemmas computing $\pi_s$ and $\pi_b$ in closed form on each piece.

Selected references

• K. Chatterjee and W. Samuelson, Bargaining under Incomplete Information, Operations Research 31(5):835–851, 1983. https://doi.org/10.1287/opre.31.5.835
• R. B. Myerson and M. A. Satterthwaite, Efficient Mechanisms for Bilateral Trading, Journal of Economic Theory 29(2):265–281, 1983. https://doi.org/10.1016/0022-0531(83)90048-0
• M. A. Satterthwaite and S. R. Williams, Bilateral Trade with the Sealed Bid k-Double Auction: Existence and Efficiency, Journal of Economic Theory 48(1):107–133, 1989. https://doi.org/10.1016/0022-0531(89)90120-8
• W. Leininger, P. B. Linhart and R. Radner, Equilibria of the Sealed-Bid Mechanism for Bargaining with Incomplete Information, Journal of Economic Theory 48(1):63–106, 1989. https://doi.org/10.1016/0022-0531(89)90121-X

Motivation

Many US school districts assign children to public schools centrally. Each family ranks the schools. Each school ranks the children by priority, which is set by state or local law (siblings, walking distance, a lottery). A procedure then turns these rankings into an assignment. Abdulkadiroğlu and Sönmez (Columbia Economics Discussion Paper 0203-18, 2003; published in the American Economic Review 93(3), 2003) cast this as a mechanism design problem. They showed that the mechanisms then in use in Boston, Columbus and Minneapolis gave families reasons to misreport their preferences. They proposed two alternatives: the student-optimal stable mechanism of Gale and Shapley, and a school-choice version of Shapley and Scarf's top trading cycles (TTC) mechanism.

Many districts also operate under controlled choice: court-ordered or voluntary rules that keep the racial or ethnic composition of each school within bounds. In Minneapolis, for instance, a 100-seat school could admit at most 75 majority and at most 55 minority students (paper, Section III). Such rules are implemented as type-specific quotas. Section III.B of the paper modifies TTC to respect these quotas. It proves that the modified mechanism keeps both properties that recommend TTC: it wastes nothing beyond what the quotas force (constrained efficiency, Proposition 6), and truth-telling is a dominant strategy (strategy-proofness, Proposition 7). This mission formalizes those two results.

Setting

There is a finite set $I$ of students and a finite set $S$ of schools. School $s$ has a capacity $q_s$, and the total number of seats suffices: $|I|\le\sum_s q_s$. Each student $i$ has a strict preference over all schools, encoded as a ranking $P_i : S\to\{0,\dots,|S|-1\}$ with rank $0$ the favourite. Each school $s$ has a strict priority ranking over all students, with rank $0$ the highest priority. Each student belongs to exactly one type $\tau(i)$, and school $s$ has a type quota $q_s^t$ for each type $t$.

An assignment $\nu$ gives each student a school or nothing ($\varnothing$, worse than every school). It satisfies the controlled choice constraints if every school $s$ receives at most $q_s$ students, and at most $q_s^t$ students of each type $t$. An assignment $\mu$ is constrained efficient if no assignment satisfying the constraints makes every student weakly better off and some student strictly better off.

The top trading cycles mechanism with type-specific quotas, $\mathrm{TTC}^q$, runs in steps. Each school keeps a counter $c_s$ (initially $q_s$) and one type counter $c_s^t$ for each type (initially $q_s^t$). A school is removed when $c_s$ reaches zero. At each step:

• every remaining student points to her favourite remaining school with room for her type, that is, with $c_s>0$ and $c_s^{\tau(i)}>0$;
• every remaining school points to its highest-priority remaining student, whatever her type;
• every student on a cycle of this graph is assigned the school she points to and leaves;
• that school's counter and its counter for her type each drop by one.

A direct mechanism is strategy-proof if no student can ever gain by misreporting her preference, whatever the others report.

Formalization targets

Goal: Proposition 7 (p. 23)

For every student $i$, every profile $P$ of announced preferences and every alternative report $Q_i$,

$$\mathrm{TTC}^q(Q_i,P_{-i})(i)=s' \implies \mathrm{TTC}^q(P)(i)=s \text{ with } P_i(s)\le P_i(s').$$

This holds for all capacities without shortage, all quotas, all types and all priorities. The priorities are fixed data, not reported.

Milestones

1. Section III.B, Step 1 (p. 22). At every step there is at least one cycle, after the convention below has removed the students who cannot point.
2. The Lemma (Appendix, pp. 28–29; declared valid for the modified mechanism on p. 30). Fix the other students' reports, and suppose student $i$ is still present at the beginning of a step under two different reports of hers. Then the two runs have the same remaining students and the same counters at that point.
3. Proposition 6 (p. 23). $\mathrm{TTC}^q(P)$ satisfies the controlled choice constraints and is constrained efficient with respect to $P$.

Significance

Strategy-proofness is what lets a district publish a simple instruction: rank the schools in your true order. A strategy-proof mechanism does not reward families who can afford to gather information and game the system. Proposition 7 shows that this guarantee survives the addition of flexible diversity quotas, which many districts are legally bound to impose. Proposition 6 shows that the quotas cost nothing beyond the losses they themselves cause. Both results were proved in 2003 by pen and paper. The published proof of Proposition 7 is a short adaptation of the proof of Proposition 4 (strategy-proofness of plain TTC). It rests on a lemma about how the algorithm's intermediate states depend on one student's report.

To our knowledge neither result has a machine-checked proof. The related platform theorem AGT.ttc_strategyproof concerns the Shapley–Scarf housing market, where every agent owns one house and the mechanism selects the core. It does not cover capacities, priorities or quotas. A formal proof here would check the adaptation that the paper leaves to the reader, and would give a reusable formal model of cycle-clearing allocation algorithms with multiple counters.

Difficulty

The algorithm clears all cycles of a step at once, and a student's report changes the graph at every step she is present. The paper's argument compares two whole runs of the algorithm, under the true report and under a misreport, step by step. That comparison needs precise control of which parts of the state a single student's report can influence, and when. A local argument about one step does not suffice. The student's outcome can depend on cycles that form several steps after the two runs could first have diverged.

With quotas, the pointing graph also depends on the type counters. A school can be present but closed to one type, and a school points to its best remaining student even when it has no room for her type. The comparison must therefore track the type counters as well as the set of remaining schools. Efficiency cannot be read off step by step against unrestricted matchings either: every competing assignment must satisfy both the capacity and the quota constraints.

Formalization scope

Students, schools and types are finite types; no nonemptiness is assumed. Preferences and priorities are bijective rankings onto Fin, so strictness is built in. Rank $0$ is the favourite or the highest priority. The no-shortage condition $|I|\le\sum_s q_s$ appears in every theorem, as the standing assumption of Section I. No relation between $q_s$ and $q_s^t$ is imposed, which generalises the paper.

The algorithm is a concrete, total definition: a state with remaining students, counters, type counters and partial assignments, a step map that clears all cycles simultaneously, and $|I|$ iterations. run … t is the state at the beginning of the paper's Step $t+1$.

The paper's step is undefined when a remaining student has no remaining school with room for her type. She cannot point, and the promised cycle may not exist. The formalization adopts one convention: at the beginning of each step, such a stuck student is removed unassigned, and her outcome is $\varnothing$, ranked below every school. Counters only decrease, so a stuck student stays stuck. Whenever nobody gets stuck, the algorithm is exactly the paper's, and when every quota is at least the capacity it is plain TTC. The goal and Proposition 6 are stated for assignments that may leave students unassigned. When everyone is assigned, they coincide with the paper's statements over matchings.

The formalization does not add a hypothesis that the run never gets stuck. Such a hypothesis would restrict the algorithm's own behaviour and could make the theorems vacuous. Nor may strategy-proofness be weakened to comparisons at the truthful profile only: the others' reports and the misreport are arbitrary.

Contributions welcome: invariants of the step map (counters bounded by the initial values, assigned students leave for good), the cycle-existence lemma for functional graphs on finite sets, and the comparison lemma. These pieces are shared with the plain-TTC mission of this series.

Selected references

• Atila Abdulkadiroğlu and Tayfun Sönmez, School Choice: A Mechanism Design Approach, Columbia University Department of Economics Discussion Paper No. 0203-18, 2003. https://doi.org/10.7916/D8057T27
• Atila Abdulkadiroğlu and Tayfun Sönmez, School Choice: A Mechanism Design Approach, American Economic Review 93(3), 729–747, 2003. https://doi.org/10.1257/000282803322157061
• Lloyd Shapley and Herbert Scarf, On Cores and Indivisibility, Journal of Mathematical Economics 1(1), 23–37, 1974. https://doi.org/10.1016/0304-4068(74)90033-0

Motivation

Public school districts in many US cities let families rank schools and then assign seats by a centralized procedure. Each school has a limited number of seats, and state or local law gives some students priority at some schools, for example for a sibling already enrolled or for living within walking distance. Abdulkadiroğlu and Sönmez (Columbia Economics Discussion Paper 0203-18, 2003; published in the American Economic Review 93(3), 2003) framed this as a mechanism design problem and showed that the mechanism then used in Boston rewards families who misreport their preferences. They proposed two replacements with written proofs of their properties. This mission covers the second one, the top trading cycles mechanism, and its two properties: every outcome is Pareto efficient, and no student can gain by misreporting.

The paper drew on earlier results for simpler allocation problems:

• 1974: Shapley and Scarf introduce housing markets and Gale's top trading cycles algorithm, in which each agent owns one house.
• 1977: Roth and Postlewaite show the algorithm finds the unique core allocation of a housing market.
• 1982: Roth proves the core mechanism for housing markets is strategy-proof.
• 1999: Abdulkadiroğlu and Sönmez adapt the algorithm to house allocation with existing tenants and prove strategy-proofness.
• 2000: Pápai introduces hierarchical exchange rules, a wider class that includes these mechanisms.
• 2003: the paper formalized here extends the algorithm to schools with capacities and school-specific priorities (Propositions 3 and 4).

Setting

A school choice problem consists of a finite set $I$ of students, a finite set $S$ of schools, a capacity $q_s \in \mathbb N$ for each school, a strict preference $P_i$ of each student over all schools, and a strict priority ordering $\succ_s$ of each school over all students. The standing assumption is that there is no shortage of seats:

$$|I| \le \sum_{s\in S} q_s .$$

Preferences are rankings: $P_i(s)\in\{0,\dots,|S|-1\}$ is the rank of $s$ for student $i$, with rank $0$ the favourite. Priorities are rankings of students in the same way, with rank $0$ the highest priority. A matching is a map $\mu : I\to S$ with $\#\{i:\mu(i)=s\}\le q_s$ for every school $s$. A matching $\mu$ is Pareto efficient if no other matching $\nu$ gives every student a weakly better school ($P_i(\nu(i))\le P_i(\mu(i))$) and some student a strictly better one.

A direct mechanism maps the reported preference profile, together with the fixed priorities and capacities, to a matching. It is strategy-proof if no student can ever obtain a school she strictly prefers by changing her own report while the others keep theirs.

The top trading cycles algorithm keeps a counter $c_s$ of free seats at each school, starting at $q_s$. A school is remaining while $c_s>0$. At each step every remaining student points to her favourite remaining school, and every remaining school points to the remaining student with the highest priority for it. A cycle is a list $(s_1,i_1,\dots,s_k,i_k)$ of distinct schools and students in which $s_1$ points to $i_1$, $i_1$ points to $s_2$, and so on, and $i_k$ points to $s_1$. Every student on a cycle is assigned the school she points to and is removed. Each school on a cycle loses one seat. All cycles present at a step are cleared at that same step. The top trading cycles mechanism $\mathrm{TTC}(q,\succ,P)$ returns the resulting assignment.

Formalization targets

Goal: Proposition 4 (strategy-proofness)

For all capacities with no shortage, all priorities, every profile $P$, every student $i$ and every alternative report $Q_i$, student $i$ is assigned schools $s = \mathrm{TTC}(q,\succ,P)(i)$ and $s' = \mathrm{TTC}(q,\succ,(Q_i,P_{-i}))(i)$, and

$$P_i(s) \le P_i(s') .$$

Milestones

1. At every step at which some student remains, there is a cycle (Section II.B, p. 15).
2. After $|I|$ steps no student remains, and the outcome is a matching (Section II.B, p. 16).
3. Lemma (Appendix, pp. 28–29): if student $i$ is still remaining at the beginning of a step under two different reports of her own, the remaining students and the remaining schools at that point are the same under both reports.
4. Proposition 3 (p. 17): the outcome is a Pareto efficient matching with respect to the reported profile.
5. When all schools share one priority ordering $\pi$, the mechanism equals the serial dictatorship induced by $\pi$ (Section II.B, p. 16).

Significance

Strategy-proofness means truthful reporting is a dominant strategy for every student. Families need no information about other families' reports. Under the Boston mechanism, ranking a popular school first can cost a student her priority at her second choice. Proposition 3 separates the top trading cycles mechanism from the Gale–Shapley student-optimal stable mechanism, which is also strategy-proof but can select Pareto dominated matchings.

The results are proved in the paper, in short prose arguments in its Appendix. To the best of our knowledge they have no machine-checked proof. The platform already has the housing-market version, AGT.ttc_strategyproof, but that statement covers one house per agent with the mechanism characterised as the core. Capacities, school priorities and the step-by-step algorithm are absent from it. This mission produces a checked account of the algorithm with capacities and counters, together with its termination and invariance properties.

Difficulty

The paper's argument moves from the step at which student $i$ leaves under one report to the step at which she leaves under another. It relies on the claim that the cycles formed before either step are unaffected by $i$'s report. Informally, $i$ is not on a cycle yet, so what she points to does not matter. Formally, "the same cycles form" requires comparing two runs of a simultaneous-clearing procedure step by step. At each step one has to show that the set of cycles, and hence the counters and the remaining schools, agree, even though $i$ points to different schools in the two runs. Reasoning about a single cycle at a time does not work, because the algorithm clears all cycles of a step at once. Termination is also not immediate: without the no-shortage condition the algorithm can leave students unassigned. Seats are counted with multiplicity, so a school can stay in the market for several steps.

Formalization scope

Everything lives in the namespace SchoolChoice.TTC. Students and schools are arbitrary finite types with decidable equality; the set of students may be empty. Capacities are q : S → ℕ, and a school of capacity zero is never remaining. A preference is a bijection S ≃ Fin (card S) and a priority is a bijection I ≃ Fin (card I), in both cases with rank 0 the best. Strictness and completeness of both therefore hold by construction, and every school is acceptable. A state of the algorithm consists of the remaining students, the counters and the assignments made so far. run q pri P t is the state after t completed steps, which is the beginning of the paper's Step t + 1. The mechanism ttc q pri P : I → Option S reads off the assignment after card I steps. Every theorem assumes card I ≤ ∑ s, q s.

The algorithm is a concrete, deterministic definition that clears all cycles at every step. The mechanism is not defined as "some Pareto efficient matching" or characterised by properties, since that would make Proposition 3 trivial. The goal asserts that both outcomes exist, so an unassigned outcome cannot satisfy it vacuously. The misreport, the other students' reports and the priorities are all universally quantified.

A complete development needs termination of the algorithm, a combinatorial account of the pointing graph (cycles in a finite functional graph), and the step-by-step invariance argument of the Lemma. The last two are reusable for the type-specific quota variant and for other trading-cycle mechanisms. Contributions of intermediate lemmas are welcome: counter invariants such as "the sum of the counters is at least the number of remaining students", monotonicity of the remaining sets, and the fact that a student on a cycle receives her favourite remaining school.

Selected references

• Atila Abdulkadiroğlu and Tayfun Sönmez, School Choice: A Mechanism Design Approach, Columbia University Department of Economics Discussion Paper No. 0203-18, 2003. https://doi.org/10.7916/D8057T27
• Atila Abdulkadiroğlu and Tayfun Sönmez, School Choice: A Mechanism Design Approach, American Economic Review 93(3), 729–747, 2003. https://doi.org/10.1257/000282803322157061
• Lloyd Shapley and Herbert Scarf, On Cores and Indivisibility, Journal of Mathematical Economics 1(1), 23–37, 1974. https://doi.org/10.1016/0304-4068(74)90033-0
• Alvin E. Roth and Andrew Postlewaite, Weak versus Strong Domination in a Market with Indivisible Goods, Journal of Mathematical Economics 4(2), 131–137, 1977. https://doi.org/10.1016/0304-4068(77)90004-0
• Alvin E. Roth, Incentive Compatibility in a Market with Indivisible Goods, Economics Letters 9(2), 127–132, 1982. https://doi.org/10.1016/0165-1765(82)90003-9
• Atila Abdulkadiroğlu and Tayfun Sönmez, House Allocation with Existing Tenants, Journal of Economic Theory 88(2), 233–260, 1999. https://doi.org/10.1006/jeth.1999.2553
• Szilvia Pápai, Strategyproof Assignment by Hierarchical Exchange, Econometrica 68(6), 1403–1433, 2000. https://doi.org/10.1111/1468-0262.00166

Motivation

An organization whose members hold private information faces two problems at once. The first is the team problem of Marschak and Radner: choose the rules by which members observe, communicate and decide so as to maximize the expected payoff of the organization as a whole (Marschak–Radner 1972). The second is the incentive problem: a member who is paid by their own results has no reason to follow those rules, and in particular no reason to report truthfully what they have observed. Theodore Groves' Incentives in Teams (Econometrica 41(4), 1973) connected the two. For a decentralized firm in which subunits report to a head, it exhibits compensation rules that make the team-optimal behaviour, truthful messages included, each subunit manager's unique best reply.

The construction is the origin of what is now called the Groves scheme, and with Vickrey's second-price auction (Vickrey 1961) and Clarke's pivot rule (Clarke 1971) it forms the Vickrey–Clarke–Groves (VCG) family of mechanisms.

Timeline:

• 1961, Vickrey: second-price auctions make truthful bidding a dominant strategy for a single object.
• 1971, Clarke: pivot payments for public-good decisions with deterministic valuations.
• 1972, Marschak–Radner: the economic theory of teams, with information and decision structures but a common payoff.
• 1973, Groves: compensation $C_i^{II}$ based on the head's conditional expectation of the other units' payoffs; Theorem 1 proves optimality in a conglomerate with independent component states and one round of communication.
• 1977, Green–Laffont: in the complete-information setting, Groves-type payments are the only ones that make truth-telling dominant (Econometrica 45(2)).
• 1979, d'Aspremont–Gérard-Varet: Bayesian incentive-compatible mechanisms with expected externality payments (J. Public Econ. 11(1)).

The conglomerate model

The organization consists of a head (component $0$) and finitely many subunits $i = 1, \dots, n$. Each component $k$ has its own random component state $s_k \in S_k$, and the components are independent: the state of the environment $s = (s_0, s_1, \dots, s_n)$ is distributed according to the product law $P(s) = P_0(s_0) \prod_{i} P_i(s_i)$ (Condition S.2).

Every member plays a strategy $\beta_k = (\zeta_k, \gamma_k, \delta_k)$ made of an observation strategy $\zeta_k$ on its own state, a message strategy $\gamma_k$ and a decision strategy $\delta_k$ (Condition S.3). Communication runs only between the head and each subunit, in one exchange: the head observes $\zeta_0(s_0)$ and sends $\gamma_0^i(\zeta_0(s_0))$ to subunit $i$; the subunit, with information $y_i(s) = [\zeta_i(s_i), \gamma_0^i(\zeta_0(s_0))]$, sends back $\gamma_i(y_i(s))$; the head's information is $y_0(s) = [\zeta_0(s_0), \{\gamma_i(y_i(s))\}_{i}]$ (3.1). Decisions are $\delta_i(y_i(s))$ and $\delta_0(y_0(s))$.

The organization payoff is a sum of components (Condition S.4),

$$\omega_0(\beta, s) = \sum_{i=1}^n v_i[\delta_i(y_i(s)), \delta_0(y_0(s)); s_i] + v_0[\delta_0(y_0(s)), s_0],$$

and $\bar\omega_0(\beta) = E[\omega_0(\beta, s)]$. Each $v_i$ accrues directly to subunit $i$ (Condition S.5). Strategy sets $B_0, B_1, \dots, B_n$ are given; $\beta/\beta_i$ denotes $\beta$ with subunit $i$'s strategy replaced by $\beta_i$. Two strategies $\beta_i', \beta_i''$ are equivalent if $\bar\omega_0(\beta/\beta_i') = \bar\omega_0(\beta/\beta_i'')$ for every $\beta \in B$.

Assumption A requires a $\beta^* \in B$ maximizing $\bar\omega_0$ over $B$ such that, for each subunit, $\bar\omega_0(\beta^*) > \bar\omega_0(\beta^*/\beta_i)$ whenever $\beta_i \in B_i$ is not equivalent to $\beta_i^*$.

An incentive structure $W = \{\omega_i\}$ pays subunit $i$ the amount $\omega_i(\beta, s)$. The class $\mathscr{J}$ (3.2) consists of those of the form $\omega_i = v_i[\dots] + C_i(y_0(s))$: own payoff plus a compensation computed from the head's information only. $W$ is optimal (2.6) if $\beta_i^*$ maximizes $\bar\omega_i(\beta^*/\beta_i)$ over $B_i$, uniquely up to equivalence.

Formalization targets

Goal: Theorem 1 (p. 625)

With $C_i^{II}(y_0) = \sum_{j \ne i} E\big[v_j[\delta_j^*(y_j^*(s)), \delta_0^*(y_0^*(s)); s_j] \,\big|\, y_0^*(s) = y_0\big] - A_i$, the sum running over all components $j \in \{0, \dots, n\}$ other than $i$ and the expectation taken under $\beta^*$ (3.3), the structure $\omega_i^{II} = v_i[\dots] + C_i^{II}(y_0(s))$ lies in $\mathscr{J}$ and satisfies, for every subunit $i$ and every $\beta_i \in B_i$,

$$\bar\omega_i^{II}(\beta^*/\beta_i) \le \bar\omega_i^{II}(\beta^*), \qquad \text{with strict inequality if } \beta_i \not\equiv \beta_i^*.$$

It holds for every $\beta^*$ satisfying Assumption A, all strategy sets and all constants $A_i$.

Milestones

1. The Appendix Lemma: the sets of states consistent with the head's information under $\beta^*/\beta_i$ and under $\beta^*$ have the same projections onto every component other than $i$.
2. The right-hand side of (A.2): the head's conditional expectation factorizes over the independent components.
3. (A.2) for a subunit $j \ne i$, and 4. (A.2) for the head's component $j = 0$: the expected payoff of component $j$ under $\beta^*/\beta_i$ equals the expected value of its conditional expectation.
4. (A.1): $\bar\omega_i^{II}(\beta^*/\beta_i) + A_i = \bar\omega_0(\beta^*/\beta_i)$ for all $\beta_i \in B_i$.

Significance

Theorem 1 shows that a head who knows only the messages it receives can nonetheless align every subunit's interest with the organization's, without monitoring decisions or observations. It is an early statement that expected-externality payments make truthful communication an equilibrium of a decentralized organization, and the Bayesian, team-theoretic counterpart of the dominant-strategy results of Vickrey and Clarke. Its structure (own payoff plus a transfer depending only on the others' reported information) is the template later characterized by Green and Laffont and generalized by d'Aspremont and Gérard-Varet.

Theorem 1 is proved in the paper; nothing here is open mathematically. What the mission adds is a machine-checked version with every modelling choice explicit: how information is generated by the message protocol, what the conditional expectation in (3.3) means on events of probability zero, and which equivalence "uniquely" refers to. No machine-checked proof of Theorem 1 is known to the platform. The platform's AGT.vcg_incentive_compatible treats the complete-information, direct-revelation analogue (deterministic valuations, dominant strategies), a different model with a different conclusion.

Difficulty

The tempting argument conditions on the head's information $y_0^*(s) = y_0$ under $\beta^*$ and compares it with the head's information under a deviation. That comparison fails when a deviating subunit sends a message that $\gamma_i^*$ never sends: the conditioning event then has probability zero under $\beta^*$, and the conditional expectation of (3.3) is not determined by the joint law. A second obstacle is that the head's information under a deviation differs from the information under $\beta^*$ in every coordinate the deviation touches, while the compensation is computed as if $\beta^*$ were played; the statement to be proved compares expectations taken under two different joint strategies, and the one-exchange protocol makes the head's messages, and hence every subunit's information, depend on the head's own state. Treating these dependencies loosely either produces a circular definition of the information functions (as (3.1) is printed) or a statement that fails on events of probability zero.

Formalization scope

• Every component state space $S_k$ is a finite type with weights that are nonnegative and sum to one; the joint law is the product of these weights and expectations are finite sums. The paper allows general probability spaces; the finite case covers the whole argument and gives conditional expectations at a point an elementary meaning.
• Subunits form a finite index type; the head is a separate component with its own observation, message and decision types. Observation, message and decision spaces are fixed types per component.
• Information (3.1) follows the single exchange of messages the paper describes in §4.A (p. 627): the head's message to subunit $i$ is a function of the head's observation. As printed, (3.1) is circular; this protocol is the paper's own resolution.
• $C_i^{II}$ is used in factorized form: the head's term conditions only the head's state on the head's observation, and subunit $j$'s term conditions only $s_j$ on the message $j$ sent. A separate milestone states that this equals the literal conditional expectation of (3.3) whenever the conditioning event has positive probability. The literal elementary quotient takes the value $0$ on null events, and with it Theorem 1 is false (one subunit that can send an unused message suffices); the factorized form is what the Appendix computes. The sum in (3.3) includes the head's component $v_0$.
• Equivalence of strategies is footnote 5's, over all $\beta \in B$; optimality includes the strict inequality for non-equivalent deviations. A formalization that replaces equivalence by equality of strategies, fixes $B_i = \{\beta_i^*\}$, drops the strict inequality, or assumes (A.1) as a hypothesis is not this theorem.
• The Lemma carries the added hypothesis that the set $B(s)$ is nonempty; the paper's proof presumes it and the statement is false without it.

Contributions welcome: proofs of the milestones, and reusable finite-probability facts (conditioning on product events, iterated expectation over a coordinate) stated for product weights.

Selected references

• T. Groves, Incentives in Teams, Econometrica 41(4):617–631, 1973. https://doi.org/10.2307/1914085
• J. Marschak and R. Radner, Economic Theory of Teams, Yale University Press, 1972.
• W. 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
• E. H. Clarke, Multipart Pricing of Public Goods, Public Choice 11:17–33, 1971. https://doi.org/10.1007/BF01726210
• J. Green and J.-J. Laffont, Characterization of Satisfactory Mechanisms for the Revelation of Preferences for Public Goods, Econometrica 45(2):427–438, 1977. https://doi.org/10.2307/1911219
• C. d'Aspremont and L.-A. Gérard-Varet, Incentives and Incomplete Information, Journal of Public Economics 11(1):25–45, 1979. https://doi.org/10.1016/0047-2727(79)90043-4

When is the auctioneer's revenue acceptable?

The Vickrey-Clarke-Groves auction is the textbook mechanism for selling several objects at once: bidders report valuations for bundles, the auctioneer computes the welfare-maximizing allocation, and each winner pays the externality it imposes on the others. Truthful bidding is a dominant strategy and the outcome is efficient. Yet Ausubel and Milgrom (2006) catalogued its practical defects: revenue can be zero when the objects are valuable, revenue can fall when bidders or bids are added, losing bidders can profit by colluding, and a bidder can profit from false identities. Chapter 15 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) reproduces those examples and then gives the cooperative-game answer to when they cannot occur: the VCG payoff vector should lie in the core, the set of outcomes no coalition of auctioneer and bidders can improve upon, and it does so for every set of participants exactly when the coalitional value function is bidder-submodular. This mission formalizes that characterization, Theorem 15.3, together with the lemma and theorem leading to it.

Setting

Players are the auctioneer $0$ and bidders $1, \dots, n$. A coalitional value function $V$ assigns to each coalition $T$ the value it can create by trading among themselves: $0$ if the auctioneer, who owns the objects, is not in $T$, and otherwise the optimal value of the auctioneer's allocation problem among the bidders of $T$, each bidder receiving at most one bundle and bundles disjoint (capValue). Two properties of $V$ are all the theory uses: coalitions without the auctioneer are worthless, and adding players never lowers the value (IsCoalitionalValue).

A payoff vector $\pi$ gives each player a payoff. It lies in the core of the game on a coalition $S \ni 0$ (InCore V S π) if the payoffs of $S$ sum to $V(S)$ and no sub-coalition $T \subseteq S$ is paid less than $V(T)$. The VCG payoff vector $\bar\pi(S)$ (vcgPayoff) pays each bidder $k$ its marginal contribution $V(S) - V(S \setminus k)$, which is its valuation minus its VCG payment, and the auctioneer the remainder. A core vector is bidder dominant (BidderDominant) if every bidder weakly prefers it to every other core vector. $V$ is bidder-submodular (BidderSubmodular) if each bidder's marginal contribution weakly decreases as the coalition grows.

Formalization targets

Goal: Theorem 15.3

For a coalitional value function $V$, the following are equivalent: (i) $V$ is bidder-submodular; (ii) for every coalition $S \ni 0$ the core equals $\Pi_S = \{\pi : \sum_{k \in S}\pi_k = V(S),\ 0 \le \pi_k \le \bar\pi_k(S)\ \forall k \in S \setminus 0\}$; (iii) for every coalition $S \ni 0$, $\bar\pi(S)$ lies in the core of $S$. This is vcg_core_characterization.

Supporting targets

That the combinatorial auction's $V$ is a coalitional value function; Lemma 15.1, the core is nonempty and each bidder's VCG payoff is the largest it receives at any core point; Theorem 15.2, the VCG vector is the bidder-dominant core point when it is in the core, and otherwise no bidder-dominant point exists and the auctioneer's VCG payoff is below every core payoff.

The English auction of Sect. 15.2, presented as a primal-dual interpretation of a linear program, and the combinatorial allocation problem of Sect. 15.3 carry no numbered results and are not targets.

Significance

Theorem 15.3 is the criterion an auction designer can check before running a VCG auction: when the bidders' valuations make $V$ bidder-submodular (for instance when objects are substitutes), the VCG outcome is a competitive outcome, its revenue meets the core benchmark, and none of the defects of Sect. 15.4.2 can arise; when they do not, Theorem 15.2 says the auctioneer's revenue is strictly below every competitive outcome. The result underlies the ascending package auctions proposed as VCG alternatives and the procurement auctions used in supply chains, such as the combinatorial reverse auctions of the chapter's case study.

None of these results has a machine-checked proof. The book proves all three. The formal treatment of the core and of marginal-contribution vectors is reusable for the cooperative-game models of cost allocation in supply chains.

Difficulty

The theorems are combinatorial statements about a function on finite sets, and the difficulty is entirely in the bookkeeping of coalitions. Lemma 15.1 needs the explicit core vector of its proof to be verified against every sub-coalition, which splits into cases on whether the sub-coalition contains the auctioneer and the distinguished bidder. The implication (i) $\Rightarrow$ (ii) telescopes marginal contributions along a chain of coalitions between a sub-coalition and $S$, and the chain has to be built and its sum computed. The implication (iii) $\Rightarrow$ (i) is the delicate one: a failure of submodularity is a pair of nested coalitions, and the proof needs to extract from it a single-element step at which a bidder's marginal contribution increases, then show the two-bidder sub-coalition blocks the VCG vector. The obvious idea, that submodularity can be checked only on single-element extensions, is correct but must itself be proved.

Formalization scope

Coalitions are finite sets of Fin (n+1) and payoff vectors are functions on all players; the core and $\Pi_S$ constrain only the players of $S$, so vectors differing outside $S$ are interchangeable. The core's budget equation sums over all players of the coalition, including the auctioneer, which is what the book's proofs use although its displayed definition sums over the bidders. The theorems take $V$ as any function with the two properties, and the auction's $V$ is shown to have them; the VCG vector is defined by the formulas (15.23) and (15.24) rather than through the payment rule, whose equivalence is the book's derivation. Bidder-submodularity is stated for $S \subseteq S'$ rather than proper inclusion, which changes nothing.

The definition module is shared by all five items. The single-item English auction as a primal-dual algorithm and the condition on individual preferences (substitutes) that implies bidder-submodularity are natural extensions on the same definitions.

Selected references

• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 15. https://doi.org/10.1002/9781119584445
• L. M. Ausubel and P. Milgrom, The lovely but lonely Vickrey auction, in Combinatorial Auctions, MIT Press, 2006. https://doi.org/10.7551/mitpress/9780262033428.003.0002
• S. de Vries and R. V. Vohra, Combinatorial auctions: a survey, INFORMS Journal on Computing 15(3), 2003. https://doi.org/10.1287/ijoc.15.3.284.16077
• W. Vickrey, Counterspeculation, auctions, and competitive sealed tenders, Journal of Finance 16(1), 1961. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x

Algorithmic Game Theory III: Arrow and Gibbard–Satterthwaite

Motivation

Before a mechanism can pay anyone, it must decide something — and the impossibility theorems of social choice say that deciding honestly is already hard. Arrow's theorem (1951) showed that any method of aggregating individual rankings into a social ranking that respects unanimity and independence of irrelevant alternatives must be a dictatorship; Gibbard (1973) and Satterthwaite (1975) showed the voting analogue: any non-dictatorial voting rule onto three or more candidates can be strategically manipulated. These two results frame all of mechanism design — they are the reason Chapter 9 of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007), this mission's source, introduces money and quasilinear utilities immediately after proving them: without transfers, incentive compatibility is an impossibility, not a design constraint.

A timeline: Arrow proved the aggregation impossibility in his 1951 monograph Social Choice and Individual Values; Gibbard (1973) established the manipulability of non-dictatorial voting schemes via game forms, Satterthwaite (1975) independently via a direct argument; the derivation of Gibbard–Satterthwaite as a corollary of Arrow's theorem, which the book follows and this mission adopts as its attack path, is standard since the 1970s.

Setting

Fix a finite set $A$ of alternatives (candidates) and a finite set $\iota$ of voters. A preference is a strict total order on $A$; we write the relation as $r(a,b)$, read "$a$ is strictly preferred to $b$" (the book writes $b \prec a$). A preference profile assigns a preference to each voter. A social welfare function $F$ maps profiles to a social preference; a social choice function $f$ maps profiles to a single chosen alternative (Definition 9.1).

The properties at stake (Definitions 9.2, 9.4, 9.5, 9.7):

• $F$ satisfies unanimity if on every profile where all voters hold the identical preference $r$, the social preference is $r$.
• $F$ satisfies independence of irrelevant alternatives (IIA) if the social preference between $a$ and $b$ depends only on the voters' preferences between $a$ and $b$.
• Voter $i$ is a dictator in $F$ if the social preference always equals $i$'s; in $f$, if $f$ always elects $i$'s top alternative.
• $f$ is incentive compatible if no voter, by misreporting, can obtain an outcome they strictly prefer (under their true preference) to the truthful outcome; $f$ is monotone if whenever a single voter's change of vote moves the outcome from $a$ to $a' \ne a$, that voter ranked $a$ above $a'$ before and $a'$ above $a$ after.
• $f$ is onto if every alternative is elected on some profile.

Formalization targets

Goal (capstone) — Theorem 9.8, Gibbard–Satterthwaite

$$|A| \ge 3,\ f \text{ incentive compatible and onto } A \implies f \text{ is a dictatorship.}$$

Theorem 9.3 — Arrow

$$|A| \ge 3,\ F \text{ a social welfare function satisfying unanimity and IIA} \implies F \text{ is a dictatorship.}$$

Proposition 9.6 — incentive compatibility = monotonicity

$$f \text{ is incentive compatible} \iff f \text{ is monotone},$$

with no cardinality or finiteness assumptions: the two properties are quantifier-for-quantifier the same data viewed twice.

Significance

These are the two foundational impossibility theorems of social choice, and the pivot of the whole mechanism-design part of this series: the VCG mission that follows exists because Gibbard–Satterthwaite closes the door on non-trivial strategyproof choice without money. The chapter derives Gibbard–Satterthwaite from Arrow through the top-set extension (Definition 9.9, Lemmas 9.10–9.11), so a solver of the capstone gets Arrow as a stepping stone, not a detour.

Formalizing them produces the platform's first social-choice library: preference profiles as strict total orders, the aggregation vocabulary, and the impossibility pair. Arrow's theorem has been formalized before in other proof assistants (Nipkow's Isabelle formalization, 2009; a Mizar formalization by Wiedijk), which is evidence the statement shapes here are the standard ones — but no Lean 4/mathlib formalization exists, and none on this platform.

Difficulty

The proofs are short on paper and famously slippery in the details. Arrow's proof (the book gives Geanakoplos's pairwise-neutrality route) is a sequence of profile surgeries: each step swaps one voter's ranking of a pair and tracks the social outcome through IIA; the formal cost is constructing the intermediate profiles and proving they remain strict total orders — pure bookkeeping, but a lot of it. The hybrid-profile argument needs, over three or more alternatives, custom orders placing chosen pairs at chosen positions; building these on an abstract finite type is where most of the work lies. For the capstone, the book's route through the top-set extension $\prec^S$ (move $S$ to the top, Definition 9.9) requires proving the extension is again a strict total order (Lemma 9.10) and inherits unanimity, IIA, and non-dictatorship (Lemma 9.11); a solver may equally take any direct proof of Gibbard–Satterthwaite — the statement fixes no route. Proposition 9.6 is a genuine warm-up: unfolding both definitions and rearranging quantifiers.

Formalization scope

Preferences are relations A → A → Prop carrying IsStrictTotalOrder; r a b means "$a$ is strictly preferred to $b$", the reverse of the book's $\prec$ — every definition's docstring states this orientation. Aggregators are total functions on all relation-valued profiles; every property quantifies only over genuine preference profiles, so behavior on invalid inputs is irrelevant, and nothing can be smuggled through junk inputs. Unanimity is the book's identical-profile form (Definition 9.2), which together with IIA yields the pairwise form used in proofs. Both alternatives and voters are finite types; |A| ≥ 3 enters as 2 < Fintype.card A. Arrow's theorem carries Nonempty ι, matching the book's setting of $n \ge 1$ voters; it is not needed for truth — with zero voters the identical-profile unanimity is already unsatisfiable over three or more alternatives, so that case is vacuous either way. Gibbard–Satterthwaite deliberately omits it: with zero voters ontoness onto three alternatives is unsatisfiable, and the statement holds vacuously. Dictatorship for choice functions is Definition 9.7 exactly: whenever some alternative is the dictator's unique maximum, it is elected.

Selected references

• K. J. Arrow, Social Choice and Individual Values, Wiley, 1951 (2nd ed. 1963). Link
• A. Gibbard, Manipulation of voting schemes: a general result, Econometrica 41 (1973), 587–601. DOI
• M. A. Satterthwaite, Strategy-proofness and Arrow's conditions, Journal of Economic Theory 10 (1975), 187–217. DOI
• J. Geanakoplos, Three brief proofs of Arrow's impossibility theorem, Economic Theory 26 (2005), 211–215. DOI
• T. Nipkow, Social choice theory in HOL: Arrow and Gibbard–Satterthwaite, J. Automated Reasoning 43 (2009), 289–304. DOI
• N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Chapter 9, §9.2. DOI