Algorithmic Game Theory

Motivation

A market in which each trader owns one indivisible good has a basic coordination question: can all goods be reassigned so that no group of traders can withdraw its own goods and improve every member's outcome? Houses are the paper's running example. Monetary transfers and fractional houses are absent, so ordinary convex allocation arguments do not describe the setting. Shapley and Scarf use games without side payments to express what each coalition of owners can achieve, and identify a balance property of this game in their Section 4 theorem (Shapley and Scarf, 1974).

The paper states that a general balanced-game theorem gives a nonempty core once balance has been established. Its Section 4 contribution is the classification of this particular housing market game. The separate top-trading-cycles construction in Section 6 gives another route to a core allocation and is the subject of the second mission in this series (Shapley and Scarf, 1974).

Setting

Let $N$ be a nonempty finite set of traders. Trader $j$ brings one indivisible item $j$. Trader $i$'s ranking of item $j$ is represented by a real number $a_{ij}$. Only comparisons within one trader's row matter: $a_{ij}>a_{ik}$ means that $i$ prefers $j$ to $k$, while equality represents indifference. No strict-preference or positivity assumption is imposed on the preference matrix $A=(a_{ij})$.

A coalition $S\subseteq N$ can redistribute the items brought by its members. Its allocation matrix $P$ has $P_{ij}=1$ when trader $i$ receives item $j$, and zero otherwise. An $S$-allocation puts exactly one 1 in each column indexed by $S$ and has zeros in rows and columns outside $S$. An $S$-permutation is an $S$-allocation with row sums at most one, so every member of $S$ receives exactly one of the coalition's items. Rows index traders and columns index items.

For a proposed payoff vector $x\in\mathbb R^N$, define the acceptability matrix

$$b_{S|ij}(x)= \begin{cases} 1,& i\in S\text{ and }x_i\le a_{ij},\\ 0,&\text{otherwise}. \end{cases}$$

The coalition payoff set is

$$V(S)=\{x\in\mathbb R^N:\text{some }S\text{-permutation }P \text{ satisfies }P_{ij}\le b_{S|ij}(x)\text{ for all }i,j\}.$$

Thus a coalition can reach a payoff threshold if it can give each member an item that member values at least as highly. The comparison is weak, so ties count as acceptable. This is the characteristic function used in the paper's Section 4 (Shapley and Scarf, 1974, pp. 109–110 of the source printing).

A balanced family $T$ is a family of nonempty coalitions with nonnegative real weights $\delta_S$, zero outside $T$, such that every trader has total covering weight one:

$$\sum_{\substack{S\in T\\j\in S}}\delta_S=1 \quad(j\in N).$$

The weights may be zero even for a coalition listed in $T$. A balanced game is a game without side payments whose feasible payoff sets obey

$$\bigcap_{S\in T}V(S)\subseteq V(N)$$

for every balanced family $T$. This includes overlapping families, not merely partitions (Shapley and Scarf, 1974, pp. 108–109).

Formalization targets

The goal is the paper's Section 4 theorem:

$$\text{For every finite nonempty }N\text{ and every }A:N\times N\to\mathbb R,\quad V_A\text{ is a balanced game}.$$

It contains four requirements. For each nonempty $S$, $V_A(S)$ is closed; it is downward closed in the coordinates of $S$; and its payoff slice after removing the interiors of singleton payoff sets is bounded and nonempty. The fourth requirement is the balanced-family inclusion displayed above.

The milestones name the paper's intervening claims in their order: the three game conditions, the identity $B_N(x)=\sum_{S\in T}\delta_SB_S(x)$, the doubly stochastic character of a balanced mixture $D=\sum_{S\in T}\delta_SP_S$, and the existence of a grand-coalition permutation $P_N\le B_N(x)$ when $D\le B_N(x)$. The final milestone states the matrix existence claim made at the end of Section 4, without committing the theorem statement to a particular construction.

Significance

The result establishes that the finite housing market falls under the paper's general balance framework. In the paper, the cited theorem that balanced games have nonempty cores then yields a core existence conclusion for this market. That general existence theorem is external to the Section 4 proof and is not asserted by this mission's goal (Shapley and Scarf, 1974, pp. 109–110).

The formal development supplies reusable definitions of games without side payments and balanced families alongside the market-specific allocation and acceptability matrices. It also gives precise targets for the matrix claims used in the paper. The source result is proved in print; these Lean statements are proposed formalization targets and their proof bodies remain open. Nearby platform items about transferable-utility games, including the Bondareva–Shapley goal, use a real value for each coalition and do not define this paper's payoff-set game. They are not substituted for these objects.

Difficulty

The challenge is the passage from coalition-wise feasibility to feasibility for all traders together. A balancing family can overlap: choosing one feasible permutation for each coalition does not immediately give a single permutation of $N$. Their weighted mixture has fractional matrix entries. The condition $B_N(x)\ge D$ also has to survive the move from such a mixture to an actual zero-one permutation matrix. Without that last assertion, the balancing equations alone do not prove the inclusion $V(S)$ requires. Separately, the bounded nonempty payoff-slice condition must be checked for every nonempty coalition; merely proving closedness and downward closure would define a weaker class of games.

Formalization scope

Traders are an arbitrary finite nonempty Lean type, and payoffs live in $N\to\mathbb R$. The paper's $E^S$ is encoded as the coordinate subspace of vectors zero outside $S$; interiors are taken in the product topology on $N\to\mathbb R$. The boundedness and nonemptiness test applies to the intersection of that subspace with $V(S)$ after removing the singleton interiors. All conditions defining a game quantify over nonempty coalitions. The market formula is also defined at $S=\varnothing$, where it yields all of $\mathbb R^N$.

Allocation matrices are real zero-one matrices. An $S$-permutation retains the paper's column, support, and row conditions; it is not replaced by an unconstrained permutation of all traders. The inequality between matrices is entrywise. The acceptability matrix has a 1 exactly when $i\in S$ and $x_i\le a_{ij}$; its columns are not independently restricted to $S$. Balancing weights are nonnegative, may vanish inside the family, and cover every trader in $N$. These choices exclude the trivializations $V(N)=\mathbb R^N$, balance tested only on partitions, and coalitions using outsiders' items.

