Algorithmic Game Theory

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

Motivation

A correlated equilibrium describes a recommendation scheme for a game: a common random device selects a profile of actions, tells each player only their own recommended action, and no player gains in expectation by replacing that recommendation with another action. This makes sense even when there are infinitely many players. The finite-player existence theorem, however, does not settle what happens to a probability distribution on the product of infinitely many strategy sets, or whether that distribution is countably additive. Hart and Schmeidler proved that continuous payoffs and finite individual strategy sets suffice, with no countability assumption on the player set. Their Theorem 2(ii) is the target here.

The distinction between correlation and independent play is material. Peleg's 1969 paper studied equilibrium points with infinitely many players. Hart and Schmeidler reproduce a discontinuous binary-action example with no Nash equilibrium yet a countably additive correlated equilibrium, then change its payoffs to obtain a game with no countably additive correlated equilibrium. Those examples explain why the measure class and payoff regularity in the theorem need to be stated precisely. The modified example is an additional target of this mission. The main existence theorem is already proved in the 1989 paper; the mission asks for a machine-checked formalization of that known result and its selected proof steps.

Setting

Let $N$ be a nonempty set of players, possibly uncountable. Player $i\in N$ has a nonempty finite set $S^i$ of pure strategies. A strategy profile is a tuple $s\in S=\prod_{i\in N}S^i$. A game specifies a real payoff $h^i(s)$ for every player and profile. Each $S^i$ has the discrete topology; $S$ has the product topology. Write $\Sigma_0$ for the product σ-algebra, generated by cylinder events that inspect finitely many coordinates. It can be strictly smaller than the Borel σ-algebra of $S$ when $N$ is uncountable.

For $r^i,t^i\in S^i$, write $(s^{-i},t^i)$ for the profile obtained by replacing only the $i$th coordinate of $s$ by $t^i$. A countably additive probability measure $p$ on $(S,\Sigma_0)$ is a correlated equilibrium when every recommendation $r^i$ gives a nonnegative expected advantage over switching to $t^i$:

$$\int_{\{s:s^i=r^i\}}\left[h^i(s)-h^i(s^{-i},t^i)\right]\,dp(s)\ge 0.$$

The inequality is weighted by the probability of receiving $r^i$; it remains meaningful when that probability is zero. The integrand must be integrable on this cylinder. In the theorem, continuity and compactness provide the boundedness and measurability needed for the integral. For the separate discontinuous example, integrability is checked as part of the equilibrium condition.

Formalization targets

Theorem 2(ii): countably additive existence

For arbitrary nonempty $N$, finite nonempty $S^i$, and continuous payoffs $h^i:S\to\mathbb R$, the goal is

$$\exists p\in\mathcal P_{\sigma}(S,\Sigma_0)\quad \forall i\in N\ \forall r^i,t^i\in S^i, \quad \int_{\{s:s^i=r^i\}}[h^i(s)-h^i(s^{-i},t^i)]\,dp(s)\ge0.$$

Here $\mathcal P_{\sigma}$ denotes countably additive probability measures. The supporting targets follow the source's proof: every finite-restriction game has an equilibrium, a family of such equilibrium measures has a cluster point when tested against continuous real functions, and that cluster point satisfies the incentive inequalities. The cluster statement tests finite collections of functions, which is what a neighborhood in the weak topology requires.

Example 2: the continuity boundary

Players $i=1,2,\ldots$ choose $s^i\in\{0,1\}$. Let Case 1 mean that only finitely many players choose $1$. The payoff is $s^i/i^2$ in Case 1 and $-s^i$ otherwise. The additional target states

$$\nexists\text{ a countably additive correlated equilibrium on }(S,\Sigma_0).$$

Theorem 2(i), which asserts existence for bounded measurable payoffs using a finitely additive probability on a larger algebra, is outside this proposal. It is a different conclusion requiring finitely additive integration.

Significance

Theorem 2(ii) gives an equilibrium distribution that is an ordinary countably additive probability measure, while allowing arbitrarily many players. It lets the same incentive test be applied to each player's observable recommendation event, without replacing the product σ-algebra by a larger space of events. Example 2 shows the statement changes when continuity is dropped: bounded measurable binary payoffs alone do not guarantee a countably additive equilibrium. Both claims are established in the source paper.

Formalizing the result produces reusable interfaces for probability measures on products of finite strategy spaces, finite-support equilibrium distributions, and weak tests by continuous functions. The local Lean files compile as statements; the goal and milestone theorems remain open for machine-checked proofs. Platform work on finite Nash and correlated equilibria, including AGT.nash_existence, AGT.IsCorrelatedEquilibrium, Aumann1987.*, and CalibratedCE.*, supplies related vocabulary but uses finite-player or different distribution conventions. None of those declarations is used as a substitute for this theorem about an arbitrary player set.

