Algorithmic Game Theory

Motivation

Banks lend to one another, and the shape of the resulting network decides how a loss at one bank reaches the others. A long line of work, starting with Allen and Gale (2000) and continued by Acemoglu, Ozdaglar and Tahbaz-Salehi (2015), compares the ring network, where each bank is owed money by one neighbour, with the complete network, where every bank holds an equal share of every other bank's debt. That literature studies contagion after shocks hit and finds that the complete network spreads losses thinly and can absorb small shocks better.

Shu's paper (Management Science, doi:10.1287/mnsc.2022.01519) asks the ex-ante question: when banks choose how much risk to take, knowing the network they sit in, which network makes them take more? A successful bank subsidizes its failed counterparties through the clearing of interbank debt, and anticipating that subsidy pushes it toward riskier projects. Proposition 4 of the paper says that this effect is stronger in the complete network. This mission formalizes that proposition and the computation behind it.

Setting

There are $N\ge2$ banks. In a regular network with share matrix $\Theta=[\theta_{ij}]$, bank $j$ owes bank $i$ the face value $\theta_{ij}\bar d$, every bank has total interbank liability $\bar d>0$, and every bank also owes a senior deposit $v>0$. The two networks of Definition 3 are

$$\Theta^R:\ \theta_{ij}=1 \text{ iff } j\equiv i-1 \pmod N,\qquad \Theta^C=\tfrac{1}{N-1}\big(\mathbb 1_{N,N}-I_N\big).$$

Each bank $i$ chooses a project $Z_i$ in a common interval $[\underline Z,\overline Z]$. The project pays $Z_i$ with probability $P(Z_i)$ and $0$ otherwise, independently across banks. Assumption 1 requires $P(Z)\in(0,1)$, $P$ decreasing, and $P(Z)\,Z$ concave. The standing assumption $\underline Z\ge v+\bar d$ says a successful bank never defaults.

After the state $\omega\in\{s,f\}^N$ is realized, interbank payments clear. A payment equilibrium is a vector $d$ with

$$d_i=\Big\{\min\Big[\textstyle\sum_j\theta_{ij}d_j+e_i-v,\ \bar d\Big]\Big\}^+,$$

where $e_i=Z_i$ if bank $i$ succeeds and $0$ if it fails. Bank $i$'s profit is $\big(\sum_j\theta_{ij}d^*_j+e_i-v-d^*_i\big)^+$. A risk-taking equilibrium is a profile $Z^*$ in which each $Z^*_i$ maximizes bank $i$'s expected profit given $Z^*_{-i}$. Equilibria need not be unique, and the paper selects the least one.

The key quantity is the network risk-taking distortion

$$\mathcal D_i(Z_{-i})=\sum_{\omega_{-i}}\Big(\bar d-\sum_j\theta_{ij}d^*_j(\omega^{i=s})\Big)\Pr(\omega_{-i}),$$

which is bank $i$'s expected net interbank payment to the other banks when its own project succeeds. In a regular network, expected profit equals $P(Z_i)(Z_i-v)-P(Z_i)\,\mathcal D_i(Z_{-i})$, so $\mathcal D_i$ acts like extra debt that the bank repays only when it succeeds. Superscripts $C$ and $R$ mark the complete and ring networks.

Formalization targets

Goal: Proposition 4

With $Z^C$ the least equilibrium of the complete network and $Z^R$ the least equilibrium of the ring,

$$Z^R_i\le Z^C_i\qquad\text{for every bank } i.$$

Milestones

1. Clearing in the complete network (IA p. 15): a failed bank pays $\big(\bar d-\frac{N-1}{S}v\big)^+$, where $S$ is the number of successful banks.
2. (I.13): with $q$ the common success probability of the other banks and $\Pr(m)=\binom{N-1}{m}(1-q)^mq^{N-1-m}$,

$$\mathcal D^C_i=\sum_{m=1}^{N-1}\min\Big(\frac{mv}{N-m},\frac{m\bar d}{N-1}\Big)\Pr(m).$$

3. (I.14): in the ring, a failed bank pays $(\bar d-K_iv)^+$, where $K_i$ counts the consecutive failed banks upstream of $i$, starting with $i$ itself.
4. (I.15): the conditional distribution, given $m$ failures, of what a successful bank receives in the ring.
5. Closed form of $\mathcal D^R_i$ (IA p. 16, also p. 14).
6. Lemma I.A (ii): $\sum_{l=r}^n\binom lr(n-l)=\binom{n+1}{r+1}\frac{n-r}{r+2}$. Part (i), the classical hockey-stick identity, is already published and proved on the platform and is included by reference.
7. Lemma I.B: $\sum_i A_i^+\ge(\sum_iA_i-B)^++B$ whenever $B<\max_iA_i$.
8. $\mathcal D^R_i\le\mathcal D^C_i$ when all other banks choose the same project.

Significance

The result. Proposition 4 reverses the conventional reading of the complete network as the safer structure. The co-insurance that makes it resilient after a shock is the same cross-subsidy that weakens incentives before the shock. Two networks with the same face-value liabilities $\bar d+v$ therefore induce different equilibrium risk-taking. Liabilities alone are not a sufficient statistic for risk incentives, and the network topology matters in its own right. The same comparison is the template for the paper's later results on the number of banks and on central clearing.

Formalizing it. The proposition is proved in the paper, not open, and none of it is machine-checked yet. A formal proof must establish the two clearing vectors, the counting identity behind (I.15), and the two closed forms of the distortion. The printed argument also leaves a step to be supplied: its final appeal to "the monotone selection theorem" needs the distortion comparison at every profile of the other banks. It is proved only when they all choose the same project, and it is false in general. The goal is nevertheless stated for least equilibria exactly as in the paper, and its formal proof has to bridge that gap. The milestones are true as stated.

Difficulty

The distortion of the ring is not a function of the number of failures alone. What a successful bank receives depends on the length of the run of failed banks immediately upstream of it, so the closed form needs an exact count of the binary strings with a given number of failures and a given initial run length. The comparison of the two distortions is not termwise either: the positive part sits inside a sum on the ring side and outside it on the complete side.

The obvious final step is to say that the distortion is larger in the complete network, and that a larger distortion raises the optimal risk exposure. That step does not go through as stated. The equilibrium comparison needs control of the best-response maps at every profile, while the distortion comparison holds only on the diagonal, where all other banks choose the same project. Some further structure of the two games is needed to restrict attention to that diagonal.

Formalization scope

Banks are Fin N with $N\ge2$, and states are Fin N → Bool with true meaning success. The paper's general model is specialized to a regular network given by $(\Theta,\bar d,v)$, which covers both networks of Definition 3. Every expectation is a finite sum over the $2^N$ states, so no measure theory is involved. The payment equilibrium $d^*$ is the greatest solution of the clearing system, because the paper asserts only generic uniqueness. Every bank's project lies in $[\underline Z,\overline Z]$, and $\underline Z\ge v+\bar d$ is a hypothesis of every statement.

The distortion milestones (2, 5 and 8) are stated at the constant profile in which every bank chooses the same $z$, which is how the page's single $P(Z_{-i})$ reads. At $m=N-1$, where every other bank fails, the printed ring binomial has lower index $-1$, and the weight is fixed explicitly to $1$ at $l=N-1$. Proposition 4 is stated for least equilibria and weak inequality. It adds one hypothesis the page does not state, continuity of $P$ on $[\underline Z,\overline Z]$, so that best responses and least equilibria exist. Without it the IsLeast hypotheses could be unsatisfiable and the goal vacuous.

Trivializing encodings are ruled out: $d^*$ is an actual solution of the clearing system, not a junk supremum, and the run length $K_i$ is only used in states where some bank succeeds.

A complete development needs Knaster–Tarski on the box $[0,\bar d]^N$, the clearing computations for the two networks, binomial identities, and a monotone comparative statics argument for the equilibria. Published Topkis results on supermodular games (existence of least equilibria, and monotonicity of least fixed points in a parameter) are included by reference as tools. The clearing and counting lemmas are reusable for the paper's other results on ring and complete networks. Proofs of any milestone, and of the goal, are welcome.