The definitions need finite-sum and matrix support from Mathlib, while the eventual proof can use Mathlib's doubly stochastic matrix and permutation-matrix library. Contributions that establish the stated game conditions or any of the four sourced matrix milestones are within scope. The paper's Section 8 counterexample and the optional superadditivity observation are outside this mission's attack path.

Selected references

• Lloyd S. Shapley and Herbert Scarf, On cores and indivisibility, Journal of Mathematical Economics 1 (1974), 23–37. DOI: 10.1016/0304-4068(74)90033-0. The supplied scan has printed folios 104–123; Section 4 is on folios 109–111.

Motivation

Planning a road improvement requires an estimate of how traffic will redistribute over the routes affected. Because speed falls as flow rises, sending every vehicle along the route that is quickest today changes which route is quickest. J. G. Wardrop posed the question in its simplest setting in 1952: a given flow $Q$ chooses among $D$ alternative routes between one origin and one destination, and the journey time on each route rises with the flow on it. He proposed two criteria for the resulting distribution. The first, equal journey times, became known as Wardrop's first principle or user equilibrium: "the journey times on all the routes actually used are equal, and less than those which would be experienced by a single vehicle on any unused route." It describes the state in which no driver can shorten their trip by switching routes, and it is the equilibrium notion behind traffic-assignment models and the theory of selfish routing.

Timeline:

• 1952. Wardrop states both criteria and, for parallel routes with journey times of the form (22), derives the closed-form equal-times split (23)–(24) (Wardrop 1952, p. 345).
• 1956. Beckmann, McGuire and Winsten show that, on general networks with increasing link costs, the equal-times conditions are the optimality conditions of a convex program, which gives existence and uniqueness of link flows (Beckmann et al. 1956).
• 2014. Kelly and Yudovina give a textbook treatment of the network case (Kelly–Yudovina 2014, ch. 4); its existence theorem is on Prove2Me for total, continuous, increasing delay functions.

Setting

There are $D$ routes, $i = 1, \dots, D$. Route $i$ has two positive constants: $b_i$, its journey time when no additional traffic uses it, and $p_i$, the additional flow at which its speed would drop to zero. When an additional flow $x$ uses route $i$, its journey time is

$$t_i(x) = \frac{b_i}{1 - x/p_i}, \qquad 0 \le x < p_i. \tag{22}$$

This form comes from a linear speed/flow relation on each route. A feasible split of the total flow $Q$ is a vector $q = (q_1, \dots, q_D)$ with $0 \le q_i < p_i$ and $\sum_i q_i = Q$. A feasible split $q$ satisfies the equal-times criterion with common time $t$ when

• every used route ($q_i > 0$) has $t_i(q_i) = t$, and
• every unused route ($q_i = 0$) has $t \le b_i$, so a single vehicle could not do better than $t$ by moving to it.

Write $U(t) = \{ i : b_i < t \}$ for the routes whose empty-route time is below $t$. In Lean these objects are routeTime b p i x, IsFeasible p Q q, IsEqualTimes b p Q q t and usedSet b t, all in the namespace WardropTraffic.EqualTimes.

Formalization targets

Goal: the closed form (23)–(24)

For every $Q$, $t$ and $q$, the split $q$ is feasible and satisfies the equal-times criterion with common time $t$ if and only if

$$q_i = \begin{cases} p_i\left(1 - \dfrac{b_i}{t}\right) & b_i < t,\\[4pt] 0 & \text{otherwise,}\end{cases} \qquad Q = \sum_{i \in U(t)} p_i - \frac{1}{t}\sum_{i \in U(t)} p_i b_i .$$

This states which routes are used, the flow on each, and the relation between the total flow and the common journey time. The milestones are the steps of Wardrop's derivation:

1. $t_i(x) \ge b_i$ for $0 \le x < p_i$, with equality exactly when $x = 0$;
2. a route in use has $b_i < t$;
3. every route with $b_i < t$ is in use;
4. on a route in use, $q_i = p_i(1 - b_i/t)$, equation (23).

Companion: the equal-times split exists and is unique

If $0 < Q < \sum_i p_i$, there is exactly one pair $(q, t)$ satisfying the criterion. This formalizes the paper's closing sentence, that the solution is found "by picking out the value of $t$ which corresponds to the given $Q$".

Significance

The result. For parallel routes with journey times (22), the equilibrium is explicit. The common time $t$ is the root of a single scalar equation (24), and the flows follow from $t$ by (23). The derivation also shows a threshold structure: a route is used if and only if its empty-route time is below the equilibrium time. Adding flow raises $t$, and the routes enter the set in use one at a time, in increasing order of $b_i$. This structure is what the paper's second criterion (minimum average time, the next mission of this series) is compared with.

Formalizing it. The result is classical and its proof is elementary; it has not been machine-checked. The platform has the existence of a Wardrop equilibrium on general networks for delay functions that are total, continuous and increasing on $\mathbb R$, with no closed form. That model excludes the vertical asymptote of (22) at $q_i = p_i$ and has no empty-route time $b_i$. This mission adds the closed-form characterization for Wardrop's own model, both directions of it, and the existence and uniqueness of the split, including the corner cases that the printed criterion leaves open.

Difficulty

Each step is short. The difficulty is in the boundaries. The paper labels the routes so that $b_1 < \dots < b_D$ and speaks of "the first $j$ routes", with $b_j < t \not> b_{j+1}$. A faithful formal version has to say what happens at $t = b_{j+1}$, at ties among the $b_i$, at $t \le \min_i b_i$ (no route is used), and at a route used near capacity. The printed criterion says "less than" for unused routes, yet the derivation's own case split allows equality. With the strict comparison, an equal-times split fails to exist at the values of $Q$ where $t$ coincides with some $b_k$. The companion's uniqueness requires $Q > 0$: at $Q = 0$ every $t \le \min_i b_i$ is a common time of the zero split. Existence requires a continuity and monotonicity argument for the right-hand side of (24) as a function of $t$.

Formalization scope