Difficulty

Finite strategy sets do not make the full profile space finite when the player set is infinite. A direct finite-game argument therefore supplies only finite restrictions, and an arbitrary limit of their distributions may lose either countable additivity or the incentive inequalities if the topology and σ-algebra are handled carelessly. Continuity is what makes the payoff-difference tests compatible with the weak topology on measures. The paper's discontinuous Example 2 rules out the tempting extension from continuous to merely bounded measurable payoffs.

Formalization scope

Profiles have Lean type ∀ i, S i; payoffs have type ι → (∀ i, S i) → ℝ. The theorem assumes [Nonempty ι], a finite nonempty strategy type for each player, discrete topologies and discrete measurable structures on the factors, and continuity of every payoff on the product. It does not assume Countable ι. The default Pi measurable structure is $\Sigma_0$. Measures are Mathlib's countably additive Measure, with IsProbabilityMeasure. IsCorrelatedEq includes IntegrableOn explicitly, because an undefined Bochner integral otherwise evaluates to zero in Lean and could make the equilibrium condition empty.

An f-set has a nonempty finite strategy subset at every coordinate and differs from a singleton at only finitely many coordinates. Finite weighted profiles represent its equilibrium measure; this avoids treating a profile singleton as measurable in an uncountable product. For the cluster-point statements, f-sets contain a fixed anchor profile $\hat s$. The paper orders all f-sets by inclusion and calls them a net, but that index set is not directed: two singleton products can disagree at infinitely many coordinates. Anchored f-sets are directed and admit every finite coordinate demand used in the argument. This repair is explicit in the milestone statements and audit notes. Neither the goal nor the equilibrium definition depends on the chosen anchor.

The development needs product topology and σ-algebra facts, finite-game correlated-equilibrium existence, compactness for probability measures tested by continuous functions, and finite-sum-to-integral connections. Contributions proving these steps or the main theorem are in scope. The finitely additive conclusion of Theorem 2(i), Peleg's first example, and the paper's noncountably additive example measure are not formalized here. A sorry-free check supplies a concrete two-player coordination game and a correlated equilibrium, demonstrating that the main hypotheses are satisfiable.

Selected references

• Sergiu Hart and David Schmeidler, Existence of Correlated Equilibria, Mathematics of Operations Research 14 (1989), 18–25. DOI: 10.1287/moor.14.1.18.
• Bezalel Peleg, Equilibrium Points for Games with Infinitely Many Players, Journal of the London Mathematical Society s1-44 (1969), 292–294. DOI: 10.1112/jlms/s1-44.1.292.

Motivation

A two-person zero-sum stochastic game (also called a Markov game) is a Markov decision problem with two decision makers who pull in opposite directions: at every time point both players choose an action simultaneously, one player pays the other, and the system moves to a random next state whose law depends on the current state and both actions. Stochastic games were introduced by Shapley (Shapley 1953) and are the standard model for adversarial sequential decisions in operations research, economics and computer science (pursuit–evasion, inspection, robust control against an adversarial environment).

Shapley proved that a discounted stochastic game has a value and that both players have stationary optimal policies. The value, however, is in general not computable by linear programming: it need not lie in the field generated by the data. Kallenberg's Example 6.2.1 (after Parthasarathy and Raghavan) has rational data and an irrational value in one state. When only one player controls the transition probabilities, the situation changes: the value and stationary optimal policies are the optimal solutions of one pair of dual linear programs (Parthasarathy & Raghavan, as cited in Kallenberg 1983, pp. 192 and 196; Kallenberg 1983, Chapter 6).

Timeline.

• 1953: Shapley proves existence of the value and of stationary optimal policies for the discounted game.
• 1977–1978: Parthasarathy and Raghavan study games in which one player controls the transitions and identify an order-field property for the value and optimal decision rules (cited in Kallenberg 1983, pp. 192, 196).
• 1983: Kallenberg presents the dual pair (6.2.1)/(6.2.2), with the controlling player's policy read off the dual and the opponent's from the primal, and a constructive existence proof (Remark 6.2.2).

Setting

The state space is $E = \{1,\dots,N\}$ with $N>0$. In state $i$ player I chooses an action $a$ from a finite nonempty set $A(i)$ and player II an action $b$ from a finite nonempty set $B(i)$. Player I then receives $r_{iab}$ from player II, and the next state is $j$ with probability $p_{iabj} \ge 0$, where $\sum_j p_{iabj} \le 1$.

A history at time $t$ is $(i_1,a_1,b_1,\dots,i_{t-1},a_{t-1},b_{t-1},i_t)$. A policy $R_1$ of player I chooses, at each time and history, a probability distribution on $A(i_t)$; policies $R_2$ of player II are defined likewise. A policy is stationary, written $\pi^\infty$ or $\rho^\infty$, if the distribution depends only on the current state. With $v_i^t(R_1,R_2)$ the expected reward in period $t$ from initial state $i$, the total reward is $v_i(R_1,R_2) = \sum_{t\ge1} v_i^t(R_1,R_2)$.