Not posed here: Proposition 1 (strategic complementarity in any network, a separate mission), Proposition 2 (existence), and the later comparative statics in the number of banks, central clearing and bailouts.

Selected references

• C. Shu, Endogenous Risk Exposure and Systemic Instability, Management Science (accepted manuscript, 17 Sep 2024). https://doi.org/10.1287/mnsc.2022.01519
• F. Allen and D. Gale, Financial Contagion, Journal of Political Economy 108(1), 2000. https://doi.org/10.1086/262109
• D. Acemoglu, A. Ozdaglar and A. Tahbaz-Salehi, Systemic Risk and Stability in Financial Networks, American Economic Review 105(2), 2015. https://doi.org/10.1257/aer.20130456
• L. Eisenberg and T. H. Noe, Systemic Risk in Financial Systems, Management Science 47(2), 2001. https://doi.org/10.1287/mnsc.47.2.236.9835
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539

Motivation

When many independent users share a network, each routes its own traffic to minimize its own delay, and nobody optimizes the system as a whole. Koutsoupias and Papadimitriou asked how much this lack of coordination can cost: how far the social cost of a Nash equilibrium can be from the social optimum, in the worst case. Their paper Worst-case equilibria (STACS 1999; journal version 2009, doi:10.1016/j.cosrev.2009.04.003) introduced this ratio, later named the price of anarchy, and studied it on the simplest network: parallel links between one source and one destination. The ratio has since become a standard measure of the inefficiency of equilibria in routing, scheduling and auctions (see Chapters 17–20 of Nisan, Roughgarden, Tardos and Vazirani, Algorithmic Game Theory, 2007).

Most of the paper concerns links of equal capacity. Its last result, Theorem 4, turns to two links of different speeds and shows that unequal speeds make equilibria worse: the worst-case ratio rises from $3/2$ for two identical links to the golden ratio $\varphi=(1+\sqrt5)/2\approx1.618$.

Timeline. 1999: Koutsoupias and Papadimitriou define the coordination ratio; for two identical links they prove it is exactly $3/2$, and for two links with speeds they give the golden-ratio lower bound of Theorem 4. 2002–2003: Mavronicolas and Spirakis, Koutsoupias, Mavronicolas and Spirakis, and Czumaj and Vöcking determine the asymptotic order of the price of anarchy for $m$ identical and for $m$ related links (Czumaj–Vöcking, ACM TALG 2007).

Setting

There are $n$ agents and $m$ parallel links. Agent $i$ has an amount of traffic $w_i>0$, and link $j$ has a speed $s_j>0$. A pure profile $a=(a_1,\dots,a_n)$ sends each agent's whole traffic over one link $a_i$. The load of link $j$ is $L_j(a)=\sum_{k:\,a_k=j}w_k$, and an agent on link $j$ experiences the delay $L_j(a)/s_j$.

A mixed strategy of agent $i$ is a probability distribution $(p_i^1,\dots,p_i^m)$ over the links; the agents randomize independently. The expected cost of agent $i$ is its expected delay. A profile $p$ is a Nash equilibrium if no agent can lower its expected cost by changing its own distribution. The expected traffic on link $j$ is $M^j=\sum_i p_i^jw_i$, and the cost to agent $i$ of placing its traffic on link $j$ is

$$c_i^j=\frac{M^j+(1-p_i^j)\,w_i}{s_j}. \tag{8}$$

The social cost of $p$ is the expected makespan, the expected maximum delay over the links,

$$\operatorname{cost}(p)=\sum_a\Big(\prod_i p_i^{a_i}\Big)\max_j\frac{L_j(a)}{s_j},$$

and $\operatorname{opt}=\min_a\max_j L_j(a)/s_j$ is the optimal makespan over pure assignments. The price of anarchy is the largest ratio $\operatorname{cost}(p)/\operatorname{opt}$ over instances and equilibria.

Formalization targets

Goal: Theorem 4 (PDF p. 6)

For two links with speeds $0<s_1\le s_2\le\varphi s_1$, there is an instance with positive traffic and a Nash equilibrium $p$ with $\operatorname{opt}>0$ and

$$\operatorname{cost}(p)=R\cdot\operatorname{opt},\qquad R=1+\frac{s_2}{s_1+s_2};$$

moreover $R\le\varphi$ on this range, and $R=\varphi$ when $s_2=\varphi s_1$.

Milestones

1. (8): the expected delay of a pure deviation is $c_i^j=(M^j+(1-p_i^j)w_i)/s_j$.
2. Support property (§2, applied with speeds): at an equilibrium each agent puts positive probability only on links minimizing $c_i^j$, and its expected cost is $c_i=\min_jc_i^j$.
3. For $s_1\le s_2$, the probabilities $p_1^1=s_1^2/(s_2(s_1+s_2))$ and $p_2^1=1-s_2^2/(s_1(s_1+s_2))$ lie in $[0,1]$ if and only if $s_2\le\varphi s_1$.
4. With $w_1=s_2$, $w_2=s_1$, this profile is a Nash equilibrium.
5. Its social cost is $(s_1+2s_2)/(s_1+s_2)$.
6. The instance has $\operatorname{opt}=1$.
7. $R\le\varphi$, with equality at $s_2/s_1=\varphi$.

Significance

The result. Theorem 4 shows that the price of anarchy of parallel links depends on the heterogeneity of the links, not only on their number: two identical links have price of anarchy $3/2$ (Theorems 1 and 3 of the paper), while two links of different speeds already reach $\varphi$. The setting is that of related (uniformly related) machines, the model in which Czumaj and Vöcking later proved the asymptotic order of the price of anarchy for $m$ links.

Formalizing it. The result is proved on paper; this mission produces a machine-checked proof. Beyond the theorem, it yields reusable statements about mixed equilibria of load-balancing games on the published agt_games vocabulary: the closed form (8) of a pure deviation's expected cost and the support characterization of equilibria, both stated for any number of agents and links. A search of the Prove2Me catalog (October 2026) found no formalization of any part of this result.

Difficulty

The arithmetic of the instance is elementary, so the work lies in connecting the paper's computations to the definitions. The paper's notion of equilibrium quantifies over all mixed deviations, and its expected costs are sums over all $m^n$ pure profiles; the proof reasons instead with the per-link costs $c_i^j$ of (8) and the indifference of each agent between the links it uses. Turning that into a proof requires showing that an agent's expected cost is the $p_i$-weighted average of the $c_i^j$ (linearity over independent randomization) and that the average over $2^2$ outcomes reduces to the paper's four-term formula. A naive approach that checks only pure deviations does not give the equilibrium property directly; one must pass from pure to mixed deviations. The restriction $s_2\le\varphi s_1$ is not cosmetic: beyond it the second agent's probability is negative.

Formalization scope

The game is defined in WorstCaseEq.Speeds.Model on top of the published agt_games definitions (AGT.IsMixedNash, AGT.expectedPayoff, AGT.profileProb). These maximize payoffs, so an agent's payoff is minus its delay. Agents and links are Fin n and Fin m, indexed from $0$, so the paper's links 1, 2 and agents 1, 2 are 0, 1. A mixed profile is a real matrix p i j; being a family of probability distributions is part of the Nash condition. Makespan, social cost and opt require at least one link (NeZero m).

The paper does not print the social cost for links with speeds; the computation in the proof of Theorem 4 uses the expected maximum of load divided by speed, and that is the definition. It is not the maximum of the expected loads, a smaller quantity. The page numbers cited are PDF page indices of the journal version (dated April 29, 2009), which prints no page numbers after page 1.

"The price of anarchy is at least $R$" is formalized as the existence of an instance and an equilibrium whose social cost equals $R$ times a positive optimum. A quotient $\operatorname{cost}/\operatorname{opt}$ is avoided because it takes the junk value $0$ when $\operatorname{opt}=0$, and the requirement $\operatorname{opt}>0$ rules out degenerate witnesses with no traffic. The ratio conditions $s_2/s_1\le\varphi$ and $s_2/s_1=\varphi$ are written $s_2\le\varphi s_1$ and $s_2=\varphi s_1$ (equivalent since $s_1>0$), and $\varphi$ is Mathlib's Real.goldenRatio.

Contributions welcome: proofs of any milestone. Milestones 1 and 2 are general facts about mixed equilibria of weighted load-balancing games and are reusable beyond this mission.