• Routes are indexed by Fin D, and all quantities are real.
• The standing hypotheses are $b_i > 0$ and $p_i > 0$ for every $i$. Feasibility includes $q_i < p_i$, the range in which (22) is a positive finite journey time. Without it, Lean's $b_i/0 = 0$ would give a route at capacity journey time $0$.
• The criterion is formalized in the weak form $t \le b_i$ on unused routes, as the paper's derivation uses it. Every split satisfying the printed strict form satisfies it, and the definitions file records the implication. The goal under the weak form is therefore stronger than under the strict one.
• The ordering $b_1 < \dots < b_D$ is not assumed. "The first $j$ routes" becomes the set $U(t) = \{i : b_i < t\}$. This generalisation also covers ties.
• No sign condition on $t$ or $Q$ is assumed in the goal. For $t \le \min_i b_i$ the term $1/t$ multiplies an empty sum, and both sides of the equivalence force $q = 0$ and $Q = 0$.
• The goal is a two-sided equivalence for arbitrary $(Q, q, t)$. The companion requires $0 < Q < \sum_i p_i$ and asserts existence and uniqueness. Together they rule out a vacuous reading in which no split satisfies the criterion.

The development needs only the definitions above and basic real analysis (the intermediate value theorem for the companion). The model of a finite family of parallel routes with hyperbolic journey times is reusable for the minimum-average-time criterion. Proofs of the milestones, of the goal and of the companion are welcome.

Selected references

• J. G. Wardrop, Some theoretical aspects of road traffic research, Proc. Instn Civ. Engrs Part II 1 (1952), 325–362. https://doi.org/10.1680/ipeds.1952.11259
• M. Beckmann, C. B. McGuire, C. B. Winsten, Studies in the Economics of Transportation, Yale University Press, 1956 (RAND RM-1488, 1955). https://www.rand.org/pubs/research_memoranda/RM1488.html
• F. Kelly, E. Yudovina, Stochastic Networks, Cambridge University Press, 2014, ch. 4. https://doi.org/10.1017/CBO9781139565363

Motivation

Two impossibility theorems frame the theory of collective choice. Arrow's theorem (1951) says that a rule aggregating individual preference orderings into a social ordering, subject to a short list of reasonable conditions, must be dictatorial. The Gibbard–Satterthwaite theorem (Gibbard 1973, Satterthwaite 1975) says that a voting procedure selecting a single alternative, which no voter can manipulate by misreporting, must be dictatorial once at least three outcomes are possible. Both conclusions are the same, and the two conditions—Arrow's axioms and strategy-proofness—look unrelated: one is about the coherence of a social ranking, the other about voters' incentives.

Satterthwaite's paper (Northwestern Discussion Paper No. 122, 1974; J. Econ. Theory 10, 1975) shows that the two conditions are in fact the same condition. Section 4 constructs a one-to-one correspondence between strict strategy-proof voting procedures with full range and strict social welfare functions satisfying Arrow's conditions, under which each social welfare function's top choice is the voting procedure's outcome. This mission formalizes that correspondence.

Timeline. Arrow (1951, 2nd ed. 1963) proved the general possibility theorem with conditions of non-negative response (NNR), citizens' sovereignty (CS), independence of irrelevant alternatives (IIA) and non-dictatorship. Gibbard (1973) proved that strategy-proof game forms with at least three outcomes are dictatorial, by first showing that a strategy-proof procedure induces an Arrovian social welfare function and then applying Arrow's theorem. Satterthwaite (1974/75) gave an independent direct proof of the voting-procedure theorem and proved the correspondence theorem (Theorem 2), which turns Gibbard's construction into an exact equivalence.

Setting

A committee $I_n$ of $n$ individuals chooses from a finite set $S_m$ of $m$ alternatives. A strong order on $S_m$ is a complete, transitive relation $R$ with no indifference between distinct alternatives; $x\,\bar R\,y$ denotes strict preference. Let $\rho_m$ be the set of strong orders and $\rho_m^n$ the set of strict ballot sets $B=(B_1,\dots,B_n)$.

• A strict voting procedure is a map $v:\rho_m^n\to S_m$; its range is $T_p=\{v(B):B\in\rho_m^n\}$. It is strategy-proof if no individual $i$, at any $B$, has a ballot $B_i'$ with $v(B_1,\dots,B_i',\dots,B_n)\,\bar B_i\,v(B)$.
• A strict social welfare function is a map $u:\rho_m^n\to\rho_m$; $A_B=u(B)$ is the social ordering.
• For $W\subseteq S_m$, $\Psi_W(R)$ is the set of $R$-best elements of $W$, and $\theta_W(R)$ is the restriction of $R$ to $W$.
• $u$ underlies $v$, and $v$ is derived from $u$, if $\Psi_{S_m}[u(B)]=\{v(B)\}$ for every $B$.

Arrow's conditions on $u$: CS—for all $x\ne y$ some $B$ gives $x\,\bar A_B\,y$; IIA—if $\theta_W(C_i)=\theta_W(D_i)$ for all $i$ then $\Psi_W(A_C)=\Psi_W(A_D)$; NNR—raising an alternative $x$ in individual ballots, with the order of the other alternatives unchanged, never lowers $x$ against any other alternative in the social ordering. PO (Pareto optimality): unanimous strict preference for $x$ over $y$ yields $x\,\bar A\,y$.

Formalization targets

Goal: Theorem 2 (p. 35)

For $n\ge2$ and $m\ge3$ there is a bijection

$$\lambda:\{v \text{ strict, strategy-proof},\ T_p=S_m\}\ \longrightarrow\ \{u \text{ strict},\ \text{CS},\ \text{NNR},\ \text{IIA}\}$$

with $\Psi_{S_m}[\lambda(v)(B)]=\{v(B)\}$ for every $v$ and every $B\in\rho_m^n$.

Milestones

1. CS, NNR and IIA imply PO (p. 31, after Arrow), and PO implies CS (p. 31).
2. Lemma 7 (p. 30): the voting procedure derived from a strict $u$ with CS, NNR, IIA exists, is strategy-proof and has range $S_m$.
3. Gibbard's claim (p. 33): for a strict strategy-proof $v$ with range $S_m$ and a fixed strong order $Q$, the relation $P(B)$ defined by $x\,\bar P\,y\iff x=v[\Delta_{xy}(B_1),\dots,\Delta_{xy}(B_n)]$ is a strong order, and $\mu:B\mapsto P(B)$ underlies $v$ and satisfies PO and IIA.
4. Uniqueness (p. 34): at most one strict $u$ with PO and IIA underlies a strict strategy-proof $v$.
5. NNR (p. 34): such an underlying $u$ satisfies NNR.
6. Lemma 8 (p. 35): a strict strategy-proof $v$ with range $S_m$ has exactly one underlying strict $u$ with CS, NNR, IIA.