A pair $(R_1^*,R_2^*)$ is optimal if, componentwise,

$$v(R_1,R_2^*) \le v(R_1^*,R_2^*) \le v(R_1^*,R_2) \qquad\text{for all policies } R_1,R_2, \tag{6.1.1}$$

and then $\mathrm{val(TMG)} := v(R_1^*,R_2^*)$ is the value of the game.

Assumption 6.2.1 (contraction). There are $\mu \gg 0$ and $\alpha\in[0,1)$ with $\sum_j p_{iabj}\mu_j \le \alpha\mu_i$ for all $i$, $a\in A(i)$, $b\in B(i)$. The discounted game is the case $\mu = e$.

Assumption 6.2.2 (single controller). $p_{iabj}$ does not depend on $b$; it is written $p_{iaj}$.

For a stationary $\rho$ write $r_{ia}(\rho) = \sum_b r_{iab}\rho_{ib}$ and $p_{iaj}(\rho)=\sum_b p_{iabj}\rho_{ib}$. A vector $y$ is TMG-superharmonic if some stationary $\rho^\infty$ of player II satisfies $y_i \ge r_{ia}(\rho) + \sum_j p_{iaj}(\rho) y_j$ for all $a\in A(i)$, $i\in E$. For weights $\beta_j>0$ the two linear programs are

$$\min\Big\{\textstyle\sum_j\beta_jy_j \ \Big|\ \sum_j(\delta_{ij}-p_{iaj})y_j-\sum_b r_{iab}\rho_{ib}\ge0;\ \sum_b\rho_{ib}=1;\ \rho_{ib}\ge0\Big\} \tag{6.2.1}$$ $$\max\Big\{\textstyle\sum_iz_i \ \Big|\ \sum_i\sum_a(\delta_{ij}-p_{iaj})x_{ia}=\beta_j;\ -\sum_a r_{iab}x_{ia}+z_i\le0;\ x_{ia}\ge0\Big\} \tag{6.2.2}$$

Formalization targets

Goal: Theorem 6.2.3

Under Assumptions 6.2.1 and 6.2.2, let $(y^*,\rho^*)$ and $(x^*,z^*)$ be optimal solutions of (6.2.1) and (6.2.2), and $\pi^*_{ia} := x^*_{ia}/\sum_a x^*_{ia}$. Then

$$v(R_1,(\rho^*)^\infty) \le v((\pi^*)^\infty,(\rho^*)^\infty) = y^* \le v((\pi^*)^\infty,R_2)\qquad\text{for all policies } R_1,R_2 .$$

The goal fixes no constants; it states that the LP pair produces the value and optimal stationary policies.

Milestones

1. Theorem 6.2.1 (Shapley): under Assumption 6.2.1 both players have stationary optimal policies.
2. Theorem 6.2.2: under Assumption 6.2.1, $\mathrm{val(TMG)}$ is the smallest TMG-superharmonic vector.
3. Theorem 6.2.4 (i): for a stationary $\pi^\infty$ of player I, $x_{ia}(\pi) = [\beta^T(I-P(\pi))^{-1}]_i\pi_{ia}$ and $z_i(\pi) = \min_{b} r_{ib}(\pi)\sum_a x_{ia}(\pi)$ give a feasible point of (6.2.2) with $\sum_i z_i(\pi) = \min_\rho \sum_j\beta_j v_j(\pi^\infty,\rho^\infty)$.
4. Theorem 6.2.4 (ii): every feasible $(x,z)$ of (6.2.2) has $x = x(\pi)$ and $z\le z(\pi)$ for $\pi_{ia} = x_{ia}/\sum_a x_{ia}$.

Theorems 6.2.1 and 6.2.2 hold for the general contracting game. Assumption 6.2.2 enters only from (6.2.1) on.

Significance

The result. Theorem 6.2.3 turns a single-controller game into a finite computation, Algorithm XXVII: solve one LP pair and read off the value and optimal stationary policies of both players. A consequence (Remark 6.2.1) is that the value and the optimal decision rules lie in the field generated by the rewards and transition probabilities. Example 6.2.1 shows this fails without Assumption 6.2.2. Theorem 6.2.4 matches the feasible points of the dual program with the stationary policies of the controlling player. This is the game version of the correspondence between state-action frequencies and policies in Markov decision problems.

Formalizing it. All results are proved in the book, and Theorem 6.2.1 is classical. None of them is formalized: the platform has turn-based stochastic games with positional strategies (TBSGStrategyIteration), which do not cover simultaneous moves or history-dependent randomized policies. The mission adds a reusable model of simultaneous-move stochastic games with history-dependent policies, together with machine-checked optimality of the LP solution against every such policy.