Selected references

• E. Koutsoupias and C. Papadimitriou, Worst-case equilibria, STACS 1999, LNCS 1563, pp. 404–413, doi:10.1007/3-540-49116-3_38; journal version, Computer Science Review 3(2), 2009, pp. 65–69, doi:10.1016/j.cosrev.2009.04.003.
• A. Czumaj and B. Vöcking, Tight bounds for worst-case equilibria, ACM Transactions on Algorithms 3(1), 2007, doi:10.1145/1186810.1186814.
• N. Nisan, T. Roughgarden, É. Tardos and V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Chapter 20, doi:10.1017/CBO9780511800481.

Motivation

Mobile devices run applications whose computational load can exceed what the device itself can serve in reasonable time and with reasonable battery drain. Computation offloading sends part of that load elsewhere: to a cloudlet, a small cluster of servers one wireless hop away, or to a distant cloud reached through the wide-area network. The cloudlet is shared, so its response time depends on how much load all users send to it, and each user's best offloading decision depends on everybody else's. Cardellini, De Nitto Personé, Di Valerio, Facchinei, Grassi, Lo Presti and Piccialli (Math. Program., 2016, DOI 10.1007/s10107-015-0881-6) model this as a non-cooperative game between users and study it with the tools of variational inequalities.

The game is a generalized Nash equilibrium problem (GNEP): not only the costs but also the feasible sets of the players depend on the other players' choices, because all users share one capacity constraint on the cloudlet. GNEPs with a shared convex constraint (jointly convex games) can be reduced to a single variational inequality, a reduction the paper takes from Facchinei, Fischer and Piccialli (Oper. Res. Lett. 2007, DOI 10.1016/j.orl.2006.03.004); Facchinei and Kanzow survey the area (Ann. Oper. Res. 2010, DOI 10.1007/s10479-009-0653-x). This mission formalizes the first step of the paper's analysis: the game has an equilibrium.

Setting

There are $N$ users $u=1,\dots,N$ and three tiers $I=\{m,\mathrm{clet},\mathrm{cloud}\}$ (mobile device, cloudlet, cloud). User $u$ chooses the fractions $x_u=(x_{u,m},x_{u,\mathrm{clet}},x_{u,\mathrm{cloud}})$ of its tasks run on each tier. A profile is $x=(x_1,\dots,x_N)\in\mathbb R^{3N}$.

The data are reals $\alpha_u,\beta_u,\gamma_u,\delta_u$ (arrival rates divided by service or transfer rates), powers $P_{u,m},P_{u,t},P_{u,\max}$, the number $n\ge1$ of cloudlet servers, the offloadable fraction $\chi\in(0,1]$ and a utilisation cap $U_{\max}$. Assumption A requires $U_{\max}$ and every $\alpha_u,\delta_u$ to lie in $(0,1)$.

User $u$'s private feasible set is

$$\tilde K_u=\Big\{x_u\in\mathbb R^3_+:\ \textstyle\sum_{i\in I}x_{u,i}=1,\ x_{u,\mathrm{clet}}+x_{u,\mathrm{cloud}}\le\chi,\ \alpha_uP_{u,m}x_{u,m}+\beta_uP_{u,t}(x_{u,\mathrm{clet}}+x_{u,\mathrm{cloud}})\le P_{u,\max}\Big\},$$

the shared constraint is $\Omega=\{x:\frac1n\sum_v\delta_vx_{v,\mathrm{clet}}\le U_{\max}\}$, and the joint feasible set is $K=\big(\prod_u\tilde K_u\big)\cap\Omega$. User $u$ minimises the mean response cost

$$\lambda_uR_u(x_u,x_{-u})=\frac{\alpha_ux_{u,m}}{1-\alpha_ux_{u,m}}+\beta_ux_{u,\mathrm{clet}}+\gamma_ux_{u,\mathrm{cloud}}+\frac{\delta_ux_{u,\mathrm{clet}}}{1-\frac1n\sum_v\delta_vx_{v,\mathrm{clet}}}$$

over $\{y\in\tilde K_u:(y,x_{-u})\in\Omega\}$. A solution of the GNEP is a profile $\bar x\in K$ at which no user can lower its cost by a deviation that keeps the shared constraint satisfied.

The map $F:\mathbb R^{3N}\to\mathbb R^{3N}$ stacks the users' partial gradients,

$$F(x)_u=\Big(\frac{\alpha_u}{(1-\alpha_ux_{u,m})^2},\ \beta_u+\delta_u\frac{1-\frac1n\sum_{v\ne u}\delta_vx_{v,\mathrm{clet}}}{\big(1-\frac1n\sum_v\delta_vx_{v,\mathrm{clet}}\big)^2},\ \gamma_u\Big),$$

and $\bar x$ solves the variational inequality $\mathrm{VI}(K,F)$ if $\bar x\in K$ and $F(\bar x)^\top(x-\bar x)\ge0$ for all $x\in K$. Such solutions are the variational (or normalized) solutions of the game.

Formalization targets

Goal: Proposition 1 (p. 12)

Under Assumption A, and provided every $\tilde K_u$ is nonempty,

$$\exists\,\bar x\in K\ \ \forall u\ \ \forall y\in\tilde K_u\ \text{with}\ (y,\bar x_{-u})\in\Omega:\quad \lambda_uR_u(\bar x_u,\bar x_{-u})\le\lambda_uR_u(y,\bar x_{-u}).$$

Milestones

1. $F(x)_u=\nabla_{x_u}\lambda_uR_u(x)$ wherever both denominators are positive (p. 11).
2. For fixed $x_{-u}$, user $u$'s feasible set is convex and its cost is convex on it (p. 11).
3. Every solution of $\mathrm{VI}(K,F)$ is a solution of the GNEP (proof of Proposition 1).
4. $F$ is continuous on $K$, and $K$ is compact and convex (proof of Proposition 1).
5. $\mathrm{VI}(K,F)$ has a solution (proof of Proposition 1, citing Facchinei–Pang, Corollary 2.2.5).

Milestones 3 and 5 give the goal; milestones 1 and 2 are what milestone 3 rests on, and milestone 4 is what milestone 5 rests on. The platform's Proved statement of Brouwer's fixed-point theorem (AGT.brouwer_fixed_point) is included as a reference item for milestone 5.

Significance

The result. Existence of an equilibrium is the precondition for everything else in the paper: the monotonicity of $F$ (Theorem 1), the reformulation with a cloudlet price as an extended game (Theorem 2), and the distributed algorithm whose convergence is Theorem 3. Proposition 1 also shows that variational solutions exist, which is the specific equilibrium the paper's algorithm computes.

Formalizing it. The result is proved in the paper, in three lines that cite two textbook theorems. The work here is to make those citations machine-checked for this concrete model: that the closed-form $F$ is indeed the stacked partial gradient, that each user's problem is convex despite the rational cost terms, that the VI-to-GNEP reduction holds, and that a VI on a compact convex set with continuous map has a solution. None of these steps is formalized in Mathlib for GNEPs; the last is a finite-dimensional Hartman–Stampacchia theorem, which Mathlib does not contain. No part of this paper has a machine-checked proof.

Difficulty

The obvious argument is to apply Kakutani's theorem to the best-response correspondence. With a shared constraint this needs lower semicontinuity of the feasible-set map $x_{-u}\mapsto\{y\in\tilde K_u:(y,x_{-u})\in\Omega\}$, which is a separate argument, and Kakutani is not in Mathlib either. The VI route avoids it but has its own points. The cost has the rational terms $\alpha_ux_{u,m}/(1-\alpha_ux_{u,m})$ and $\delta_ux_{u,\mathrm{clet}}/D(x)$, and convexity and differentiability must be checked on the region where the denominators are positive; on a user's feasible set this needs Assumption A and the shared constraint, not the private constraints alone. The existence of a VI solution needs a fixed-point theorem on a compact convex set, and Mathlib has no Brouwer theorem. That is why the platform's statement of it is attached to this mission.

Formalization scope