Significance

The correspondence explains why the two impossibility theorems have the same conclusion: for strict preferences, a strategy-proof procedure with full range and an Arrovian social welfare function are two descriptions of one object. In particular either impossibility theorem, together with Theorem 2, yields the other. The paper draws a second consequence: a social welfare function violating rationality or IIA has a derived voting procedure that is manipulable, so Arrow's much-debated conditions are forced by the practical requirement of strategy-proofness.

On the formal side, the platform already has machine-checked proofs of the strict Arrow theorem (AGT.arrow_theorem, unanimity and pairwise IIA) and of the strict full-range Gibbard–Satterthwaite theorem (AGT.gibbard_satterthwaite). Together these determine both sides of Theorem 2 as sets of dictatorships, but neither states the correspondence, the derived/underlying relation, Gibbard's construction or NNR, and nothing on the platform states Lemmas 7 or 8. The milestones here formalize the paper's direct argument, which does not pass through the impossibility theorems.

Difficulty

The obvious argument fails in two places. First, a strategy-proof voting procedure determines only the top of a social ordering, and the whole ordering must be recovered; Gibbard's relation $P$ does this, but proving that $P$ is transitive is the core of Gibbard's proof of the Gibbard–Satterthwaite theorem, which the paper cites rather than proves. Second, NNR as stated allows many individuals to move $x$ at once, while the manipulation argument works with one ballot at a time; one must pass from a single-voter change to an arbitrary one without losing IIA or PO along the way.

A newcomer's first idea is to prove both sides are dictatorships and match dictators. That proves the bijection but needs both impossibility theorems as inputs, and the correspondence must still carry the underlying relation for every procedure.

Formalization scope

• Alternatives and individuals are finite types A, ι with decidable equality; $n=|\iota|\ge2$, $m=|A|\ge3$ throughout.
• Weak orders are a structure (relation, completeness, transitivity); strong orders are the subtype with no indifference between distinct elements. Strict ballot sets are functions ι → StrongOrder A, and voting procedures and social welfare functions are defined only on them. Two social welfare functions are therefore equal exactly when they agree on every strict ballot set; this is what makes uniqueness in Lemma 8 and the bijection in Theorem 2 meaningful.
• The range $T_p$ is the image of strict ballot sets; "$T_p\equiv S_m$" is Set.range v = Set.univ.
• $\theta_W(C_i)=\theta_W(D_i)$ is agreement of the two relations on $W\times W$.
• CS is stated for $x\ne y$: as printed ("for every $x,y$") it is unsatisfiable at $x=y$ for a strict social ordering, and every statement would become vacuous. NNR's "for some $x$" is read as "for every $x$".
• "Derived from" and "underlies" are the same relation $\Psi_{S_m}[u(B)]=\{v(B)\}$; Lemma 7 asserts existence of the derived procedure and its properties for every derived procedure.
• Gibbard's $\Delta_{xy}$ and $P$ are definitions; $P$ is the reflexive closure of the paper's $\bar P$.
• The PO claim, PO ⇒ CS, uniqueness and the NNR claim are unconditional in the paper; they are stated under §4's standing $n\ge2$, $m\ge3$, since with no individuals PO fails.
• Theorem 2 is stated as an Equiv together with "$\lambda(v)$ underlies $v$" for every $v$. A bare existence of a bijection between the two sets is a cardinality fact and is not the theorem.

Reusable beyond this mission: the strict-preference vocabulary (strong orders, $\Psi_W$, Arrow's conditions in the paper's form) and Gibbard's $\Delta_{xy}$ construction. Contributions welcome: proofs of each milestone, and bridges to AGT.arrow_theorem and AGT.gibbard_satterthwaite.

Selected references

• M. A. Satterthwaite, Strategy-proofness and Arrow's Conditions: Existence and Correspondence Theorems for Voting Procedures and Social Welfare Functions, Northwestern University CMS-EMS Discussion Paper No. 122, rev. Dec. 12, 1974; J. Econ. Theory 10 (1975) 187–217. https://doi.org/10.1016/0022-0531(75)90050-2
• A. Gibbard, Manipulation of Voting Schemes: A General Result, Econometrica 41 (1973) 587–601. https://doi.org/10.2307/1914083
• K. J. Arrow, Social Choice and Individual Values, 2nd ed., Wiley, 1963.

Motivation

A social welfare function turns the rankings of the members of a committee into one ranking for the committee. Arrow's general possibility theorem (Arrow, 1951/1963) shows that, once there are at least three alternatives, no such rule satisfies a short list of conditions that each look harmless unless it follows a single member's ranking. The theorem is the starting point of social choice theory and underlies the study of voting rules, preference aggregation in economics, and rank aggregation in computer science.

Arrow's own setting allows indifference: ballots and the social ordering are weak orders, and the conditions he imposed are citizens' sovereignty, non-negative response, and independence of irrelevant alternatives. Many textbook proofs, and the existing machine-checked versions, instead take strict ballots and replace the first two conditions by the Pareto condition.

Satterthwaite's discussion paper (Satterthwaite, Northwestern DP No. 122, 1974, journal version J. Econ. Theory 10 (1975)) gives a new proof of Arrow's theorem. Strict Arrovian social welfare functions correspond one-to-one to strategy-proof voting procedures with full range, and the Gibbard–Satterthwaite theorem then forces a dictator. His §6 extends the argument to weak orders by decomposing a social welfare function into a tie-breaking step followed by a strict one. This mission formalizes that weak-order extension and the strict theorem it rests on.

Timeline.

• 1951: Arrow proves the general possibility theorem for weak orders under CS, NNR, IIA and non-dictatorship. The second edition (1963) corrects the first edition's statement.
• 1973: Gibbard proves that every strategy-proof game form with at least three outcomes is dictatorial (Econometrica 41).
• 1975: Satterthwaite proves the same independently for voting procedures, and shows that strategy-proof procedures and Arrovian social welfare functions correspond. This gives a proof of Arrow's theorem by way of strategy-proofness.