Difficulty

There are two difficulties. First, optimality in (6.1.1) is against every history-dependent randomized policy of the opponent, while the LP produces only stationary policies. Fixing one player's stationary policy reduces the game to a Markov decision problem for the other player (Remark 6.1.1), and the facts needed from that problem (stationary policies suffice, and the value is the smallest superharmonic vector) are theorems about contracting MDPs, not consequences of the LP. Second, Theorem 6.2.2 rests on Shapley's existence theorem, which is not a linear-programming fact: its usual proof is a fixed-point argument for the Shapley operator built from one-stage matrix games. Remark 6.2.2 indicates a route that avoids it, through the bounded polytope of state-action frequencies of a contracting MDP. Either way, LP duality alone does not give optimality against non-stationary opponents.

Formalization scope

• Model. $E$ is Fin N with $N>0$. Actions live in finite types α, β, and $A(i)$, $B(i)$ are nonempty Finsets. Rows are substochastic.
• Policies. A history in $H_{n+1}$ is a record of $n+1$ states and $n$ actions of each player. A policy is a family of distributions indexed by time and history, supported on the current action set. Stationary policies are the image of state-dependent decision rules.
• Probabilities and reward. History probabilities are explicit finite products, with no measure theory. The total reward is the tsum of the period rewards, which converges absolutely under Assumption 6.2.1, and every theorem assumes it.
• Linear programs. Their variables are functions on all actions that vanish off $A(i)$ (resp. $B(i)$). Optimality means feasible and attaining the min/max over the feasible set. The common $p_{iaj}$ is $p_{iab_0j}$ for a fixed $b_0\in B(i)$, and Assumption 6.2.2 makes the choice irrelevant. $\beta_j>0$ is a hypothesis, as on p. 194.
• The minimum in Theorem 6.2.4 (i) is over stationary policies of player II and is stated with attainment.

Restricting either player's policy class to stationary policies would make the optimality claims of Theorems 6.2.1 and 6.2.3 a statement about a finite family and is ruled out: the comparison class is all history-dependent randomized policies.

Lemma 6.1.1 is Mathlib's isSaddlePointOn_value (Mathlib/Order/SaddlePoint.lean) and is not restated. The LP duality theorems of Chapter 1 are proved on the platform (LinearOptimization.lp_strong_duality, lp_complementary_slackness) and may be used. Useful contributions include: the reduction of Remark 6.1.1 (a fixed stationary opponent gives an MDP), the contracting-MDP facts it needs, and a proof of Theorem 6.2.1. The model definitions are reusable for any finite stochastic game.

Selected references

• L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983, Chapter 6. https://ir.cwi.nl/pub/13008
• L. S. Shapley, Stochastic games, Proceedings of the National Academy of Sciences 39 (1953) 1095–1100. https://doi.org/10.1073/pnas.39.10.1095
• T. Parthasarathy and T. E. S. Raghavan, Finite algorithms for stochastic games, International Conference on Dynamic Programming, Vancouver, 1977; cited in Kallenberg 1983, p. 232. https://ir.cwi.nl/pub/13008
• T. Parthasarathy and T. E. S. Raghavan, An order field property for stochastic games when one player controls the transition probabilities, Game Theory Conference, Cornell, 1978; cited in Kallenberg 1983, p. 233. https://ir.cwi.nl/pub/13008

Motivation

A manufacturer launching a new product often depends on a single supplier for a critical component, and the supplier must build capacity before demand is known. The manufacturer usually knows more about demand than the supplier does: her sales force, market research and order history give her a forecast the supplier cannot verify, and she has a reason to inflate it, since more capacity costs her nothing if the supplier pays for it. Whether contracts can make forecast sharing credible, and at what cost to the supply chain, is the subject of Cachon and Lariviere, "Contracting to assure supply: how to share demand forecasts in a supply chain" (Management Science 47(5), 2001, doi:10.1287/mnsc.47.5.629.10486). Section 6.10 of G. P. Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, Vol. 11, 2003) presents a simplified version of that model, and this mission formalizes it from the author's January 2003 draft.

The section separates two regimes. Under forced compliance the supplier must build exactly the capacity the contract specifies; under voluntary compliance he may build less. The section's conclusion is that forced compliance allows both coordination and credible forecast sharing, while voluntary compliance allows forecast sharing only at the price of under-investment in capacity.

Setting