Users are Fin N (0-based) and tiers an inductive type Tier with three constructors; a profile is Fin N → Tier → ℝ. The inner product $a^\top b$ is the coordinatewise double sum (not Mathlib's sup norm on Pi types). The cost and $F$ are the paper's closed forms; $F$ is not defined as a derivative, so milestone 1 has content. Lean's $x/0=0$ makes both formulas junk where a denominator vanishes. Under Assumption A both denominators are positive on $K$ and at every point the GNEP definition compares, and milestone 1 assumes the two positivity conditions explicitly.

Standing hypotheses in every statement: Assumption A, $n\ge1$, $0<\chi\le1$. Nothing is assumed of $\beta_u,\gamma_u$ or the powers, as in the paper. Added hypothesis: every $\tilde K_u$ is nonempty, in the goal and in milestone 5. The printed proposition is false without it: if $0<P_{u,\max}<\min(\alpha_uP_{u,m},\beta_uP_{u,t})$ then $\tilde K_u=\emptyset$, so $K=\emptyset$. The condition is equivalent to $K\ne\emptyset$. Milestone 4 adds convexity of $K$ to the paper's "continuous and compact".

Trivializing formalizations are ruled out: $K$ cannot be empty under the added hypothesis, $F$ is not a derivative by definition, no statement evaluates the cost at a point with a vanishing denominator, and the GNEP keeps the shared constraint in each player's feasible set (dropping it gives a different game, a NEP).

Contributions welcome: a finite-dimensional Hartman–Stampacchia theorem (reusable well beyond this mission), the general VI-implies-GNEP reduction for jointly convex games, and proofs of the model-specific milestones.

Selected references

• V. Cardellini, V. De Nitto Personé, V. Di Valerio, F. Facchinei, V. Grassi, F. Lo Presti, V. Piccialli, A game-theoretic approach to computation offloading in mobile cloud computing, Mathematical Programming (2016). https://doi.org/10.1007/s10107-015-0881-6 (accepted manuscript: IRIS Sapienza, handle 11573/779661)
• F. Facchinei, A. Fischer, V. Piccialli, On generalized Nash games and variational inequalities, Operations Research Letters 35 (2007). https://doi.org/10.1016/j.orl.2006.03.004
• F. Facchinei, C. Kanzow, Generalized Nash equilibrium problems, Annals of Operations Research 175 (2010). https://doi.org/10.1007/s10479-009-0653-x
• F. Facchinei, J.-S. Pang, Finite-Dimensional Variational Inequalities and Complementarity Problems, Springer, 2003. https://doi.org/10.1007/b97543

Motivation

Retailers in many categories accept returns of products that are not defective: a consumer buys, learns whether the product suits them, and may send it back for a refund. Returns of this kind are a large cost item in retailing, and the refund a retailer offers is an operational decision on a par with its price and its stocking quantity. Xuanming Su, Consumer Returns Policies and Supply Chain Performance (SSRN 1020451, version of August 2008; published in Manufacturing & Service Operations Management 11(4), 2009, doi:10.1287/msom.1080.0240), studies this decision first for a single seller and then in a supply chain.

This mission formalizes the supply chain part, Section 5 of the paper. A classical result of supply chain contracting is that a manufacturer can align a retailer's ordering decision with the interest of the whole chain by a buy-back contract, which pays the retailer a credit for unsold units (Cachon, Supply Chain Coordination with Contracts, 2003). Su shows that once the retailer also sets a consumer returns policy, the standard buy-back no longer coordinates, and identifies three contracts that do. The companion mission (mission 1 of this series) formalizes the single-seller results of Sections 3–4, in particular Proposition 2, which gives the supply chain optimum used here.

Setting

A consumer who buys at price $p$ learns a valuation $V$, drawn independently from a law $\nu$ with finite mean $\mu = EV$, and then either keeps the product or returns it for the refund $r$. Keeping is optimal when $V \ge r$. Write

$$\bar G(r) = \mathbb P(V \ge r), \qquad G(r) = \mathbb P(V < r),$$

for the probabilities of keeping and returning. A consumer's expected utility from buying is $E\max(V,r)$, which is therefore the reservation price: all consumers buy if $p \le E\max(V,r)$ and none buys otherwise (the demand rule (6)). Market demand $X \ge 0$ has distribution function $F$ and $\bar F = 1 - F$; a stock $q \ge 0$ sells $E\min(X,q)$ in expectation when consumers buy, and nothing when they do not. Write $S(p,q,r)$ for these expected sales. The production cost is $c$, leftover and returned units are salvaged at $s$, and $0 \le s < c < \mu$.

The total supply chain profit is

$$\Pi_T(p,q,r) = [(p-s)\bar G(r) + (p-r)G(r)]\,S(p,q,r) - (c-s)q. \tag{15}$$

A manufacturer sells to a retailer, who sets $p$, $q$ and (except in Proposition 4) $r$. The contracts are:

• standard buy-back $(w,b)$: wholesale price $w$, credit $b$ per leftover unit; the retailer earns (14);
• differentiated buy-back $(w,b,l)$: credit $b$ per unsold unit and $b-l$ per returned unit; the retailer earns

$$\Pi_R(p,q,r) = [(p-b)\bar G(r) + (p-r-l)G(r)]\,S(p,q,r) - (w-b)q; \tag{31}$$

• direct-to-manufacturer returns with a buy-back $(w,b)$: consumers return to the manufacturer, who sets $r$; the profits are (19) and (21);
• sales rebate $(w,u)$: a rebate $u$ per unit sold, returned or not; the retailer earns (25).

The supply chain optimum, from Proposition 2 of the paper, is

$$p^{SC} = E\max(V,s), \qquad \bar F(q^{SC}) = \frac{c-s}{E\max(V,s)-s}, \qquad r^{SC} = s.$$

Formalization targets

Goal: Proposition 3 (p. 16)

For $\phi \in [0,1]$ and $\bar\phi = 1-\phi$, the differentiated buy-back

$$w = \phi c + \bar\phi\,E\max(V,s), \qquad b = \phi s + \bar\phi\,E\max(V,s), \qquad b - l = s$$

makes the supply chain optimum a retailer optimum and gives the retailer the share $\phi$:

$$\Pi_R(p,q,r) \le \Pi_R(p^{SC},q^{SC},r^{SC}) \ \ \forall p, r,\ q \ge 0, \qquad \Pi_R(p^{SC},q^{SC},r^{SC}) = \phi\,\Pi_T(p^{SC},q^{SC},r^{SC}),$$

and the contract is implementable: $w \ge b$, $l \ge 0$, $b - l \ge s$.

Milestones

1. Under a standard buy-back the retailer's optimal refund is $r^* = b$ (Sec. 5.1, p. 15).
2. Under (31) the retailer's optimum is $p^* = E\max(V,b-l)$, $\bar F(q^*) = (w-b)/(E\max(V,b-l)-b)$, $r^* = b-l$ (proof of Proposition 3, p. 27).
3. Under (16)–(18), $w - b = \phi(c-s)$ and $E\max(V,b-l) - b = \phi[E\max(V,s)-s]$ ((32)–(33)).
4. At $(E\max(V,s), q, s)$ the retailer earns $\phi\,\Pi_T$ ((34)–(39)).
5. Retailer plus manufacturer profit under direct returns is $\Pi_T$ (Sec. 5.3, p. 17).
6. Proposition 4: with direct-to-manufacturer returns and the buy-back (22)–(23), the chain optimum is a Nash equilibrium between retailer and manufacturer, with retailer share $\phi$.
7. Proposition 5: the sales rebate $u = \frac{E\max(V,s)-s}{c-s}(w-c)$ makes the chain optimum a retailer optimum.
8. With a rebate paid on kept units only, the retailer's optimal refund is $r^* = s - u < s$ (Sec. 5.4, p. 19).

Significance

The results separate what a contract must observe in order to coordinate a chain with consumer returns: either the manufacturer distinguishes returned from unsold units (Propositions 3 and 4), or it observes sales (Proposition 5). The negative results (milestones 1 and 8) show why the standard buy-back and a kept-only rebate fail: each distorts the retailer's refund away from the salvage value. These statements are proved in the paper by short arguments; none of them has, to the knowledge of this mission, a machine-checked proof. Formalizing them yields a reusable model of a newsvendor with an endogenous price and refund under valuation uncertainty, and a checked account of the coordination conditions, including the boundary cases ($\phi = 0$, atoms in the valuation law) that the paper does not discuss.

Difficulty

Each result combines two optimizations, and neither is routine at the generality of the formal statements. The first is over price and refund jointly: the demand rule makes every profit discontinuous in $p$ and $r$, and the refund problem must be solved for an arbitrary valuation law, where atoms make the tie rule at $V = r$ matter. The second is a newsvendor problem in $q$ for an arbitrary demand law: the paper writes the optimal stock as $\bar F^{-1}$ of a fractile, which presumes a continuous, strictly increasing $F$, whereas here $F$ may jump or be flat and the optimal stock is any solution of the fractile equation. The obvious reduction, "the retailer's profit is $\phi\,\Pi_T$, so its maximizer is the chain's", is not available: that identity holds only at the chain's price and refund, and away from them the retailer's profit is not proportional to $\Pi_T$. In Proposition 4 the manufacturer's deviation to a refund below $s$ acts on the consumers' purchase decision, and the paper's remark that no one then buys is false when $V \ge s$ almost surely, so that case needs its own argument.

Formalization scope

Prices, refunds, costs, quantities and profits are real numbers. The valuation law $\nu$ is a probability measure on $\mathbb R$ with integrable identity (a strict generalization of the paper's density $g$); $\bar G(r) = \nu([r,\infty))$ and $G(r) = \nu((-\infty,r))$, matching the rule "keep iff $V \ge r$". The demand law $D$ is a probability measure on $\mathbb R$ with $D((-\infty,0)) = 0$, and $E\min(X,q)$ is SupplyChainTheory.expSales from the published module SupplyChainTheory_contracts. Every profit includes the demand rule (6): without it, (15) and (31) are unbounded in $p$. Optimization is over all real $p$ and $r$ and all $q \ge 0$, nonnegative stocks and demand being the paper's setting; with negative stocks the profits are unbounded. Optimality of the paper's closed-form triple is claimed, never uniqueness, and "induces the retailer to maximize supply chain profit" is stated as "the chain-optimal triple is a retailer optimum"; that the triple maximizes $\Pi_T$ is Proposition 2, formalized in mission 1, and not restated. The optimal stock is any solution of the fractile equation, and no continuity of $D$ is assumed. The Nash equilibrium of Proposition 4 is written as the two best-response inequalities. Proposition 5 adds the hypothesis $w \ge s$, implied by the paper's range $w \ge c$ (p. 19) and necessary: for $w < s$ the retailer's profit is unbounded. The kept-only rebate of Sec. 5.4 has no printed formula; its profit is (24) with the rebate removed from the returned-units term. Printed page numbers equal PDF page numbers throughout the source. A formalization in which the retailer's profit is defined as $\phi\,\Pi_T$, or in which the optimization is restricted to $r = s$, would make the goal trivial and is excluded: (31) is stated with free $w$, $b$, $l$, and the contract enters only through hypotheses.

The model module (SuReturns.Coordination.Model) restates the single-seller objects of mission 1 in this sub-namespace. Contributions welcome: proofs of the two optimization steps as reusable lemmas (the refund step for a general valuation law and the newsvendor step for an arbitrary demand law), which serve every milestone here.

Selected references

• X. Su, Consumer Returns Policies and Supply Chain Performance, SSRN working paper 1020451, version of August 2008. https://ssrn.com/abstract=1020451 ; published in Manufacturing & Service Operations Management 11(4), 2009. https://doi.org/10.1287/msom.1080.0240
• G. P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in Operations Research and Management Science, vol. 11, 2003. https://doi.org/10.1016/S0927-0507(03)11006-7
• B. A. Pasternack, Optimal Pricing and Return Policies for Perishable Commodities (the buy-back contract), Marketing Science 4(2), 1985. https://doi.org/10.1287/mksc.4.2.166

Motivation

The linear complementarity problem asks, for a real square matrix $M$ of order $n$ and a vector $q\in\mathbb R^n$, for a vector $z$ with

$$z\ge 0,\qquad w=Mz-q\ge 0,\qquad z^{\mathsf T}w=0 .$$

It is the common form of the Kuhn–Tucker conditions of linear and convex quadratic programs and of the equilibrium conditions of two-person non-zero-sum (bimatrix) games. In 1964 Lemke and Howson gave a constructive existence proof for equilibrium points of bimatrix games by following a path of adjacent extreme points of a polyhedron (Lemke–Howson 1964). In 1965 Lemke adapted that path-following technique to the general problem above, under a condition on $M$ that covers the positive semidefinite case treated by Dantzig and Cottle and the case $M>0$ (Lemke 1965). The resulting procedure, now called Lemke's algorithm or complementary pivoting, became a standard method for linear complementarity problems and a template for later path-following existence proofs (Cottle, Pang, Stone 1992).

Timeline:

• 1964: Lemke and Howson, adjacent-extreme-point path for bimatrix games.
• 1965: Lemke, existence for matrices satisfying conditions (i)–(ii) below (the goal of this mission), under a non-degeneracy assumption, by an augmented path with an artificial variable $z_0$.
• Later literature names matrices with (i)–(ii) copositive-plus, and removes non-degeneracy by lexicographic perturbation.

Setting

Fix a finite index set of size $n$, a real $n\times n$ matrix $M$ and $q\in\mathbb R^n$. Inequalities between vectors are componentwise and $e$ is the all-ones vector.

• The set $Z=\{z\in\mathbb R^n : z\ge 0,\ w=Mz-q\ge 0\}$; $w$ is always the function $Mz-q$ of $z$.
• An equilibrium point is a point $z\in Z$ with $z^{\mathsf T}w=0$; $S$ is the set of them.
• For any $z\in\mathbb R^n$, the matrix $N(z)$ consists of the columns of $(M^{\mathsf T},I)$ that are kept when one deletes the $i$-th column of $M^{\mathsf T}$ whenever $w_i\ne 0$ and the $i$-th column of $I$ whenever $z_i\ne0$.
• An extreme point of $Z$ is a point $z\in Z$ with $\operatorname{rank}N(z)=n$; $z$ lies on an open edge if $z\in Z$ and $\operatorname{rank}N(z)=n-1$. An open edge is the set of points of $Z$ sharing the matrix $N(z)$ of such a point; a ray is an open edge with exactly one end-point.
• $Z$ is non-degenerate if for every $z\in\mathbb R^n$ the columns of $N(z)$ are linearly independent.
• For an index $s$, $Z_s=\{z\in Z : z^{\mathsf T}w=z_sw_s\}$. An adjacency path is a non-empty connected class of closed edges of $Z$ no three of which meet; its end-points are the extreme points lying on exactly one of its edges.
• The augmented sets: $Z^*=\{(z,z_0) : z\ge0,\ z_0\ge0,\ Mz+z_0e-q\ge0\}$, its subset $Z_0^*$ where $z^{\mathsf T}w=0$, and, for a number $k$, $Z^{**}$, the set of the form above for the bordered data $\begin{pmatrix}M&e\\-e^{\mathsf T}&0\end{pmatrix}$, $\begin{pmatrix}q\\-k\end{pmatrix}$.

Formalization targets

Goal: Theorem 4 (p. 7)

Suppose $Z$ is non-degenerate and that for every $u\ge0$

$$\text{(i)}\ u^{\mathsf T}Mu\ge 0,\qquad \text{(ii)}\ u^{\mathsf T}Mu=0\ \Longrightarrow\ Mu+M^{\mathsf T}u=0 .$$

Then

$$Z\ne\emptyset\ \Longrightarrow\ \exists z\in Z,\ z^{\mathsf T}(Mz-q)=0 .$$

Milestones, in the order the paper's proof uses them

1. Theorem 1 (p. 3): for non-degenerate $Z$, $Z_s$ is empty or a disjoint union of adjacency paths whose end-points are exactly the equilibrium points.
2. Lemma 2 (p. 4): $Z=\emptyset$ iff some $u\ge0$ has $M^{\mathsf T}u\le0$, $u^{\mathsf T}q>0$.
3. Theorem 2 (p. 4): if some $Z_s$ contains precisely one ray of a non-degenerate $Z$, the number of equilibrium points is odd.
4. p. 6: for $k$ chosen as in (12), the starting ray $E_0^*$ ($z=0$) is a ray of $Z^{**}$ inside $Z_0^{**}$, and it is the only one.
5. Lemma 2 (p. 6): $Z^{**}$ has an equilibrium point.
6. Lemma 3 (p. 7): a ray $(\bar z+\theta u,\bar z_0+\theta u_0)$ of $Z^*$ in $Z_0^*$ with $e^{\mathsf T}u=1$ satisfies $u^{\mathsf T}Mu+u_0=0$.
7. (22)–(25) (pp. 7–8): under (i)–(ii) such a ray has $\bar z_0=0$ and $\bar z$ an equilibrium point of $Z$, or $\bar z_0>0$ and $Z=\emptyset$.

Companion results

The Corollary (p. 5: $q=e$, $M>0$ gives an odd number of equilibrium points), Theorem 3 (p. 5: if $z^{\mathsf T}Mz\ge0$ for all $z$, at most one equilibrium point) and Theorem 5 (p. 8: if moreover $Z\ne\emptyset$, $Z$ has at least $n$ rays).

Significance

Theorem 4 is an existence theorem for a class of linear complementarity problems that contains convex quadratic programming (the case $z^{\mathsf T}Mz\ge0$ for all $z$) and strictly positive matrices, and its proof is an algorithm: the path followed is the sequence of pivots of Lemke's method. The parity statements (Theorem 2, the Corollary) are an early instance of the path-following parity arguments later abstracted in the complexity class PPAD (Papadimitriou 1994).

The theorem is classical and proved. To our knowledge neither Lemke's theorem nor the polyhedral path machinery of Theorems 1–2 has a machine-checked proof in Lean or Mathlib. This mission produces the vocabulary of non-degenerate complementarity polyhedra (the matrix $N(z)$, open edges, rays, adjacency paths), the parity theorem, and the existence theorem itself; the Farkas-type Lemma 2 (p. 4) is already available on the platform.

Difficulty

The algebraic part (Lemma 3 and (22)–(25)) is short. The difficulty is combinatorial-geometric: Theorem 1 requires that, under non-degeneracy, every extreme point of $Z$ has exactly $n$ incident edges, that each point of $Z_s$ is an extreme point or lies on an open edge, and that the edges contained in $Z_s$ form paths whose end-points are exactly the equilibrium points; the parity of Theorem 2 then needs finiteness of the set of extreme points. None of this polyhedral structure (edges as zero-pattern classes, their closures and end-points) is in Mathlib. Moreover, the printed proof of Theorem 4 applies Theorem 2 to $Z^{**}$, whose non-degeneracy the paper obtains from an informal perturbation remark, and it sketches the step from the end of the augmented path to a ray of $Z^*$; a complete proof of the goal must supply these steps or take another route.

Formalization scope

• Vectors are functions from a finite index type $\iota$ to $\mathbb R$ ($n=|\iota|$; $\mathrm{Fin}\,n$ is a special case); the bordered system lives on $\iota\oplus\{\ast\}$. $w$ is always $Mz-q$, never a free variable.
• $N(z)$ is the indexed family of its columns, $\operatorname{rank}N(z)$ the dimension of their span; "$\operatorname{rank}N(z)=n-1$" is written $\operatorname{rank}N(z)+1=n$.
• Non-degeneracy (Def. 3) is linear independence of the columns of $N(z)$ for every $z\in\mathbb R^n$. The phrase "(but not all)" is read as excluding only the empty matrix; the other reading differs only when $q=0$, and the formal definition is then the stronger hypothesis.
• An open edge is the set of points of $Z$ with the zero pattern of a point $z_0$ with $\operatorname{rank}N(z_0)=n-1$; closed edges are closures; end-points of an open edge $E$ are the points of $\overline E\setminus E$; a ray has exactly one. Adjacency paths are classes of closed edges.
• Conditions (i)–(ii) are quantified over $u\ge0$ only. "Non-negative definite" (Theorems 3, 5) is $z^{\mathsf T}Mz\ge0$ for all $z$, with no symmetry assumed.
• "An odd number" is finiteness plus odd cardinality; "at least $n$ rays" counts rays as an extended natural number; "at most one" is a subsingleton.
• Equilibrium points include membership in $Z$: $z^{\mathsf T}(Mz-q)=0$ alone holds at $z=0$ and would make the goal trivial. The goal mentions neither $Z^*$, $Z^{**}$, $k$, rays nor paths; in particular non-degeneracy of $Z^{**}$ is not a hypothesis of the goal.
• Deviations: Lemma 2 (p. 6) assumes non-degeneracy of $Z^{**}$ (Def. 3 does not define it for the non-square $Z^*$); milestone 4 holds for every $k$ without non-degeneracy; Lemma 3 and (22)–(25) parametrize the ray as in (15) without requiring $\bar z^*$ to be an extreme point, which makes them stronger.

Contributions welcome: the polyhedral lemmas for non-degenerate $Z$ (extreme points have $n$ edges, finitely many extreme points), the parity argument, and any complete route to Theorem 4.

Selected references

• C. E. Lemke, Bimatrix Equilibrium Points and Mathematical Programming, Management Science 11(7):681–689, 1965. https://doi.org/10.1287/mnsc.11.7.681 (cited from the HAL deposit hal-01885823v1)
• C. E. Lemke, J. T. Howson, Equilibrium Points of Bimatrix Games, J. SIAM 12(2):413–423, 1964. https://doi.org/10.1137/0112033
• R. W. Cottle, J.-S. Pang, R. E. Stone, The Linear Complementarity Problem, Academic Press 1992; SIAM Classics 2009. https://doi.org/10.1137/1.9780898719000
• C. H. Papadimitriou, On the complexity of the parity argument and other inefficient proofs of existence, J. Computer and System Sciences 48(3):498–532, 1994. https://doi.org/10.1016/S0022-0000(05)80063-7

Motivation

Large retailers hold point-of-sale and loyalty-card data that their suppliers cannot observe, and many of them sell access to it through data-sharing programs; others share the same data for free, or with only some suppliers (Shang, Ha & Tong 2016, §1). When two competing manufacturers sell through one common retailer, sharing a demand signal with a manufacturer changes how he sets his wholesale price, which in turn changes the retailer's margins and the rival's demand. Whether the retailer wants to share, with how many manufacturers, and at what price, is therefore a question about a multistage game with incomplete information.

Shang, Ha and Tong answer it for linear demand, a linear-expectation signal and quadratic production costs, under two contracting protocols. This mission covers the production economy case (marginal cost decreasing in volume, §6 of the paper), in which the retailer may have an incentive to share information even without payment. A companion mission covers production diseconomy (§5).

Setting

Two manufacturers $i \in \{0,1\}$ sell substitutable products through a common retailer. Demand for product $i$ is

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

where $p_i$ is the retail price, $\phi > 0$ measures competition intensity and $\theta$ is a demand shock with mean $0$ and variance $\sigma^2 > 0$. The retailer observes a demand signal $Y$ with $E[Y \mid \theta] = \theta$ and a linear-expectation structure $E[\theta \mid Y] = \beta Y$, where $\beta = \beta(t,\sigma)$ is the signal weight. Producing $q$ units costs $bq - c_e q^2$ with $c_e > 0$; the paper writes $c = -c_e$ and assumes $c_e < 2/(1+\phi)$ (the Assumption, p. 251). Retailing is costless.

The game has three stages.

1. Information contracting. Under concurrent contracting the retailer offers both manufacturers the same payment $T \ge 0$ for the signal; they decide simultaneously and play a Pareto-optimal pure equilibrium. Under sequential contracting she offers a payment $T_f$ to a first manufacturer $k$ and, after his decision, a payment $T_s$ to the other; the outcome is a subgame-perfect equilibrium (SPE). The retailer commits not to share for free after a rejection (§6.2).
2. Pricing. Given the information statuses $X_i \in \{I, U\}$, each manufacturer sets a wholesale price $w_i$ (a function of $Y$ if informed, a constant otherwise), then the retailer sets retail prices; the solution concept is Bayesian Nash equilibrium.
3. Demand realizes and profits are collected.

The ex ante profits of the pricing equilibrium are denoted $\pi_M(0)$, $\pi_M^U(1)$, $\pi_M^I(1)$, $\pi_M(2)$ for a manufacturer and $\pi_R(n)$ for the retailer, $n$ the number of informed manufacturers. $n_e^N$, $n_e^C$, $n_e^S$ denote the equilibrium number of informed manufacturers without contracting, under concurrent and under sequential contracting.

Formalization targets

Goal: Proposition 8(d)

For every $\phi > 0$ and $0 < c_e < 2/(1+\phi)$, pricing equilibria exist, concurrent outcomes and sequential SPEs exist, and for every concurrent outcome and every SPE (either first mover)

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

where $\Pi_R$ is the retailer's profit after side payments and $\Pi_M$ the manufacturers' total profit net of them. The second inequality is asserted for all $c_e$ except at most two values depending only on $\phi$. The comparisons about every pricing equilibrium family exclude the single value $c_e^* = (2+3\phi)/[(1+2\phi)(1+\phi)]$ (see Formalization scope). The paper says "higher"; the inequalities are weak because both sides coincide on intervals of positive length.

Milestones

1. Lemma 1: the pricing equilibrium exists and, for $c_e \ne c_e^*$, is unique and linear in $Y$ with explicit coefficients.
2. §4.2: the ex ante profits $\pi_M(\cdot)$ and $\pi_R(\cdot)$ in closed form.
3. Lemma 5(a)–(c) and Lemma 5(d): sign comparisons of these profits in $c_e$, with thresholds $1/(1+\phi)$, $(4+5\phi)/[(2+3\phi)(1+\phi)]$, $c_e^a$ and $c_e^N$.
4. Proposition 7: thresholds $c_e^C$, $c_e^S$ such that

$$n_e^Z = 0 \text{ for } c_e < \tfrac{1}{1+\phi}, \quad n_e^Z = 2 \text{ for } \tfrac{1}{1+\phi} \le c_e < c_e^Z, \quad n_e^Z = 1 \text{ for } c_e^Z \le c_e < \tfrac{2}{1+\phi}.$$

5. Proposition 6(b): the same structure for $n_e^N$ with a threshold $c_e^N$.
6. Proposition 8(a): $c_e^N < c_e^S \le c_e^C$.

Significance

Proposition 8(d) says that a common retailer who sells information prefers to sell it sequentially, and that the manufacturers bear the cost: sequential offers let her extract a larger payment from the first manufacturer, because his outside option depends on what she will do with the second. Together with Propositions 6 and 7 it explains why retailers under production economy share with only a subset of suppliers once economies of scale or competition are strong, and why a retailer may share data for free, a practice the diseconomy model cannot produce.

The results are proved in the paper, partly by "it is straightforward" arguments (the proofs of Lemmas 2–5 are omitted). No part of the paper is formalized. A formalization adds a machine-checked account of the equilibrium selection at the boundary payments, where the paper's case analysis is informal, and of the points at which the retailer is indifferent between outcomes.

Difficulty

The pricing stage is a Bayesian game with a continuum of strategies: an informed manufacturer's strategy is an arbitrary square-integrable function of the signal. Lemma 1's uniqueness needs the Assumption (without it the manufacturer's problem is not concave) and a conditional-expectation argument, not a finite-dimensional computation. The comparisons of Lemma 5 are sign conditions on rational functions of $(c_e, \phi)$ whose thresholds $c_e^a$, $c_e^N$ are implicit roots. The contracting stage is where the naive argument fails: at the boundary payments several equilibria give the retailer the same payoff but the manufacturers different payoffs, so "the" outcome is not well defined there, and a direct comparison of closed-form profits at the paper's selected equilibria does not cover every equilibrium.

Formalization scope

Lean represents manufacturers by Fin 2, statuses by an inductive type with informed and uninformed, and a pricing strategy by a function of the signal value. The committed conventions are these.

1. Admissible strategies are measurable with square-integrable $w_i(Y)$, and constant for an uninformed manufacturer; ex ante optimality over them is the Bayesian equilibrium condition.
2. The retailer's rule is a best response for every wholesale price pair and signal value, off path included.
3. The production cost is the uncapped quadratic $bq - c_e q^2$. The paper caps the quantity at $\bar q = b/(2c_e)$ but assumes the cap is reached with negligible probability (footnote 11, p. 251) and computes every result of §4.2 and §6 without it. The condition $b < a$ of that footnote is not imposed.
4. Contracting uses pure strategies, nonnegative payments, and no free-sharing move after a rejection.
5. A concurrent outcome is a payment and a pure equilibrium whose retailer payoff equals the supremum of her payoffs over Pareto-optimal equilibria. The supremum is not always attained: for large $c_e$ the paper's optimal payment $\pi_M^I(1) - \pi_M(0)$ makes $(U,U)$ an equilibrium that Pareto-dominates the one-informed outcome it selects.
6. Threshold statements take the two-clause form: the stated value of $n$ is attained on each region with its printed endpoints, and is the only value on the region's interior. Thresholds depend only on $\phi$ and are quantified before all other parameters.
7. The manufacturers' comparison in the goal excludes at most two values of $c_e$. At the thresholds $c_e^C$, $c_e^S$ outcomes with different manufacturer totals coexist, and the universal comparison fails.
8. A correction of the paper. At $c_e^* = (2+3\phi)/[(1+2\phi)(1+\phi)]$, which lies in $(1/(1+\phi), 2/(1+\phi))$, the slope of the best-response wholesale price (2) is exactly $-1$. The equations $w_i = \hat w_i(w_j)$ are then singular, and every status profile has a continuum of pricing equilibria (for $n = 0$, $w_{1,2} = \bar w \pm t$ for every $t$) whose ex ante profits differ. Lemma 1's uniqueness claim fails there, so do the §4.2 identities for every equilibrium family, and so does every statement built on them. Each statement that quantifies over all pricing equilibria therefore assumes $c_e \ne c_e^*$; existence is still asserted at $c_e^*$.

The ex ante profits in every statement are those of an equilibrium of the pricing game on the signal model, not the §4.2 closed forms; a formalization that defined them by the closed forms would reduce the goal to algebra and a $2 \times 2$ game, and is ruled out. The model layer (signal model, pricing equilibrium, payoff table, both contracting games) is shared, name for name, with the production diseconomy mission. Contributions are welcome on each milestone, and on reusable pieces: linear-expectation signals, and pointwise optimization under conditional expectation.

Selected references

• Shang W., Ha A. Y., Tong S., Information Sharing in a Supply Chain with a Common Retailer, Management Science 62(1):245–263, 2016. https://doi.org/10.1287/mnsc.2014.2127
• Ericson W. A., A note on the posterior mean of a population mean, Journal of the Royal Statistical Society B 31(2):332–334, 1969 (cited for the formula of $\beta(t,\sigma)$, which this mission does not use).
• Vives X., Oligopoly Pricing: Old Ideas and New Tools, MIT Press, 1999, §2.7.2.
• Li L., Information sharing in a supply chain with horizontal competition, Management Science 48(9):1196–1212, 2002. https://doi.org/10.1287/mnsc.48.9.1196.177

Motivation

Stochastic fictitious play is a basic model of learning in repeated games. Each period every player best responds to the empirical frequencies of the opponents' past play, after the player's payoffs have been hit by a fresh random shock. It was introduced by Fudenberg and Kreps (1993), is a standard object in the theory of learning in games (Fudenberg and Levine, The Theory of Learning in Games, 1998), and underlies the quantal-response and logit-learning models used in experimental economics and multi-agent reinforcement learning. The question is whether the players' beliefs settle down, and on what.

Potential games, in which all players receive the same payoff, cover pure coordination games and, after the usual payoff transformations, congestion games and weighted potential games. For them Hofbauer and Sandholm (Econometrica 70, 2002) proved that stochastic fictitious play converges almost surely, and that under a generic regularity condition the limit is a single linearly stable rest point of the perturbed best response dynamic.

Timeline. Fudenberg and Kreps (1993) and Kaniovski and Young (1995) established convergence in 2×2 games. Benaïm and Hirsch (1999) related the process to its mean ordinary differential equation and proved convergence in some $p$ player, two strategy games. Hofbauer (2000) and Hofbauer and Hopkins (2000) constructed Lyapunov functions for the deterministically perturbed dynamics. Hofbauer and Sandholm (2002) combined these with a representation theorem for random utility models and with Pemantle's (1990) nonconvergence theorem to obtain the result formalized here.

Setting

A $p$ player game has finite strategy sets $S^\alpha = \{0,\dots,n^\alpha-1\}$ and utilities $u^\alpha : S \to \mathbb R$ on pure profiles $S = \prod_\beta S^\beta$. The game is a potential game if $u^\alpha(s) = u^\beta(s)$ for all players and all profiles. Mixed profiles form $\Sigma = \prod_\alpha \Delta S^\alpha$, and player $\alpha$'s payoff vector is $U^\alpha_i(x^{-\alpha}) = \sum_{s:\,s^\alpha=i} u^\alpha(s)\prod_{\beta\ne\alpha}x^\beta_{s^\beta}$.

Player $\alpha$'s payoffs are perturbed by a random vector $\varepsilon^\alpha$ with a strictly positive density $f^\alpha$ on $\mathbb R^{n^\alpha}$. The choice function is $C^\alpha_i(\pi) = P(\arg\max_j \pi_j + \varepsilon^\alpha_j = i)$, assumed continuously differentiable, and the perturbed best response is $\tilde B^\alpha(x^{-\alpha}) = C^\alpha(U^\alpha(x^{-\alpha}))$.

In standard stochastic fictitious play, shocks $\varepsilon^\alpha_t$ are independent over time and across players. From an arbitrary initial pure profile, at time $t+1$ each player plays a maximizer of $U^\alpha_k(Z_t^{-\alpha}) + (\varepsilon^\alpha_t)_k$, where the beliefs are the time averages

$$Z_t = \frac1t\sum_{u=1}^t \zeta_u .$$

The mean dynamic of this process is the perturbed best response dynamic

$$(P)\qquad \dot x^\alpha = \tilde B^\alpha(x^{-\alpha}) - x^\alpha .$$

A rest point $x^*$ of (P) is hyperbolic if every eigenvalue of $DF(x^*)$ restricted to the tangent space $\prod_\alpha \mathbb R^{n^\alpha}_0$ of $\Sigma$ has nonzero real part, and linearly stable if every such eigenvalue has negative real part. $RP(P)$ and $LS(P)$ denote the rest points and the linearly stable rest points.

By Theorem 2.1 of the paper, $C^\alpha(\pi) = \arg\max_{y\in\operatorname{int}\Delta}(y\cdot\pi - V^\alpha(y))$ for an admissible deterministic perturbation $V^\alpha$, so (P) coincides with the deterministically perturbed dynamic (PV), in which the argmax replaces $C^\alpha$.

Formalization targets

Goal: Theorem 6.1(iii)

For every potential game, every family of densities meeting the conditions above, every probability space, independent shock family and initial profile:

1. if the shocks are smooth enough that the $V^\alpha$ are $C^N$, $N = \sum_\alpha(n^\alpha-1)$, then

$$P\big(\omega(Z_t)\text{ is a connected subset of } RP(P)\big) = 1;$$

2. if every rest point of (P) is hyperbolic and the field of (P) is $C^2$, then

$$P\Big(\lim_{t\to\infty} Z_t \text{ exists and lies in } LS(P)\Big) = 1.$$

Milestones

In attack order: Theorem 2.1 (the representation), Proposition 4.1 (the function $\Pi(x) = \sum_s u^1(s)\prod_\alpha x^\alpha_{s^\alpha} - \sum_\alpha V^\alpha(x^\alpha)$ is a strict Lyapunov function for (PV)), the identification of the critical points of $\Pi$ with the rest points of (PV), Proposition 4.2 ($CR(PV) = RP(PV)$ under $C^N$ smoothness), Proposition 4.3 (under hyperbolicity $RP(PV)$ is finite and equals $CR(PV)$), and Lemmas A.5 and A.4 (a uniform nondegeneracy condition for the noise of the process).

Significance

The result. Theorem 6.1(iii) says that decentralised, boundedly rational learning in common-interest games does not cycle or wander: beliefs converge to a rest point of the perturbed dynamic, and generically to one that is linearly stable, hence a local maximizer of the perturbed potential $\Pi$. Rest points approximate Nash equilibria as the noise vanishes (Proposition 3.1 of the paper), so the theorem is a selection result for equilibria reached by learning. It is also a template for the stochastic-approximation analysis of learning algorithms whose mean dynamic has a Lyapunov function.

Formalizing it. The theorem is proved in the paper, but none of its ingredients is machine-checked: the random utility representation, chain recurrence of flows, Lyapunov arguments for (PV), and the stochastic-approximation step (Benaïm–Hirsch, Benaïm, Pemantle) are all absent from Mathlib and from this platform. A complete development produces a reusable stochastic-approximation layer, not only this theorem.

Difficulty

The obvious argument, "(P) has a strict Lyapunov function, so the process converges to its rest points", fails twice. First, a strict Lyapunov function does not by itself make every chain recurrent point a rest point (the paper cites counterexamples of Akin and of Benaïm); the step needs either Sard's theorem for a $C^N$ function or finiteness of the rest points, and the stochastic-approximation theory controls the process only through the chain recurrent set. Second, convergence to linearly stable points requires showing that the process avoids unstable rest points. This rests on Pemantle's theorem, whose nondegeneracy hypothesis must be verified uniformly over states and directions (Lemma A.4). Neither step follows from the ODE alone: the theorem is about the random process $Z_t$.

Formalization scope

Players are Fin p with p ≥ 2, strategies Fin (n α) with n α ≥ 1, and mixed profiles live in the ambient space (α : Fin p) → Fin (n α) → ℝ, on which every vector field is defined. Choice probabilities are probabilities of strict argmax events under volume.withDensity (f α). The process $Z_t$ is defined pathwise from the shocks, ties broken by the smallest index (a null event), and the theorem quantifies over every probability space and every independent shock family with the given laws. Derivatives of $V^\alpha$ are those of $V^\alpha$ composed with the projection onto the plane $\sum_i y_i = 1$. Eigenvalues are the complex roots of the characteristic polynomial of the derivative restricted to the tangent space of $\Sigma$. Solutions of a dynamic are differentiable curves on $[0,\infty)$ that stay in $\Sigma$, and chain recurrence uses $\varepsilon$-chains with times $t_i \ge 1$.

A formalization about the ODE (P) in place of the process $Z_t$, a fixed noise law such as logit, or convergence to $RP(P)$ in place of $LS(P)$ would prove a different and weaker statement. These are excluded.

Needed infrastructure: the random utility representation (mission I of this series), flows and chain recurrence of $C^1$ vector fields on compact sets, Sard's theorem for real-valued $C^N$ functions, and the stochastic-approximation theorems of Benaïm–Hirsch (1999, Thm 3.3), Benaïm (1999, Props. 5.3 and 6.4) and Pemantle (1990, Thm 1). The last three are reusable well beyond this mission, and contributions of any of them are welcome.

Selected references

• J. Hofbauer and W. H. Sandholm, On the Global Convergence of Stochastic Fictitious Play, Econometrica 70(6), 2265–2294, 2002. https://doi.org/10.1111/1468-0262.00376
• M. Benaïm and M. W. Hirsch, Mixed Equilibria and Dynamical Systems Arising from Fictitious Play in Perturbed Games, Games and Economic Behavior 29, 36–72, 1999. https://doi.org/10.1006/game.1999.0717
• M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, 1–68, 1999. https://doi.org/10.1007/BFb0096509
• R. Pemantle, Nonconvergence to Unstable Points in Urn Models and Stochastic Approximations, Annals of Probability 18(2), 698–712, 1990. https://doi.org/10.1214/aop/1176990853
• D. Fudenberg and D. M. Kreps, Learning Mixed Equilibria, Games and Economic Behavior 5, 320–367, 1993. https://doi.org/10.1006/game.1993.1021
• J. Hofbauer and E. Hopkins, Learning in Perturbed Asymmetric Games, Games and Economic Behavior 52, 133–152, 2005. https://doi.org/10.1016/j.geb.2004.06.006