Setting

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

A social welfare function $u$ assigns to every ballot set a social ordering $A=u(B)\in\pi_m$. A strict social welfare function $\mu$ is defined only on strong ballot sets $\rho_m^n$ and takes values in $\rho_m$. For $W\subseteq S_m$, $\Psi_W(R)$ is the set of $R$-best elements of $W$, and $\theta_W(R)$ is the restriction of $R$ to $W$.

• CS (citizens' sovereignty): for all distinct $x,y$ some ballot set yields $x\,\bar A\,y$.
• IIA (independence of irrelevant alternatives): if $\theta_W(C_i)=\theta_W(D_i)$ for every $i$, then $\Psi_W(A_C)=\Psi_W(A_D)$.
• NNR (non-negative response): if $D$ differs from $C$ only by raising an alternative $x$ on some ballots, then $x\,\bar A_C\,z$ implies $x\,\bar A_D\,z$ for all $z\neq x$.
• Dictatorial: some $i$ exists such that $x\,\bar B_i\,y$ implies $x\,\bar A\,y$ for every ballot set and all $x,y$.

A tie-breaking function $\alpha$ maps every weak ballot set to a strong one while keeping every strict preference. It is regular if each individual's ties are broken by a fixed strong order $Q_i$.

Formalization targets

Goal: Theorem 3' (p. 49)

For $n\ge 2$, $m\ge 3$ and any social welfare function $u$ on weak ballot sets,

$$u \text{ satisfies CS, NNR, IIA} \;\Longrightarrow\; \exists\, i\;\forall B\;\forall x,y:\; x\,\bar B_i\,y \Rightarrow x\,\overline{u(B)}\,y .$$

The converse is false with indifference, so the goal is one-directional.

Milestones

1. Theorem 3 (p. 36): for strict $\mu$, CS, NNR and IIA hold if and only if $\mu$ is dictatorial.
2. Lemma 10, first sentence (p. 44): if $u$ has range in $\rho_m$ and $u=\mu\circ\gamma$ with $\gamma$ regular and $\mu$ strict Arrovian, then $u$ satisfies IIA, CS and NNR.
3. Lemma 10, second sentence (p. 44): if $u$ has range in $\rho_m$ and satisfies IIA, CS and NNR, then $u=\mu\circ\alpha$ for a tie-breaking function $\alpha$ and a strict $\mu$ satisfying IIA, CS and NNR.
4. Lemma 11 (p. 48): breaking the ties of each social ordering $u(B)$ by a strong order $Q$ preserves CS, NNR and IIA and gives range in $\rho_m$.

Significance

Theorem 3' is Arrow's theorem in the setting Arrow stated it: weak-order ballots, a weak social ordering, and the conditions CS and NNR instead of the Pareto condition. Lemma 10 and Lemma 11 together say that Arrovian social welfare functions with indifference are determined by strict ones up to tie-breaking. This is the structural fact the paper also uses for its weak-order correspondence (Theorem 2').

All results here are proved in the paper. None is formalized as stated. The platform holds a proved strict Arrow theorem, AGT.arrow_theorem, for social welfare functions on strict total orders under unanimity and pairwise IIA. Theorem 3's only-if half follows from it once CS, NNR and IIA are shown to imply the Pareto condition and the two encodings are bridged. The weak-order statement, the tie-breaking lemmas, and the "if" half of Theorem 3 are new to the platform.

Difficulty

Passing from strict to weak orders is the hard step. Restricting a weak ordering to a pair of alternatives does not determine its choice sets on larger sets once ties are present. A social welfare function that satisfies IIA on weak orders need not induce one on strong orders through an arbitrary tie-breaker. Breaking ties ballot by ballot with a non-regular rule can destroy IIA, and breaking ties in the social ordering can destroy NNR unless the same fixed order is used throughout. The obvious reduction is "break all ties and apply the strict theorem", and it fails: the dictator of the tie-broken function could depend on the tie-breaking order. The fact that it does not is part of what must be shown.

Formalization scope

• Alternatives and individuals are finite types A and ι with decidable equality. $n$ = Fintype.card ι, $m$ = Fintype.card A, and $n\ge 2$, $m\ge 3$ are hypotheses as printed. All statements live in StrategyProofArrow.WeakArrow.
• A weak order is a structure (a relation with completeness and transitivity). A strong order is the subtype with no indifference between distinct elements. Strong ballot sets are functions into that subtype, so a strict social welfare function is defined on admissible profiles only.
• $\theta_W(C)=\theta_W(D)$ is agreement of the two relations on $W\times W$. $\Psi_W$ is a set, compared as a set, since weak orders can have several best elements.
• CS is stated for distinct $x\neq y$. As printed ("for every $x,y$") it is unsatisfiable at $x=y$, and every theorem would become vacuous. No other trivializing reading is possible: the dictator conclusion is the paper's one-directional negation of ND, not $u(B)=B_i$, which would be false for weak orders.
• Lemma 11's tie-breaker acts on a single ordering. It is encoded as breaking the ties of $u(B)$ by a strong order $Q$, the "tie-breaking order for $\gamma$" of the proof of Theorem 3'.
• Lemma 10's printed $u^{nm}(B)=u^{nm}[\gamma(B)]$ is read $u(B)=\mu(\gamma(B))$, following the proof.

The definitions duplicate objects drafted in the sibling missions of this series (weak and strong orders, CS, NNR, IIA). Proofs of the strict theorem from the Gibbard–Satterthwaite theorem, bridges to AGT.arrow_theorem, and reusable lemmas about tie-breaking of weak orders are all welcome.

Selected references

• M. A. Satterthwaite, Strategy-proofness and Arrow's Conditions: Existence and Correspondence Theorems for Voting Procedures and Social Welfare Functions, Northwestern University CMS-EMS Discussion Paper No. 122, 1974 (rev. Dec. 12, 1974); J. Econ. Theory 10 (1975) 187–217. https://doi.org/10.1016/0022-0531(75)90050-2
• K. J. Arrow, Social Choice and Individual Values, 2nd ed., Yale University Press, 1963. https://doi.org/10.12987/9780300186987
• A. Gibbard, Manipulation of Voting Schemes: A General Result, Econometrica 41 (1973) 587–601. https://doi.org/10.2307/1914083

Motivation

A finite two-person zero-sum game is given by a real pay-off matrix, and its value can be computed by linear programming. In 1949 George W. Brown proposed a much simpler procedure, now called fictitious play: each player in turn plays a best pure reply to the accumulated play of the opponent so far, and the running averages are read off as estimates of the value (Brown, RAND P-78, 1949). Brown conjectured that both estimates converge to the value. Julia Robinson proved the conjecture in An Iterative Method of Solving a Game, Annals of Mathematics 54 (1951).

The result is the starting point of the theory of learning in games. Fictitious play is the basic model of boundedly rational players who best-respond to empirical frequencies, and the question "for which classes of games does it converge?" has driven a long line of work.

Timeline.

• 1949–1951: Brown proposes the method and conjectures convergence for zero-sum games.
• 1951: Robinson proves it for every vector system of every zero-sum matrix game; the statement contains no rate.
• 1958: Shapiro extracts from Robinson's argument a rate: the gap $(\max V(t) - \min U(t))/t$ is $O(t^{-1/(m+n-2)})$ (doi:10.1002/cpa.3160110408).
• 1964: Shapley gives a 3 × 3 bimatrix (non-zero-sum) game in which fictitious play does not converge (doi:10.1515/9781400882014-002).
• 1996: Monderer and Shapley prove convergence for games with identical interests (doi:10.1006/jeth.1996.0014).
• 2014: Daskalakis and Pan show that with adversarial tie-breaking the convergence can be much slower than the rate $t^{-1/2}$ conjectured by Karlin (arXiv:1412.4840).

Setting

Let $A = (a_{ij})$ be a real $m \times n$ matrix, $m, n \ge 1$. The first player chooses a row $i$, the second a column $j$, and the second pays the first $a_{ij}$. A mixed strategy is a probability vector $x = (x_1, \dots, x_m)$ for the first player, or $y = (y_1, \dots, y_n)$ for the second. For all mixed strategies,

$$\min_j \sum_i a_{ij} x_i \le \max_i \sum_j a_{ij} y_j. \tag{1}$$

A pair $(X, Y)$ for which equality holds is a solution, and the common number $v$ is the value of the game. The minimax theorem says that a solution exists.

Write $A_{i\cdot}$ for the $i$-th row, $A_{\cdot j}$ for the $j$-th column, and $\max W$, $\min W$ for the largest and smallest component of a vector $W$. A vector system for $A$ is a pair of sequences $U(0), U(1), \dots$ of $n$-vectors and $V(0), V(1), \dots$ of $m$-vectors with $\min U(0) = \max V(0)$ and

$$U(t+1) = U(t) + A_{i\cdot}, \qquad V(t+1) = V(t) + A_{\cdot j},$$

where $v_i(t) = \max V(t)$ and $u_j(t) = \min U(t)$. In the alternate vector system the column satisfies $u_j(t+1) = \min U(t+1)$ instead. A row $i$ is eligible in the interval $(t, t')$ if $v_i(t_1) = \max V(t_1)$ for some $t \le t_1 \le t'$, and similarly a column $j$ if $u_j(t_2) = \min U(t_2)$ for some $t \le t_2 \le t'$.

With $U(0) = V(0) = 0$, $U(t)/t$ is the payoff vector of the first player's empirical mixed strategy against each column, and $V(t)/t$ that of the second player's against each row. In the Lean development these objects are vmax, vmin, IsVectorSystem, IsAltVectorSystem, RowEligible, ColEligible and IsSolution, in the namespace RobinsonFP.Convergence.

Formalization targets

Goal: the Theorem (p. 297)

For every vector system $(U, V)$ for $A$, and $v$ the value of the game,

$$\lim_{t\to\infty} \frac{\min U(t)}{t} = \lim_{t\to\infty} \frac{\max V(t)}{t} = v.$$

The statement holds for arbitrary initial vectors with $\min U(0) = \max V(0)$ and for every way of breaking ties.

Milestones, in the order of the proof

1. Inequality (1).
2. Lemma 1: $\liminf_{t\to\infty} (\max V(t) - \min U(t))/t \ge 0$.
3. Lemma 2: if every row and column is eligible in $(s, s+t)$, then $\max U(s+t) - \min U(s+t) \le 2at$ and $\max V(s+t) - \min V(s+t) \le 2at$, where $a = \max_{i,j}|a_{ij}|$.
4. Lemma 3: under the same hypothesis, $\max V(s+t) - \min U(s+t) \le 4at$.
5. Display (3) of the proof of Lemma 4: if some row or column is not eligible in $(s, s+t^*)$, the gap $\max V - \min U$ grows by less than $\tfrac12 \varepsilon t^*$ over that window, given the bound $\tfrac12\varepsilon t$ for the vector systems of the submatrices.
6. Lemma 4: for every $\varepsilon > 0$ there is $t_0$, uniform over all vector systems for $A$, with $\max V(t) - \min U(t) < \varepsilon t$ for $t \ge t_0$.
7. $(\max V(t) - \min U(t))/t \to 0$.
8. $\limsup \min U(t)/t \le v$ and $\liminf \max V(t)/t \ge v$.

Two further items are not milestones: the Theorem for the alternate vector system, which the paper says follows by the same proofs, and the bracketing $\min U(t)/t \le v \le \max V(t')/t'$ when $U(0) = V(0) = 0$ (p. 297).

Significance

The Theorem shows that a payoff-based procedure with no linear algebra finds the value of every zero-sum matrix game. It was one of the first iterative methods for linear programs with a convergence proof, and it is the base case for every later convergence result about fictitious play: potential games, games with identical interests, $2\times n$ games, and continuous-time best-response dynamics.

The result is proved, and its proof is short. To our knowledge it has no machine-checked proof. The mission produces a Lean proof of the Theorem and its four lemmas, together with reusable definitions of vector systems and eligibility. A statement with an explicit rate, such as Shapiro's, or a proof for the alternate system, is a natural extension.

Difficulty

Lemmas 1–3 are elementary estimates. The difficulty is Lemma 4. The obvious approach follows a single run of the iteration and tries to show that the gap $\max V(t) - \min U(t)$ grows sublinearly. This fails because a run can spend arbitrarily long windows in which some row or column is never a best reply, and nothing about one fixed run controls the gap over such a window. What is needed is a bound that is uniform over all vector systems, whatever their initial vectors and tie-breaking, which is why $t_0$ in Lemma 4 comes before the vector system, and why display (3) quantifies over every vector system of the smaller matrices. In Lean, this uniformity has to range over matrices of every smaller size, so the statements must be general in the index types.

Formalization scope

• Rows and columns are indexed by finite nonempty types ι, κ (the paper's $m, n \ge 1$); Fin m, Fin n is a special case. The matrix is Matrix ι κ ℝ.
• $\max W$, $\min W$ are Finset.sup' and Finset.inf' over all indices, hence attained.
• A vector system allows any maximizing row and minimizing column at each step (an existential per step). No tie-breaking rule is fixed, and the initial vectors are arbitrary subject to $\min U(0) = \max V(0)$. The case $U(0) = V(0) = 0$ is not imposed.
• Time is a natural number. Limits are Tendsto … atTop (𝓝 ·); lim inf and lim sup of real sequences are stated in $\varepsilon$-form (for every $\varepsilon > 0$, eventually), with no boundedness side conditions.
• The value $v$ is given by a solution: every statement about $v$ assumes IsSolution A x y v, i.e. probability vectors $x$, $y$ with $\min_j \sum_i a_{ij} x_i = v = \max_i \sum_j a_{ij} y_j$. Such a solution exists by the minimax theorem, which is proved on the platform as MatousekLP.ZeroSum.minimax_equality in a different encoding. A statement with $v$ free, or with "there exists $v$", would be false or would lose the identification with the value; neither is used.
• In Lemmas 2 and 3, $a$ is any upper bound on the $|a_{ij}|$. This is equivalent to the paper's $a = \max_{i,j}|a_{ij}|$.
• In display (3), the bound for submatrices is assumed only for the submatrices that delete one row or one column, which makes the statement at least as strong as the paper's.
• The paper's closing display on p. 301 prints $\lim \min V(t)/t$ for $\lim \min U(t)/t$. The goal follows the statement of the Theorem on p. 297.

A general "restriction of a vector system to a submatrix" lemma would be reusable for later work on fictitious play. Proofs of any milestone are welcome, as are proofs of the two extra items.

Selected references

• J. Robinson, An Iterative Method of Solving a Game, Annals of Mathematics 54(2), 296–301, 1951. https://doi.org/10.2307/1969530
• G. W. Brown, Some notes on computation of games solutions, RAND Report P-78, 1949. https://www.rand.org/pubs/papers/P78.html
• H. N. Shapiro, Note on a computation method in the theory of games, Communications on Pure and Applied Mathematics 11(4), 587–593, 1958. https://doi.org/10.1002/cpa.3160110408
• L. S. Shapley, Some topics in two-person games, Advances in Game Theory, Annals of Mathematics Studies 52, 1964. https://doi.org/10.1515/9781400882014-002
• D. Monderer, L. S. Shapley, Fictitious play property for games with identical interests, Journal of Economic Theory 68, 258–265, 1996. https://doi.org/10.1006/jeth.1996.0014
• C. Daskalakis, Q. Pan, A counter-example to Karlin's strong conjecture for fictitious play, FOCS 2014. https://arxiv.org/abs/1412.4840

Motivation

Classical cooperative game theory assumes that any coalition of players can form and coordinate. In many settings cooperation is mediated by pairwise relationships: communication lines, contracts, alliances, or trade links. Roger Myerson's discussion paper Graphs and Cooperation in Games (Northwestern University, 1976; published in Mathematics of Operations Research 2(3), 1977, doi:10.1287/moor.2.3.225) models such a cooperation structure as a graph on the set of players and asks how the players should share the worth of the game when only linked players can coordinate directly.

The answer, now called the Myerson value, is the starting point of the literature on communication situations and network games. It underlies later work on network formation (Jackson and Wolinsky, A strategic model of social and economic networks, JET 1996) and on allocation rules for networks, and it is a standard textbook example of an axiomatic solution concept.

Timeline:

• 1953. Shapley defines the Shapley value $\varphi$ for transferable-utility games by efficiency, symmetry, a carrier axiom and additivity (Shapley 1953).
• 1976–1977. Myerson introduces cooperation graphs, the fairness (equal gains from each link) condition, proves existence and uniqueness of the fair allocation rule, identifies it as the Shapley value of the graph-restricted game, proves its total stability for superadditive games, and extends existence and uniqueness to games without transferable utility in graph function form.

Setting

Let $N$ be a nonempty finite set of players and $CL$ the set of nonempty coalitions $S\subseteq N$. A game in characteristic function form is a vector $v\in\mathbb R^{CL}$; $v_S$ is the transferable wealth coalition $S$ can divide.

A link $n{:}m$ is an unordered pair of distinct players and a graph $g$ is a set of links; $GR$ is the set of all graphs, $\bar g^N$ the complete graph, $g\setminus n{:}m$ the graph with one link removed, and $|g|$ the number of links. Players $a,b$ are connected in $S$ by $g$ if $a=b\in S$ or a path of links of $g$ joins them through players of $S$ only; the classes form the partition $S/g$ of $S$, and $N/g$ is the set of connected components of $g$. The graph-restricted game is

$$(v/g)_S=\sum_{T\in S/g}v_T .$$

An allocation rule is a function $Y:GR\to\mathbb R^N$, with $Y_n(g)$ the payoff of player $n$ under cooperation structure $g$. It is a fair allocation rule for $v$ if

1. (efficiency, (7)) $\sum_{n\in S}Y_n(g)=v_S$ for every $g$ and every component $S\in N/g$, and
2. (equity, (10)) $Y_n(g)-Y_n(g\setminus n{:}m)=Y_m(g)-Y_m(g\setminus n{:}m)$ for every $g$ and every link $n{:}m\in g$.

$Y$ is totally stable if $Y_n(g)\ge Y_n(g\setminus n{:}m)$ for every $g$ and every link $n{:}m\in g$, and $v$ is superadditive if $v_{S\cup T}\ge v_S+v_T$ for disjoint $S,T\in CL$.

A game in graph function form assigns to every pair $(S,g)$ with $S\in N/g$ a closed, comprehensive (closed under decreasing coordinates), proper ($\emptyset\ne W\ne\mathbb R^S$) set $w(S,g)\subseteq\mathbb R^S$ of feasible payoffs; its fair allocation rule replaces (7) by (14), $(Y_n(g))_{n\in S}\in\partial w(S,g)$.

Formalization targets

Goal: Theorem 3 (p. 8)

If $v$ is superadditive, then the fair allocation rule $Y$ for $v$ is totally stable:

$$Y_n(g)\ge Y_n(g\setminus n{:}m)\qquad\text{for all } g\in GR,\ n{:}m\in g .$$

Theorem 1 (p. 7) and Theorem 4 (p. 10)

Every $v\in\mathbb R^{CL}$ has a unique fair allocation rule; every game $w$ in graph function form has a unique $Y$ satisfying (14) and (10).

Theorem 2 (p. 8)

The fair allocation rule is

$$Y(g)=\varphi(v/g)\quad\text{for all }g\in GR,\qquad\text{in particular } Y(\bar g^N)=\varphi(v).$$

The milestones follow the paper's Section 7: the steps of the proof of Theorem 4 (displays (15)–(17)), Theorem 4, Theorem 1, the decomposition of $v/g$ and the efficiency and equity of $\varphi(v/g)$ (proof of Theorem 2), Theorem 2, and the monotonicity of $v/g$ and $\varphi(v/g)$ in a link (proof of Theorem 3). Theorem 3 is the goal because its proof uses the formula of Theorem 2, whose proof uses the uniqueness of Theorem 1, which is the transferable-utility case of Theorem 4: all four numbered results lie on one path.

Significance

The theorems give an axiomatic foundation for allocation in networks: two natural requirements, component-wise efficiency and equal gains from each link, single out one rule, and that rule is an explicit formula built from the Shapley value. At the complete graph it recovers the Shapley value itself, so the result is also a new characterization of the Shapley value. Total stability says that, for superadditive games, no player has an incentive to break a link, which connects the allocation rule to the question of which networks form.

The results are proved in the paper. A search of the platform found no formalization of cooperation graphs, the graph-restricted game, the Myerson value or total stability; the Shapley value is available as a platform definition and is reused. This mission produces machine-checked statements of all four theorems and of the intermediate steps of their proofs, together with a reusable definition layer for communication situations.

Difficulty

The equity condition (10) relates the payoff at a graph to the payoff at a graph with one fewer link, and it constrains only pairs of linked players; it is not evident that these conditions, together with efficiency on components, determine the rule at every graph, nor that they are consistent. Uniqueness and existence must hold simultaneously for all $2^{|\bar g^N|}$ graphs, and the constraints couple each graph to all of its subgraphs and each player to every other player of its component. In the graph function form, efficiency becomes a boundary condition on a closed comprehensive set, and the existence and uniqueness of the relevant extremal point depend on all three properties of $w(S,g)$.

Identifying the rule with $\varphi(v/g)$ requires the efficiency of the Shapley value on each component of $g$, which is not the efficiency of $\varphi$ on $N$, and equity requires tracking how the partitions $S/g$ change when a link is removed. Total stability is false for general games: without superadditivity a player can gain by cutting a link, so the hypothesis cannot be dropped.

Formalization scope

Players are Fin n, with $0<n$ in every theorem as the paper assumes $N$ nonempty; the paper's player $k$ is index $k-1$. The general game carrier has its own definition module, and the graph-specific definitions build on it. Graphs are SimpleGraph (Fin n): $\bar g^N$ is ⊤, the empty graph ⊥, $h\subseteq g$ is h ≤ g and $h\subset g$ is h < g. A game is a function Finset (Fin n) → ℝ; its value at $\emptyset$ is a junk coordinate that no definition reads, and no theorem assumes $v_\emptyset=0$. Superadditivity quantifies over nonempty coalitions only. The Shapley value is the platform definition Supermodularity.Cooperative.ShapleyValue, applied after resetting the value at $\emptyset$ to $0$. $\mathbb R^S$ is ↥S → ℝ with the product topology, and $\partial$ is the topological frontier.

Explicit readings of the typescript:

• The printed definition of "connected in $S$ by $g$" (p. 3) asks $n^i\in S$ only for $i\ge1$; the formalization requires every vertex of the path, including the start, to lie in $S$, which makes $S/g$ the partition of $S$ the paper describes.
• Comprehensiveness (p. 10) prints "$\forall n\in N$" for coordinates of vectors in $\mathbb R^S$; read as $n\in S$.
• Display (17) writes $Y_n(h)$ under the index $m\in S$; read as $Y_m(h)$, as in (18b).
• The proof headed "PROOF OF THEOREM 4." on p. 13 is the proof of Theorem 3.
• "The unique fair allocation rule" in Theorems 2 and 3 is stated for every fair allocation rule; existence and uniqueness are Theorem 1.
• The paper's $N$ is nonempty; every theorem carries the corresponding hypothesis $0<n$.

The equity and stability conditions quantify over links of $g$ only. Quantifying over all pairs of players would make Theorem 1 false and the goal vacuous, so that reading is ruled out. Likewise (14) is boundary membership, not membership in $w(S,g)$.

Contributions welcome: general lemmas on the partitions $S/g$ (refinement under link deletion, restriction to components), Möbius inversion over the subgraph lattice of a finite simple graph, the carrier and null-player properties of the Shapley value, and the extremal-point lemma for closed comprehensive sets. These are reusable beyond this mission.

Selected references

• R. B. Myerson, Graphs and Cooperation in Games, Discussion Paper No. 246, CMS-EMS, Northwestern University, September 1976; published in Mathematics of Operations Research 2(3):225–229, 1977. https://doi.org/10.1287/moor.2.3.225
• L. S. Shapley, A Value for n-Person Games, in Contributions to the Theory of Games II, Annals of Mathematics Studies 28, Princeton University Press, 1953, pp. 307–317. https://doi.org/10.1515/9781400881970-018
• M. O. Jackson and A. Wolinsky, A Strategic Model of Social and Economic Networks, Journal of Economic Theory 71(1):44–74, 1996. https://doi.org/10.1006/jeth.1996.0108