Demand $D_\theta$ has one of two types $\theta \in \{h, l\}$ with distribution function $F_\theta(x) = F(x\mid\theta)$. The page assumes $F_\theta(x) = 0$ for $x < 0$, $F_\theta(x) > 0$ for $x \ge 0$ (so demand has an atom at $0$), $F_\theta$ increasing and differentiable, and stochastic dominance $F_h(x) < F_l(x)$ for all $x \ge 0$. The supplier $S$ builds capacity $k$ at cost $c_k > 0$ per unit; after demand is observed he produces $\min\{D_\theta, k\}$ at cost $c_p > 0$ per unit; the manufacturer $M$ earns $r > c_p + c_k$ per unit of demand satisfied; unused capacity is worth nothing.

Expected sales with $x$ units of capacity are $S_\theta(x) = x - E[(x - D_\theta)^+]$, and the supply chain's expected profit is

$$\Omega_\theta(k) = (r - c_p)S_\theta(k) - c_k k .$$

An optimal capacity $k_\theta^o$ maximizes $\Omega_\theta$ over $k \ge 0$, and $\Omega_\theta^o = \Omega_\theta(k_\theta^o)$.

In an options contract $M$ buys $q_i$ options at $w_o$ each and pays $w_e$ for each option exercised. With $k = q_i$ her profit is $\Pi_\theta(q_i) = (r - w_e)S_\theta(q_i) - w_o q_i$ and the supplier's is $(w_e - c_p)S_\theta(q_i) + w_o q_i - c_k q_i$. The contract with share $\lambda$ sets $r - w_e = \lambda(r - c_p)$ and $w_o = \lambda c_k$. Under a wholesale price contract with price $w$ the supplier earns $\pi_\theta(k) = (w - c_p)S_\theta(k) - c_k k$; the price inducing capacity $k$ is $w_\theta(k) = c_k/\bar F_\theta(k) + c_p$ with $\bar F_\theta = 1 - F_\theta$, and the manufacturer then earns $\Pi_\theta(k) = (r - w_\theta(k))S_\theta(k)$.

With asymmetric information only $M$ observes $\theta$. Let $\hat\pi$ be the supplier's minimum acceptable profit, and define the shares

$$\lambda_l = 1 - \frac{\hat\pi}{\Omega_l^o},\qquad \lambda_h = 1 - \frac{\hat\pi}{\Omega_h^o},\qquad \hat\lambda_h = \frac{\Omega_l^o - \hat\pi}{\Omega_l(k_h^o)},\qquad \lambda_H = \min\{\lambda_h, \hat\lambda_h\}.$$

Formalization targets

Goal: forced-compliance separating contracts (§6.10.3, pp. 103–104)

The low type offers the options contract with share $\lambda_l$ and initial order $k_l^o$, the high type the one with share $\lambda_H$ and initial order $k_h^o$. Assuming $0 < \hat\pi < \Omega_l^o$ and $\Omega_l(k_h^o) > 0$:

$$0 < \lambda_l < \lambda_H < 1,\qquad \lambda_l\,\Omega_h(k_l^o) < \lambda_H\,\Omega_h^o,\qquad \lambda_H\,\Omega_l(k_h^o) \le \Omega_l^o - \hat\pi,$$

the supplier earns $\hat\pi$ from the low type and at least $\hat\pi$ from the high type, and each initial order $k_\theta^o$ maximizes both firms' profits. The profit comparisons are stated between the contract profit functions, not between shares.

Milestones

1. $S_\theta(x) = x - \int_0^x F_\theta$ (p. 98).
2. $\Omega_\theta$ is concave, and $k > 0$ is optimal iff $\bar F_\theta(k) = c_k/(r - c_p)$ (p. 99).
3. $\Omega_l(k) < \Omega_h(k)$ for $k > 0$, hence $\Omega_l^o < \Omega_h^o$ (implicit on p. 104).
4. The options contract with share $\lambda \in [0,1]$ gives $\Pi_\theta = \lambda\Omega_\theta$ and the supplier $(1-\lambda)\Omega_\theta$, so it coordinates (pp. 99–100).
5. Under voluntary compliance, $\partial\pi(k_\theta^o, k_\theta^o, \theta)/\partial k < 0$ (p. 100).
6. A capacity $k > 0$ is optimal for the supplier under a wholesale price $w$ iff $w = w_\theta(k)$ (p. 101).
7. A stationary point $k^*$ of $\Pi_\theta$ satisfies $\bar F_\theta(k^*) = \bar F_\theta(k_\theta^o)\bigl(1 + f_\theta(k^*)S_\theta(k^*)/\bar F_\theta(k^*)^2\bigr)$, so $k^* < k_\theta^o$ (p. 102).

Significance

The goal shows that with forced compliance a high-demand manufacturer can share her forecast credibly through the terms of a coordinating contract rather than its form: both types use the same contract family, the supply chain is coordinated in every state, and the only cost of asymmetric information is that the high type may be unable to push the supplier down to his reservation profit. The voluntary-compliance milestones show the other side: once the supplier may under-build, only the wholesale price affects his capacity, and the resulting capacity is strictly below the integrated optimum. Together they explain why compliance regimes matter in capacity contracting.

The results are established on the page with short arguments; none has a machine-checked proof. Formalizing them requires the derivative of expected sales for a distribution with an atom, the first-order characterization of a concave maximizer on a half-line, and careful bookkeeping of the incentive constraints. The demand and profit definitions are reusable for other capacity-procurement and newsvendor-type models.

Difficulty

The incentive constraints look like arithmetic on shares, but the strict inequality $\lambda_l < \hat\lambda_h$ needs $\Omega_l(k_h^o) < \Omega_l^o$: the low type's chain profit at the high type's capacity must be strictly below its optimum. The obvious argument via uniqueness of the maximizer is not available, because the page does not assume $F_\theta$ strictly increasing, so $\Omega_l$ need not be strictly concave and may have a whole interval of maximizers. Likewise $\Omega_l^o < \Omega_h^o$ needs a strict comparison of integrals of distribution functions. In the voluntary-compliance part, the derivative of $w_\theta(k)$ needs the density at $k^*$, and $k^* < k_\theta^o$ fails when that density is $0$.

Formalization scope

Each demand law is a probability measure on $\mathbb R$ and $F_\theta$ is Mathlib's cdf. $F_\theta$ is required to be differentiable only on $(0,\infty)$, because the page's $F_\theta(0) > 0$ makes it jump at $0$. $S_\theta$ is defined by the expectation $x - E[(x - D_\theta)^+]$, whose integrand is integrable because $D_\theta \ge 0$ almost surely. Optimal capacities are passed as arguments characterized as maximizers over $[0,\infty)$, never chosen; $k_\theta^o > 0$ is footnote 46's assumption. Derivatives are HasDerivAt statements.

Hypotheses added relative to the page, all disclosed in the items: $0 < \hat\pi < \Omega_l^o$ and $\Omega_l(k_h^o) > 0$ in the goal (the page divides by $\Omega_l(k_h^o)$ and needs $\lambda_l \in (0,1)$); $\lambda > 0$ for the voluntary-compliance derivative (at $\lambda = 0$ it vanishes); $\bar F_\theta(k^*) > 0$ and $f_\theta(k^*) > 0$ for the non-coordination result. The page's assumption $w''_\theta > 0$ is not needed and not imposed; its strict-concavity claim on p. 101 is not stated, because it would need $F_\theta$ strictly increasing. The prior $\Pr(\theta = h) = \rho$ does not enter any statement. The page's "separating equilibrium" is formalized by its defining incentive and participation conditions, not by a general signalling-game solution concept; a predicate that holds by construction of $\hat\lambda_h$ (for example $\lambda_H \le \hat\lambda_h$) is not an acceptable substitute for the profit inequalities. The fixed-fee condition of p. 105 is pure algebra on four numbers and is not included.

All definitions are local to the namespace CachonCoord.CapacityForecast. No platform theorem formalizes this model; the Snyder–Shen newsvendor definitions (SupplyChainTheory_contracts) and the revenue-sharing model of Cachon–Lariviere 2005 (RevShareCoord.*) concern different games and are not reused. Proofs of any milestone, and a sanity instance showing the model's hypotheses are satisfiable (for example demand with an atom $p_\theta$ at $0$ and an exponential tail, $p_h < p_l$), are welcome.

Selected references

• G. P. Cachon, Supply Chain Coordination with Contracts, in S. Graves and T. de Kok (eds.), Handbooks in Operations Research and Management Science, Vol. 11: Supply Chain Management, North-Holland, 2003, Ch. 6. doi:10.1016/S0927-0507(03)11006-7 (formalized from the author's 3rd draft, January 2003).
• G. P. Cachon and M. A. Lariviere, Contracting to assure supply: how to share demand forecasts in a supply chain, Management Science 47(5), 629–646, 2001. doi:10.1287/mnsc.47.5.629.10486
• R. E. Barlow and F. Proschan, Mathematical Theory of Reliability, Wiley, 1965 (increasing failure rate distributions, cited on p. 102).

Motivation

In most contracts of the supply chain coordination literature the transfer payments are fixed when the contract is signed: a wholesale price $w$, a buy-back rate $b$, a revenue share $\phi$. Some settings need payments that respond to information arriving after signing, such as realized demand at several retailers and realized production output. Fixing the per-unit price in advance then fails twice: for some output realizations the retailers do not buy everything that was produced, and for others they want more than exists, so the supplier must ration, which invites strategic ordering and misallocation (Cachon and Lariviere, 1999).

Section 6.9 of Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, vol. 11, 2003) studies an alternative after Kouvelis and Lariviere (2000): the supplier commits to hold an internal market for output after demand is observed, and pays her own production manager a fixed amount per unit of realized output. The model is a variant of Porteus and Whang (1991), who studied incentives between manufacturing and marketing managers in a firm. The section shows that this pair of mechanisms coordinates both the production decision and the allocation decision without the supplier observing either the demand shocks or the manager's effort.

This mission is part IX of a series formalizing the capstone results of that chapter.

Setting

One supplier employs a production manager and sells to two independent retailers. The constant demand elasticity is $\eta>1$.

1. The manager chooses a production input level $e\ge0$. The output is $Q=Ye$, where $Y\in[0,1]$ is a random variable. The manager incurs the cost $c(e)$, strictly convex and increasing, with derivative $c'$.
2. Retailer $i\in\{1,2\}$ observes the realization $\alpha_i$ of a random variable $A_i>0$.
3. The supplier allocates $q_i$ units to retailer $i$ with $q_1+q_2\le Q$. Retailer $i$ earns revenue $q_ip_i(q_i)$ with the inverse demand $p_i(q_i)=\alpha_iq_i^{-1/\eta}$, that is, $\alpha_iq_i^{(\eta-1)/\eta}$.

If retailer one receives the share $\gamma$ of $Q$, total retailer revenue is

$$\pi(\gamma,\alpha,Q)=\big(\alpha_1\gamma^{(\eta-1)/\eta}+\alpha_2(1-\gamma)^{(\eta-1)/\eta}\big)Q^{(\eta-1)/\eta}.$$

The optimal share is $\gamma^o(\alpha)=\alpha_1^\eta/(\alpha_1^\eta+\alpha_2^\eta)$ (Eq. (44)), and $\pi(\alpha,Q)=\pi(\gamma^o(\alpha),\alpha,Q)$ is revenue under it. The expected supply chain profit is $\Pi(e)=E[\pi(A,Ye)]-c(e)$, and the optimal effort $e^o$ solves the first-order condition (45).

In the decentralized system, if the per-unit price is $w$, retailer $i$'s profit is $\pi_i(q_i,w)=\alpha_iq_i^{(\eta-1)/\eta}-wq_i$. The contingent price is

$$w(\alpha,Q)=\Big(\frac{\eta-1}{\eta}\Big)(\alpha_1^\eta+\alpha_2^\eta)^{1/\eta}Q^{-1/\eta}.$$

The manager is paid a fixed amount per unit of realized output. With $K=E\big[(A_1^\eta+A_2^\eta)^{1/\eta}Y^{(\eta-1)/\eta}\big]$, the payment is

$$\Big(\frac{\eta-1}{\eta}\Big)(e^o)^{-1/\eta}K/E[Y]\qquad(46),$$

and his expected utility is $u(e)=(\text{payment})\cdot E[Ye]-c(e)$.

Formalization targets

Goal

The goal has two parts.

1. For every realization $\alpha_1,\alpha_2>0$ and output $Q>0$, at the price $w(\alpha,Q)$ retailer one's unique optimal order is $\gamma^o(\alpha)Q$ and retailer two's is $(1-\gamma^o(\alpha))Q$. So the retailers order exactly $Q$, the allocation maximizes revenue over all feasible allocations, and

$$\frac{\partial\pi(\alpha,Q)}{\partial Q}=w(\alpha,Q).$$

2. If $e^o>0$ satisfies (45), then under the payment (46) the manager's unique optimal effort is $e^o$. The payment equals $E[Qw(A,Q)\mid e^o]/E[Q\mid e^o]$, and the supplier's expected profit from the market is zero.

Milestones

• (44): revenue is strictly concave in $\gamma$, and $\gamma^o(\alpha)$ is the unique optimal share.
• The closed form $\pi(\alpha,Q)=(\alpha_1^\eta+\alpha_2^\eta)^{1/\eta}Q^{(\eta-1)/\eta}$.
• (45): $\Pi(e)=Ke^{(\eta-1)/\eta}-c(e)$ is strictly concave, and an interior $e^o$ is optimal if and only if $((\eta-1)/\eta)(e^o)^{-1/\eta}K-c'(e^o)=0$.
• The retailers' first-order condition, and the market allocation at $w(\alpha,Q)$.
• $\partial\pi(\alpha,Q)/\partial Q=w(\alpha,Q)$.
• The identity (46).
• The manager's optimal effort and the supplier's zero expected profit.

Significance

The result shows that one mechanism handles two separate information problems. The market price $w(\alpha,Q)$ is the shadow price of output. Charging it makes the retailers' independent orders add up to exactly the output and split it as the integrated firm would, and the supplier never needs to observe $A$. Paying the manager the output-weighted expectation of that shadow price, a single number fixed in advance, aligns his marginal incentive with the supply chain's, and the supplier does not need to observe $e$. The supplier breaks even on the market. Kouvelis and Lariviere (2000) show that in more general settings she breaks even or loses money, so any profit must come from fixed fees. The section therefore illustrates a general design principle: market-based transfer prices inside a firm, combined with linear output-based pay.

The derivations are short calculus on the page. Formalizing them pins down what the page leaves implicit: the range of efforts and allocations; the role of $E[Y]>0$ and of the integrability of the shock; the fact that each retailer's problem has a unique interior optimum only at a positive price; and how the realized output $Q=0$ enters the expectation $E[Qw(A,Q)]$. To our knowledge none of these statements has been machine-checked before.

Difficulty

The deterministic part requires real-power calculus with a non-integer exponent $(\eta-1)/\eta\in(0,1)$. Strict concavity of $\gamma\mapsto\gamma^{(\eta-1)/\eta}$ has to be used on the closed interval $[0,1]$, where the derivative blows up at the endpoints. The retailer's optimum has to be shown to be interior even though the profit at $q=0$ is defined.

The stochastic part requires pulling the effort out of the expectation, $E[\pi(A,Ye)]=Ke^{(\eta-1)/\eta}$, pointwise in the shock, including at realizations with $Y=0$. The natural first idea, to differentiate under the expectation sign, is unnecessary but tempting. The obstacle it hides is that $w(\alpha,Ye)$ is undefined where $Y=0$, so the identity (46) only holds once $Qw(A,Q)$ is read as its limit $0$ at $Q=0$. Uniqueness of the manager's optimum depends on strict convexity of $c$ alone, since his payment is linear in $e$.

Formalization scope

All objects live in the namespace CachonCoord.InternalMarket. The deterministic file Revenue defines $\pi(\gamma,\alpha,Q)$, $\gamma^o(\alpha)$ (as the printed formula, not as an argmax), $\pi(\alpha,Q)$, $\pi_i(q_i,w)$ and $w(\alpha,Q)$ with real powers (Real.rpow). The file Model bundles a probability space with measurable $A_1,A_2>0$ and $Y\in[0,1]$, the elasticity $\eta>1$, and the cost $c$. The cost is strictly convex and increasing on $[0,\infty)$ and has derivative $c'$ at every $e>0$. On top of these, Model defines $\Pi$, $K$, the payment (46) (by its printed left side, not as the ratio it is claimed to equal), expected output and market revenue, and the manager's utility (from the payment scheme, not by the printed formula). Derivatives are HasDerivAt statements and optima are IsMaxOn over $[0,1]$ or $[0,\infty)$.

The standing assumptions are those of the model paragraph on p. 92: risk neutrality and the distributional assumptions above. Added hypotheses, each disclosed in the item's Formalization Note:

• $E[Y]>0$, because (46) divides by it.
• Integrability of $(A_1^\eta+A_2^\eta)^{1/\eta}Y^{(\eta-1)/\eta}$.
• A positive price in the retailer's first-order condition.
• Differentiability of $c$ only on $(0,\infty)$.

The existence of an effort satisfying (45) is a hypothesis, as on the page. Clauses 1 of the goal are stated for fixed realizations, not as random variables.

A trivializing formalization would define $\gamma^o(\alpha)$ as an argmax, or define the payment (46) as $E[Qw]/E[Q]$; neither is done here. Outside $\gamma\in[0,1]$ and $Q>0$, Lean's real power returns junk values, and every statement restricts to that range. The companion claim that $w(\alpha,Q)$ is the unique market-clearing price is not posed.

The formalization needs no infrastructure beyond Mathlib's real powers, convexity and Bochner integral. The concavity and first-order-condition lemmas for $x\mapsto ax^{r}-bx$ with $0<r<1$ may be reused for other constant-elasticity models. Contributions are welcome at any milestone; each is independent of the others except through the closed forms.

Selected references

• G. P. Cachon, Supply Chain Coordination with Contracts, in S. Graves and T. de Kok (eds.), Handbooks in Operations Research and Management Science, Vol. 11: Supply Chain Management, North-Holland, 2003, Ch. 6, §6.9. https://doi.org/10.1016/S0927-0507(03)11006-7 (formalized from the author's 3rd draft, January 2003).
• P. Kouvelis and M. A. Lariviere, Decentralizing cross-functional decisions: Coordination through internal markets, Management Science 46(8), 2000, 1049–1058. https://doi.org/10.1287/mnsc.46.8.1049.12025
• E. L. Porteus and S. Whang, On manufacturing/marketing incentives, Management Science 37(9), 1991, 1166–1181. https://doi.org/10.1287/mnsc.37.9.1166
• G. P. Cachon and M. A. Lariviere, Capacity choice and allocation: strategic behavior and supply chain performance, Management Science 45(8), 1999, 1091–1108. https://doi.org/10.1287/mnsc.45.8.1091