Algorithmic Game Theory

Review blackmail on online platforms

Online marketplaces depend on consumer reviews, and a single negative review can move a seller's future sales. Review blackmail exploits this: a consumer buys a product, posts a negative review, and offers to remove it in exchange for a payment. Platforms such as Amazon, eBay, Taobao and TripAdvisor respond with dispute resolution mechanisms that let sellers contest reviews. Papanastasiou, Yang and Zhang (Management Science 69(10), 2023) build a game-theoretic model of the seller, the blackmailer and the market's belief about product quality, and ask how the design of such a mechanism changes the blackmailer's leverage. Their first finding concerns a centralized mechanism, where the seller reports the review and the platform judges it: making the platform faster or more accurate does not always lower the ransom the blackmailer can extract. This mission formalizes that result together with the equilibrium analysis it rests on.

The model

A monopolist sells a product of unobservable quality $q\in\{l,h\}$; the market's prior that quality is high is $a\in(0,1)$. A buyer of a high-quality product has gross utility $v_j$ with probability $\theta\in(0,1)$ and $0$ otherwise, with $v_j$ standard uniform; a low-quality product always gives $0$. One consumer arrives.

• With probability $\beta\in(0,1)$ he is malicious: he buys, posts a negative review $N$, and demands a ransom $r$ for removing it.
• Otherwise he is regular: at price $p$ he buys iff $a\theta v_j-p\ge0$, which happens with probability $\rho=1-p/(a\theta)$, and posts a truthful review, positive ($P$) or negative ($N$). No purchase means no review, written $R=0$.

The market sees the review $R\in\{N,0,P\}$, updates its belief to a posterior $a'$ by Bayes' rule, and the seller then earns a continuation payoff $\pi(a')$, with $\pi$ nonnegative, convex and strictly increasing on $[0,1]$.

Facing a ransom demand the seller can settle ($s$: pay $r$, the review disappears), do nothing ($n$: the review stays), or report ($c$) the review to the platform's centralized mechanism at a hassle cost $c\ge0$. The platform investigates immediately with probability $\gamma\in[0,1]$ (timeliness) and identifies a malicious review correctly with probability $\delta\in[0,1]$ (accuracy); the review is removed with probability $\gamma\delta$, the mechanism efficiency.

The market cannot observe the seller's interaction with the blackmailer. It holds a belief $i\in\{s,n,c\}$ about the seller's response, and this belief determines the posteriors: under belief $i$ a malicious review stays visible with probability $m_s=0$, $m_n=1$ or $m_c=1-\gamma\delta$, and $a^i_R$ is the Bayes posterior computed from the resulting review likelihoods. When the market believes $i$ and the seller plays $j$, his payoff is $\pi(a^i_0)-r$ ($j=s$), $\pi(a^i_N)$ ($j=n$), or $\gamma\delta\,\pi(a^i_0)+(1-\gamma\delta)\pi(a^i_N)-c$ ($j=c$). A response $i$ is an equilibrium if it is a best response to the belief $i$; among several equilibria, the seller-preferred one prevails. The malicious consumer buys iff some ransom $r>p$ is accepted in the prevailing equilibrium, and the equilibrium ransom $r^*$ is the greatest ransom at which settling prevails.

Formalization targets

Goal: Corollary 1 (p. 14)

If $c>0$ and $p<\pi(a)-\pi(a^n_N)-c$, there are efficiencies $0\le e_1<e_2\le1$ at both of which the malicious consumer purchases, with

$$r^*(e_1)<r^*(e_2).$$

The equilibrium ransom is not monotonically decreasing in the efficiency $\gamma\delta$.

Milestones

1. Lemma 2 (p. 11): $a^i_P=1$, $a^i_0=a$, $a^i_N\in[0,a]$, and closed forms of $a^n_N$, $a^c_N$, $a^s_N$.
2. Ordering (§4.1, p. 11): $a^s_N<a^c_N<a^n_N$ for $0<\gamma\delta<1$.
3. Proposition 1(1)–(3) (p. 13): the exact conditions under which $n$, $s$ and $c$ are equilibria, e.g.

$$i=n\ \text{is an equilibrium}\iff \pi(a^n_N)\ge\max\{\pi(a)-r,\ \pi(a)-c/\gamma\delta\}.$$

4. Proposition 2(1)–(2) (p. 13): the equilibrium ransom

$$r^*=\begin{cases}\pi(a)-\pi(a^n_N), & c\ge\gamma\delta(\pi(a)-\pi(a^n_N)),\\ (1-\gamma\delta)[\pi(a)-\pi(a^c_N)]+c, & c<\gamma\delta(\pi(a)-\pi(a^n_N)),\end{cases}$$

and the malicious consumer purchases iff $p<r^*$.

Significance

Corollary 1 is the paper's headline message about centralized dispute resolution: improving the mechanism's timeliness or accuracy can raise the ransom. Below an efficiency threshold the mechanism is never used and the ransom equals the seller's loss from a visible negative review; just above it, the market expects the seller to report blackmail, which softens how it reads a negative review, and the blackmailer can ask for more. This is the motivation for the paper's second design, semi-decentralized dispute resolution, analysed in a companion mission. Proposition 2 is the complete characterization of the blackmailer's equilibrium behaviour under the centralized mechanism and is used again in the paper's pricing analysis (§4.4).

The results are proved in the paper (Appendix C). No machine-checked version exists. This mission produces Lean statements of the model, of the Bayes posteriors, of the equilibrium conditions, of the seller-preferred selection and of the ransom characterization, all derived from the primitive game rather than from the paper's closed forms.

Difficulty

Each step is elementary, but the chain is long and sign-sensitive. The equilibrium conditions require handling a belief-dependent payoff (the posterior depends on what the market believes, not on what the seller does), so a deviation changes the action without changing the posteriors. The ransom characterization needs a three-way comparison of equilibria and the tie-breaking in favour of settling at the boundary, where two equilibria give the same payoff. The corollary needs the jump at the threshold efficiency $c/(\pi(a)-\pi(a^n_N))$ to be strictly positive and to survive a small increase of the efficiency: the posterior $a^c_N$ moves with the efficiency, so a continuity argument for $\pi$ composed with the posterior is required, and $\pi$ is only assumed convex and strictly increasing on $[0,1]$. The natural first idea, comparing the two closed forms of Proposition 2 at a single point, does not suffice, since at the threshold itself the two regimes coincide in value.

Formalization scope

• Representation. One structure Model with fields $a,\theta,\beta,p,c$ and $\pi:\mathbb R\to\mathbb R$; inductive types for quality, reviews ($N$, Z for $R=0$, $P$) and responses. The posterior post m R is Bayes' rule over the likelihood table with visibility probability $m$ of a malicious review; $a^i_R$ is post (keep (γ*δ) i) R.
• Standing assumptions (Standing): $a,\theta,\beta\in(0,1)$; $\pi\ge0$, convex and strictly increasing on $[0,1]$; $c\ge0$; and $0<p<a\theta$. The last is implicit in the paper: it makes the purchase probability $1-p/(a\theta)$ that of a standard uniform valuation and keeps the event $R=0$ of positive probability. Every theorem also assumes $\gamma,\delta\in[0,1]$.
• Added hypotheses. $0<\gamma\delta<1$ in the ordering (strictness) and in Proposition 1 (the page divides by $\gamma\delta$ and $1-\gamma\delta$). $c>0$ in Corollary 1: at $c=0$ the corollary is false. Corollary 1's hypothesis, printed with a varying $\gamma\delta$, is assumed at the threshold efficiency and required at both exhibited efficiencies.
• Conventions. "Settling prevails" means settling is an equilibrium and no equilibrium pays the seller strictly more (ties go to settling, as in the paper's proof). $r^*$ is stated with IsGreatest of the set of ransoms at which settling prevails; purchase means some such ransom exceeds $p$. "Not monotonically decreasing" means not nonincreasing.
• Ruled out. Defining the posteriors by Lemma 2's closed forms, or $r^*$ by Proposition 2's formulas, would make the milestones definitional; both are defined from the game instead.
• Infrastructure. Only Mathlib (ConvexOn, StrictMonoOn, IsGreatest). Proofs of the milestones in order, and reusable lemmas on the monotonicity of the posterior in the visibility probability, are welcome.

Selected references

• Y. Papanastasiou, S. A. Yang, A. H. Zhang, Improving Dispute Resolution in Two-Sided Platforms: The Case of Review Blackmail, Management Science 69(10):6021–6037, 2023. https://doi.org/10.1287/mnsc.2022.4655 (accepted manuscript: LBS Research Online, eprint 1988, https://lbsresearch.london.edu/id/eprint/1988/)

Motivation

Online marketplaces rely on consumer reviews, and a negative review lowers what future buyers believe about a product. Review blackmail exploits this: a consumer buys, posts a negative review, and offers to remove it for a ransom. Platforms counter with dispute-resolution mechanisms. Papanastasiou, Yang and Zhang (Management Science 69(10), 2023) compare two of them in a Bayesian game between a seller, one consumer and the market. Under the centralized mechanism the seller reports the review and the platform decides whether to remove it. Under the semi-decentralized mechanism the seller removes the review himself, and the platform checks afterwards. If it judges the removal wrongful, it reinstates the review and fines the seller a penalty $b$.

This mission covers the semi-decentralized mechanism. Its main result, Proposition 5, gives the ransom a blackmailer can extract in equilibrium in closed form and says when blackmail pays at all. A platform needs that answer when it chooses the penalty. Mission I of this series treats the centralized mechanism.

Setting

A product has quality $q\in\{l,h\}$. The prior that $q=h$ is $a\in(0,1)$. A buyer of a high-quality product gets a positive experience with probability $\theta\in(0,1)$; a low-quality product never gives one. With probability $\beta\in(0,1)$ the consumer is malicious. A malicious consumer buys at price $p$, posts a negative review $N$ and demands a ransom $r$. Otherwise the consumer is regular. A regular consumer buys with probability $\rho=1-p/(a\theta)$ (valuation $v_j$ uniform on $[0,1]$) and reviews truthfully: positive ($P$) or negative ($N$). No purchase means no review, written $R=0$; a removed review is also seen as $R=0$.

The market observes $R\in\{N,0,P\}$ and forms the posterior $a'$ by Bayes' rule. The seller then earns $\pi(a')$, where $\pi$ is nonnegative, convex and strictly increasing on $[0,1]$.

Facing a ransom demand, the seller can settle ($s$: pay $r$, review removed), do nothing ($n$), or use the mechanism ($d$). Under $d$ the platform judges immediately with probability $\gamma\in[0,1]$ (timeliness). It recognises a malicious review with probability $\delta\in[0,1]$ (accuracy). The review is therefore reinstated with probability $\gamma(1-\delta)$, and the penalty $b\ge0$ is paid with probability $1-\delta$. Write $a^i_R$ for the posterior after review $R$ when the market believes the seller's response is $i$. The payoffs of the three responses are then

$$\pi(a^i_0)-r,\qquad \pi(a^i_N),\qquad (1-\gamma(1-\delta))\pi(a^i_0)+\gamma(1-\delta)\pi(a^i_N)-(1-\delta)b.$$

The market cannot see the interaction, so $i$ is an equilibrium at $r$ if no response pays more given the belief $i$. The equilibrium ransom $r^*$ is the largest $r$ at which settling is an equilibrium and no equilibrium pays the seller more. The malicious consumer buys iff $p<r^*$.

A seller could also use the mechanism against genuine negative reviews. Proposition 4 shows that this is deterred exactly when $b\ge\underline b:=(1-\gamma)[\pi(a)-\pi(a^s_N)]$.

Formalization targets

Goal: Proposition 5 (p. 21)

Let $\delta<1$ and $T=\frac{1-\gamma(1-\delta)}{1-\delta}\big(\pi(a)-\pi(a^n_N)\big)$.

1. If $b\ge T>\underline b$:

$$r^*=\pi(a)-\pi(a^n_N),\qquad\text{and the malicious consumer buys iff } p<r^*.$$

2. If $\underline b\le b<T$:

$$r^*=(1-\delta)\big(\gamma(\pi(a)-\pi(a^d_N))+b\big),\qquad\text{and the malicious consumer buys iff } p<r^*.$$

Milestones

• (5), p. 21: the closed form of $a^d_N$, together with $a^i_0=a$.
• §5.1, p. 21: the ordering $a^s_N<a^d_N<a^n_N$.
• Proposition 4, p. 20: genuine negative reviews are kept iff $b\ge\underline b$.
• Proof of Proposition 5, Step 1, pp. 41–42: the conditions under which $s$, $n$ and $d$ are equilibria, one milestone each.

Significance

Proposition 5 has two regimes. If the penalty is high, the mechanism plays no part in blackmail: the seller would never use it, and the ransom equals the one with no mechanism at all. Below the threshold, the ransom is the seller's expected loss from using the mechanism. A lower ransom then means less blackmail, and it pushes the price at which blackmail stops paying downward. The threshold $T$ rises with the accuracy $\delta$ and falls with the timeliness $\gamma$. The paper's later results on pricing and on the platform's penalty build on this characterization.

The result is proved in the paper (Appendix C, pp. 41–43). It has no machine-checked proof. Formalizing it pins down the equilibrium concept, including the selection among multiple equilibria. It also corrects a printed slip in the proof: the simplified condition for the mechanism to be an equilibrium drops a factor $1-\delta$.

Difficulty

Each individual equilibrium condition is a rearrangement of payoff inequalities. The difficulty lies in selecting among equilibria. Several responses can be equilibria at the same ransom. Settling prevails only if no other equilibrium pays more, and the equilibria themselves depend on $r$. So the set of ransoms at which settling prevails is not given by one inequality. Its greatest element must be found across three scenarios, comparing three thresholds that involve three different posteriors. Those comparisons require the posterior ordering $a^s_N<a^d_N<a^n_N$, which comes from Bayes' rule and not from the payoff algebra. Reading the equilibrium condition for $s$ alone as the answer gives the wrong ransom in case 1.

Formalization scope

Everything lives in the namespace ReviewBlackmail.SemiDec, with one structure Model holding $a,\theta,\beta,p,\gamma,\delta,b$ and the payoff fut (the paper's $\pi$; Real.pi is never used). The predicate Standing collects the standing assumptions: $a,\theta,\beta\in(0,1)$; $\pi$ nonnegative, convex and strictly increasing on $[0,1]$; $\gamma,\delta\in[0,1]$; $b\ge0$; and the disclosed addition $0<p<a\theta$, which makes the purchase probability $\rho$ lie in $(0,1)$. Per-statement additions, each disclosed in the item:

• $\delta<1$ on the goal and on Step 1 for $n$ and $d$, which divide by $1-\delta$;
• $0<\gamma(1-\delta)<1$ on the strict ordering;
• $0<\gamma<1$ on the second half of Proposition 4.

Posteriors are defined by Bayes' rule over an explicit likelihood table with two visibility probabilities: $m$ for malicious and $g$ for genuine negative reviews. Proposition 4 needs beliefs in which genuine reviews are removed. The payoffs of Proposition 5 keep genuine reviews ($g=1$), the case the paper reduces to via Proposition 4. Ties in the selection rule go to settling.

The posteriors $a^i_R$ are never defined by their closed forms, and $r^*$ is never defined by (6) or (7). The goal is stated with IsGreatest on the set of ransoms at which settling prevails, not with sSup, so neither the closed forms nor junk values of a supremum can make the goal trivial.

A complete development needs only Mathlib's ConvexOn, StrictMonoOn and IsGreatest and real-field algebra. The algebra of Bayes posteriors with two-point priors may be reusable. Proofs of the milestones and the goal are welcome, in any order.

Selected references

• Y. Papanastasiou, S. A. Yang, A. H. Zhang, Improving Dispute Resolution in Two-Sided Platforms: The Case of Review Blackmail, Management Science 69(10):6021–6037, 2023. https://doi.org/10.1287/mnsc.2022.4655 (cited from the accepted manuscript, LBS Research Online eprint 1988, https://lbsresearch.london.edu/id/eprint/1988/).

Motivation

Banks lend to each other. When one bank's investments fail, it may be unable to repay its interbank debt, and its creditors then receive less. Since Eisenberg and Noe (2001), the standard way to compute who pays whom after such losses has been a clearing vector: a fixed point of a system in which every bank pays the smaller of what it owes and what it has. Much of the later literature on systemic risk takes the banks' assets as given and asks how losses spread through this fixed point, for example Acemoglu, Ozdaglar and Tahbaz-Salehi (2015).

Chong Shu's paper Endogenous Risk Exposure and Systemic Instability (Management Science, doi:10.1287/mnsc.2022.01519) reverses the question: when banks know they are connected, how much risk do they choose? A successful bank pays its interbank debt in full while its failed counterparties do not, so success is partly taxed by the network. This cross-subsidy shrinks the reward for choosing a safe project. The paper's first main result, Proposition 1, says that in every network the banks' risk choices are strategic complements: when one bank takes more risk, every other bank wants to take more risk too. This mission formalizes Proposition 1.

Setting

A finite set of banks is given. For banks $i,j$, $\bar d_{ij}\ge 0$ is the face value of the debt that bank $j$ owes bank $i$. Bank $j$'s total interbank liability is $\bar d_j=\sum_i\bar d_{ij}$, assumed positive, and $\theta_{ij}=\bar d_{ij}/\bar d_j$ is bank $i$'s share of it. Bank $i$ also owes a deposit $v_i>0$, which must be paid before its interbank debt.

Every bank $i$ picks a project $Z_i$ from an interval $[\underline Z,\overline Z]$. The project pays $Z_i$ with probability $P(Z_i)$ and $0$ otherwise, independently across banks. Assumption 1: $P(z)\in(0,1)$, $P$ is decreasing, and $P(z)\,z$ is concave. A standing assumption rules out systemic default: $\underline Z\ge v_i+\bar d_i$ for every $i$, so a bank whose project succeeds can always pay in full.

A state $\omega\in\{s,f\}^N$ records which projects succeeded; bank $i$'s cash flow is $e_i=Z_i$ if $\omega_i=s$ and $0$ otherwise. A payment equilibrium $d^*(\omega;Z)$ solves

$$d_i^*=\Big\{\min\Big[\sum_j\theta_{ij}d_j^*+e_i-v_i,\ \bar d_i\Big]\Big\}^+\quad\text{for all } i .$$

Bank $i$'s profit is $\Pi_i=(\sum_j\theta_{ij}d_j^*+e_i-v_i-d_i^*)^+$, and its expected profit $\mathbb E[\Pi_i(\omega;Z)]$ is the sum over states weighted by $\Pr(\omega)=\prod_j\Pr(\omega_j)$. The best-response set $\hat Z_i(Z_{-i})$ is the set of maximizers of $\mathbb E[\Pi_i]$ over $Z_i\in[\underline Z,\overline Z]$, with the other banks' choices $Z_{-i}$ held fixed. The cross-subsidy is

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

bank $i$'s expected net payment to the network when its own project succeeds.

Formalization targets

Goal: Proposition 1 (p. 10)

For banks $i\ne m$, profiles $Z\in[\underline Z,\overline Z]^N$, and $Z'$ equal to $Z$ except that $Z_m\le Z'_m$:

$$\hat z\in\hat Z_i(Z_{-i}),\ \hat z'\in\hat Z_i(Z'_{-i})\ \Longrightarrow\ \max(\hat z,\hat z')\in\hat Z_i(Z'_{-i})\ \text{ and }\ \min(\hat z,\hat z')\in\hat Z_i(Z_{-i}).$$

This is the strong-set-order form of "$\hat Z_i$ is nondecreasing in $Z_m$". It does not require the network to be regular or path-connected.

Milestones, in the order of the paper's proof

1. Lemma 2 (p. 8): $d^*(\omega;Z)$ does not depend on $Z$.
2. Auxiliary Lemma (IA p. 7): $d^*(\omega^{j=f})\le d^*(\omega^{j=s})$ componentwise.
3. (7) (p. 9): $\mathbb E[\Pi_i]=P(Z_i)(Z_i-v_i)-P(Z_i)\mathcal D_i(Z_{-i})+(1-P(Z_i))\cdot(\text{expected payoff after failure})$.
4. (I.4) (IA p. 8): $\mathcal D_i(Z_{-i})\le\mathcal D_i(Z'_{-i})$.
5. The $\Omega^{f+}_{-i}$ claims (IA p. 9): a bank that survives its own failure pays $\bar d_i$ in full, and its own state does not change what it receives.
6. $\mathcal D^*_i$ is increasing in $Z_m$ (IA p. 10).
7. Supermodularity (IA p. 10): $\mathbb E[\Pi_i]$ has increasing differences in $(Z_i,Z_m)$.

The regular-network step (I.3) (IA p. 7), that the maximizer of $P(z)(z-v)-P(z)D$ is increasing in $D$, is also posed, as a theorem outside the milestone list.

Significance

Proposition 1 makes the risk-taking game supermodular. That property is what the rest of the paper relies on. It gives existence of equilibrium (Proposition 2) through Tarski's fixed-point theorem, it identifies least and greatest equilibria, and it lets the later comparative statics compare networks: complete against ring, size, central clearing, bailouts. Each of these results argues "the cross-subsidy rises, so equilibrium risk rises", and that step is Proposition 1 applied through Topkis's monotonicity theorem.

On the formal side, no clearing model is currently on the platform. This mission supplies one: the Eisenberg–Noe clearing system with a stochastic state, the greatest clearing vector, expected profits, and best responses. It also checks the paper's proof in the non-regular case. That proof splits on the states in which a bank survives its own failure, and one inequality in it is asserted without proof. The result is proved on paper; none of it has been machine-checked.

Difficulty

In a regular network a failed bank always defaults, and the argument reduces to two monotonicity facts: (I.3) and (I.4). In a non-regular network a failed bank can still earn a profit when enough of its debtors succeed. A riskier counterparty then has two opposite effects. It raises the cross-subsidy, which pushes toward risk, and it lowers the chance of being bailed out after one's own failure, which pushes away from risk. The proof must show that the first effect dominates in every network. It does so by partitioning the states according to whether bank $i$ survives its own failure, $\Omega^{f+}_{-i}$, and by showing that the states in that set contribute nothing to the cross-partial. This requires the clearing vector to be monotone in every bank's success and stable when a surviving bank's own state flips. It also needs an inequality, $v_i+\bar d_i\ge\sum_j\theta_{ij}d^*_j(\omega^{m=f,i=s})$ whenever $\omega^{m=f}_{-i}\notin\Omega^{f+}_{-i}$, which the paper asserts without proof.

The naive route is to differentiate the first-order condition, as the paper does in (I.3). That route is not available: Assumption 1 gives neither differentiability of $P$ nor a unique maximizer.

Formalization scope

Banks form a finite type, and states are Boolean vectors (true = success). All probabilities are finite products and all expectations are finite sums: no measure theory is involved. Sums over $\omega_{-i}$ are written as sums over full states with $\omega_i$ fixed, weighted by the product over $j\ne i$.

Conventions the Lean statements commit to:

• $\bar d_{ij}\ge0$ rather than the page's $\bar d_{ij}>0$. This is the reading forced by the paper's own ring network (Definition 3), and every total $\bar d_j>0$ is assumed. Self-loops are allowed.
• $d^*$ is the greatest solution of the clearing system, the componentwise supremum of all solutions in $[0,\bar d]$. Lemma 1 asserts only generic uniqueness, so a selection is required. The greatest solution is the one Eisenberg–Noe's algorithm returns, and it equals the solution whenever that is unique.
• "Decreasing" in Assumption 1 is read weakly (AntitoneOn), which is the more general hypothesis.
• Every bank's choice, including the varied $Z'_m$, lies in $[\underline Z,\overline Z]$, and the no-default assumption $\underline Z\ge v_i+\bar d_i$ is an explicit hypothesis. Without either, Lemma 2 fails.
• Derivative statements are replaced by order-theoretic ones: the strong set order for $d\hat Z_i/dZ_m\ge0$ and for (I.3), increasing differences for the cross-partial. Strict "$>0$" claims become weak, because they are false when banks $i$ and $m$ are not path-connected.

The goal is vacuous when a best-response set is empty. This is faithful, since $\hat Z_i$ presupposes a maximizer, and best responses exist whenever $P$ is continuous. A formalization that takes $d^*$ as an arbitrary solution under a uniqueness hypothesis, or as an sSup that could be junk, would trivialize the mission. The definition used here is shown, in a sorry-free check, to solve the clearing system.

Not posed: Lemma 1 (cited from Eisenberg–Noe), Proposition 2 and Corollary 1 (consequences of Proposition 1), and the later comparative statics (Propositions 3–9). Proposition 4, the comparison of complete and ring networks, is a separate mission of this series. Reusable contributions are welcome: monotonicity of greatest fixed points in a parameter, and a general Topkis-style argmax monotonicity on chains.

Selected references

• Chong Shu, Endogenous Risk Exposure and Systemic Instability, Management Science (accepted manuscript, 17 Sep 2024). https://doi.org/10.1287/mnsc.2022.01519
• Larry Eisenberg and Thomas H. Noe, Systemic Risk in Financial Systems, Management Science 47(2), 2001. https://doi.org/10.1287/mnsc.47.2.236.9835
• Daron Acemoglu, Asuman Ozdaglar and Alireza Tahbaz-Salehi, Systemic Risk and Stability in Financial Networks, American Economic Review 105(2), 2015. https://doi.org/10.1257/aer.20130456
• Paul Milgrom and John Roberts, Rationalizability, Learning, and Equilibrium in Games with Strategic Complementarities, Econometrica 58(6), 1990. https://doi.org/10.2307/2938316
• Paul Milgrom and Chris Shannon, Monotone Comparative Statics, Econometrica 62(1), 1994. https://doi.org/10.2307/2951479
• Donald M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539

Motivation

Large technology firms often buy small startups mainly to hire their staff, a practice known as acquihiring. Antitrust authorities review acquisitions that may reduce competition in product markets, but an acquihire can instead reduce competition in the labour market: a firm that buys the employer of a scarce worker no longer has to outbid that employer for her. Bar-Isaac, Johnson and Nocke study this effect in a three-player model: a startup, its essential employee, and a potential acquirer (CRC TR 224 Discussion Paper No. 500, 2024; published in Management Science, 2025, doi:10.1287/mnsc.2024.04604).

In the paper's baseline model (Proposition 1) the acquirer, whenever it hires the employee, does so by buying the startup, and the employee always prefers direct wage competition. This mission formalizes §6, where the employee's private benefit from staying at the startup is her private information. That uncertainty softens wage competition, so acquihiring is no longer always chosen, and the paper derives the exact threshold at which the acquirer switches.

Setting

An employee produces value $v_a$ if she works for the acquirer and $v_s$ if she works for the startup. At the startup she also enjoys a private benefit $b$, which only she observes and which is uniformly distributed on $[0,B]$. She has an outside option worth $0$, and wages are unrestricted real numbers. The standing assumptions of §6 are

$$0 < B < \min\{v_a, v_s\}, \qquad v_s - B < v_a < v_s + 2B .$$

The acquirer chooses between two modes.

• Direct hiring. The acquirer and the startup make simultaneous wage offers $w_a$ and $w_s$. A type-$b$ employee joins the acquirer when $w_a > w_s + b$ and $w_a \ge 0$, and stays at the startup when $w_s + b \ge w_a$ and $w_s + b \ge 0$. Expected profits are averages over $b \sim U[0,B]$, for example

$$\pi_a(w_a, w_s) = \frac1B \int_0^B (v_a - w_a)\,\mathbf 1\{\text{type } b \text{ joins the acquirer}\}\,db .$$

A pair $(w_a, w_s)$ is an equilibrium of this wage game when each offer is a best response to the other over all real wages.

• Acquihiring. The acquirer bids for the startup. A startup that is a monopsonist pays wage $0$ and earns $v_s$, so the acquisition succeeds at price $v_s$ exactly when $v_a > v_s$, and the acquirer then pays the employee $0$. The acquirer's acquihiring profit is $\max\{0, v_a - v_s\}$ (Lemma 2 of the paper with wage floor $0$).

The quantities named in the statements are Lemma 5's wages

$$w_a^* = \frac{2v_a + v_s - B}{3}, \qquad w_s^* = \frac{2v_s + v_a - 2B}{3},$$

the indifferent type $b^* = (v_a - v_s + B)/3 = w_a^* - w_s^*$, and the threshold

$$\hat v_a = v_s + \frac{7 - 3\sqrt5}{2}\,B .$$

Formalization targets

Goal: Proposition 5

Under the standing assumptions, $\hat v_a > v_s$, $(w_a^*, w_s^*)$ is a direct-hiring equilibrium, and

$$v_a > \hat v_a \;\Longrightarrow\; \pi_a(w_a^*, w_s^*) < \max\{0, v_a - v_s\},$$ $$v_a < \hat v_a \;\Longrightarrow\; \max\{0, v_a - v_s\} < \pi_a(w_a^*, w_s^*) \ \text{ and the poaching probability is } \frac{v_a - v_s + B}{3B}.$$

In addition, every type $b \in [0,B]$ of employee is strictly better off under direct hiring than under acquihiring.

Milestones

1. A monopsonistic startup sets wage $0$ and earns $v_s$; a monopsonistic acquirer sets wage $0$ (§6, p. 15).
2. Lemma 5: the direct-hiring wages, the poaching probability $(v_a - v_s + B)/(3B) \in (0,1)$, and the acquirer's profit $(v_a - v_s + B)^2/(9B)$.
3. The two values of $v_a$ at which the profits are equal, $\hat v_a$ and $v_s + (7 + 3\sqrt5)B/2$, and the fact that the second lies above $v_s + 2B$.
4. The welfare display in the proof of Corollary 4, and Corollary 4 itself: acquihiring is more efficient than direct hiring exactly when $v_a > v_s + \tfrac45 B$, so on $\tfrac{7-3\sqrt5}{2} < (v_a - v_s)/B < \tfrac45$ the acquirer acquihires although direct hiring yields more surplus.

Significance

The proposition separates two effects that coincide in the baseline model. Without private information, wage competition is Bertrand-like: the winning firm must match the losing firm's full willingness to pay, so buying the competitor is always cheaper. With a privately known benefit, competition between the two employers resembles product differentiation, and each offers less than the employee's productive value. Direct hiring then becomes profitable when $v_a$ is close to $v_s$, and acquihiring is chosen only when $v_a - v_s$ exceeds $\frac{7-3\sqrt5}{2}B \approx 0.146\,B$. Corollary 4 compares this threshold with the efficiency threshold $\frac45 B$ and finds a band of parameters in which acquihiring occurs although it lowers total surplus. That band is the paper's case for labour-market scrutiny of acquisitions.

The results are proved on paper, by first-order conditions and a quadratic comparison. None of them has a machine-checked proof, and the platform has no prior formalization of wage competition, monopsony or acquisitions. The mission adds an explicit Bayesian wage game with expected profits written as integrals over the type distribution, with global best responses rather than first-order conditions. The objects are small enough to be reused for other two-firm wage-posting models with a uniformly distributed taste shock.

Difficulty

The algebra of Proposition 5 is a quadratic inequality in $(v_a - v_s)/B$. The work is in Lemma 5. The page solves first-order conditions inside the region $w_a \ge 0$, $0 < w_a - w_s < B$, where both expected profits are concave quadratics. An equilibrium, however, requires that no deviation pays anywhere on the real line, including offers so low that no type accepts and offers so high that every type accepts. Outside the interior region the profit functions are piecewise (zero below, linear above), and each piece has to be compared with the interior optimum. The expected profits are interval integrals of indicator functions, so evaluating them requires the measure of the set of accepting types. Ties between the two offers occur with probability zero, and the statements are insensitive to how they are broken.

Formalization scope

All quantities are real numbers. The parameters $v_a$, $v_s$, $B$ form a structure, and the five standing inequalities form a predicate that every theorem except the pure-algebra milestone takes as a hypothesis (that milestone needs only $B > 0$). Expected profits, the poaching probability and direct-hiring welfare are $\frac1B \int_0^B$ of bounded, piecewise-constant integrands, hence interval integrable. A verification file evaluates the acquirer's profit at Lemma 5's wages to its closed form on one instance, and exhibits instances of both branches of the proposition and of the window in Corollary 4. Ties $b = w_a - w_s$ go to the startup.

Conventions committed to:

• best responses range over all real wages, which is stronger than the page's first-order conditions;
• the direct-hiring branch is evaluated at Lemma 5's wages, and Lemma 5's uniqueness clause is claimed only within the interior region where the page derives it; uniqueness among all equilibria is not on the page and is not claimed;
• the acquihiring profit $\max\{0, v_a - v_s\}$ and the employee's acquihiring payoff ($0$ if $v_a > v_s$, otherwise her benefit $b$) are Lemma 2's outcomes with wage floor $0$, as §6 states; the milestone on the monopsonistic wage justifies this, and at $v_a = v_s$ the acquisition is taken to fail;
• surplus under acquihiring is $v_a$, the allocation with the employee at the acquirer, as in Corollary 4.

The direct-hiring profit is an integral over the type distribution evaluated at wages that are proved to be an equilibrium. It is not a closed-form payoff taken as a definition. Dropping any standing inequality would change Lemma 5 (the poaching probability leaves $(0,1)$) or Proposition 5 (the second root comes back into range). The employee-preference clause is part of the goal, and no equilibrium is claimed unique beyond what the page derives.

Contributions welcome: the interval-integral evaluations of step functions, the global best-response argument for Lemma 5, and the quadratic comparison with $\sqrt5$.

Selected references

• H. Bar-Isaac, J. P. Johnson, V. Nocke, Acquihiring for Monopsony Power, CRC TR 224 Discussion Paper No. 500, January 2024 (the version formalized here; journal version below).
• H. Bar-Isaac, J. P. Johnson, V. Nocke, Acquihiring for Monopsony Power, Management Science, 2025. https://doi.org/10.1287/mnsc.2024.04604

Motivation

Antitrust authorities review horizontal mergers by asking whether the merged firm will raise prices. A prior question is which mergers firms will choose to form at all. When several firms can merge, the identity of the partner matters: a large firm may absorb a small rival, or two small rivals may combine to face the large one. Wang, Wu, Tang and Dai (Management Science, 2024) study this partner-selection question in a price-competition model with two frictions common in retail and service markets: limited capacity of the small firms, and loyal segments, buyers who only buy from their own firm. Their main result says exactly which merger, if any, arises in equilibrium. Every step of its proof is an explicit comparison of closed-form profits, which makes the result a natural target for complete machine verification.

Setting

Three firms $A$, $B$, $C$ sell a homogeneous product at zero marginal cost. A unit mass of buyers each demand one unit and value it at the reservation price $r>0$. Each firm has $\alpha$ loyal buyers, $0<\alpha<1/3$; the remaining $1-3\alpha$ buyers are switchers who buy from the cheapest firm. Firm $A$ is unconstrained; the small firms $B$ and $C$ each have capacity $k$, with $\alpha<k<1$. Unserved buyers are rationed at random and spill over to the next cheapest firm.

The firms may stay independent, $\{A,B,C\}$; firm $A$ may merge with one small firm, the mixed merger $\{AB,C\}$; or the two small firms may merge, the small merger $\{A,BC\}$. A merged entity pools capacities and loyal buyers. In each structure the firms play a price game whose equilibrium is in mixed strategies. The paper's Table A1 lists, for each structure, the lower bound of price support $L^{(0)}$, $L^{(AB)}$, $L^{(BC)}$ and the equilibrium profits $\Pi^{(0)}_A$, $\Pi^{(0)}_B=\Pi^{(0)}_C$, $\Pi^{(AB)}$, $\Pi^{(AB)}_C$, $\Pi^{(BC)}_A$, $\Pi^{(BC)}$, as piecewise functions of $(\alpha,k,r)$ built from

$$s_1=(1-3\alpha)\Bigl(1-\tfrac{k}{1-2\alpha}\Bigr),\quad s_2=s_1\Bigl(1-\tfrac{k}{\alpha+s_1}\Bigr),\quad s_3=(1-3\alpha)\Bigl(1-\tfrac{2k}{1-\alpha}\Bigr),$$

the numbers of spilled-over switchers. In the small merger each small firm receives half: $\Pi^{(BC)}_B=\Pi^{(BC)}_C=\Pi^{(BC)}/2$.

A structure is an equilibrium structure when no firm or coalition gains by deviating. For $\{AB,C\}$ this is

$$\text{(1a) } \Pi^{(AB)}>\Pi^{(0)}_A+\Pi^{(0)}_B,\qquad \text{(1b) } \Pi^{(AB)}>\Pi^{(BC)}_A+\Pi^{(BC)}_B\ \text{ or }\ \Pi^{(AB)}_C\ge\Pi^{(BC)}_C ;$$

for $\{A,BC\}$ it is

$$\text{(2a) } \Pi^{(BC)}_C>\Pi^{(0)}_C,\qquad \text{(2b) } \Pi^{(BC)}_A+\Pi^{(BC)}_B\ge\Pi^{(AB)} ;$$

and the status quo $\{A,B,C\}$ is the equilibrium structure when neither condition (1) nor condition (2) holds.

Formalization targets

Goal: Proposition 3

With $k^*=\alpha(1-2\alpha)/(1-3\alpha)$,

$$\{S : S\text{ is an equilibrium structure}\}= \begin{cases} \{\{AB,C\}\} & \text{if } k^*<k<1-2\alpha,\\ \{\{A,B,C\}\} & \text{otherwise.} \end{cases}$$

The statement is an exact characterization: in the interval the mixed merger is an equilibrium structure and the small merger is not; outside it neither merger is.

Milestones

1. Lemmas 3–5: on the regions $\Omega^{(0)}_{1,2}$, $\Omega^{(BC)}_{1,2,3}$, $\Omega^{(AB)}_{1,2}$ of the $(\alpha,k)$ plane, each Table A1 maximum equals one explicit branch.
2. Proposition 1: for $k\ge 1-2\alpha$ the independent structure is the unique equilibrium structure.
3. Proposition 2 and the inequality $s_2<s_3$ from its proof: $L^{(AB)}\ge L^{(BC)}\ge L^{(0)}$.
4. The comparisons in the proof of Proposition 3: the $\Sigma$ inequality, the threshold $k^*$ for (1a), the joint profit of $A$ and $B$ under $\{A,B,C\}$, $\{A,BC\}$ and $\{AB,C\}$, and firm $C$'s three pairwise profit comparisons.

Significance

The result separates the two forces of the model. Loyal buyers make a merged entity less aggressive in price, which is why no merger is profitable when capacity is ample. Limited capacity creates spillover demand, which a large firm captures by merging with a small rival but which two small firms do not capture by merging with each other. Proposition 3 says the second force wins exactly on $(k^*,1-2\alpha)$ and that the small merger never forms. This answers one of the paper's opening questions, whether two capacity-constrained small firms merge to compete with a large one: in this model they do not.

The paper proves the result by hand, over eight regions of the parameter plane (its Figure A1). The comparisons involve rational functions whose denominators are positive only under the region's constraints, and threshold curves with square roots. A machine-checked proof certifies the region bookkeeping. No formalization of this result exists.

Difficulty

Each single comparison is elementary algebra; the difficulty is the case structure. Table A1 has four rows in $k$ whose boundaries ($(1-2\alpha)^2/(2-5\alpha)$, $(1-\alpha)/2$, $1-2\alpha$) differ per column, and three of its cells are maxima whose active branch changes along the curves $k^{(0)}_{1,2}$, $k^{(BC)}_{1,2}$, $k^{(AB)}_1$. Root-location facts such as $\alpha<k^{(0)}_1$ and $k^{(BC)}_2<(1-2\alpha)^2/(2-5\alpha)$ are needed to know which row a region lies in. One inclusion the proof uses is only shown in the paper's figure: on $\Omega^{(BC)}_1$, where condition (2a) holds, one needs $k>k^*$ in order to conclude that (2b) fails. At the region boundaries $k=(1-\alpha)/2$ and $k=k^{(AB)}_1$ several of the proof's strict inequalities are equalities.

Formalization scope

Everything is stated over the reals in the namespace EndogMerger.SymLoyal. All definitions take explicit parameters (α k r : ℝ). The standing assumptions $0<\alpha<1/3$, $\alpha<k$, $r>0$, and $k<1$ or $k<1-2\alpha$ as each statement requires, are hypotheses of each theorem. Relative to the paper, $0<\alpha$ replaces $0\le\alpha$ (every region of the analysis has $\alpha>0$), and $r>0$ is made explicit. Firm $A$'s capacity $k_A\ge 1-2\alpha$ does not enter Table A1 and is not modelled. The split of $\Pi^{(AB)}$ between $A$ and $B$ is left unspecified, as in the paper.

Table A1 is the definition. The profits and lower bounds are defined by Table A1's piecewise expressions, row by row, with max where the table has a maximum. The paper's derivation of these values as equilibrium outcomes of a mixed-strategy price game with random rationing is not formalized; Section 6 of the paper itself obtains Proposition 3 from the Table A1 profits. The paper's PDF page numbers are cited throughout; the appendix restarts its printed numbering, so printed page numbers are not used.

Three trivializing formalizations are ruled out. The profits are not defined by the closed forms of Lemmas 3–5, which would make those lemmas definitional. The equilibrium predicate for $\{A,B,C\}$ requires that neither condition (1) nor condition (2) holds, so the goal includes the claim that the small merger is never an equilibrium. The thresholds $\alpha^{(0)}_1$ and $\alpha^{(BC)}_1$ are not defined by the paper's equation $k_1(\alpha_1)=k_2(\alpha_1)$, which Real.sqrt satisfies for every $\alpha$ with a negative radicand. Instead $\alpha^{(BC)}_1=(11-\sqrt{17})/52$, and $\alpha^{(0)}_1$ is a parameter pinned as the root in $(0,1/3)$ of $-43\alpha^3+43\alpha^2-13\alpha+1$.

Where the paper's proof claims a strict inequality on a closed region whose boundary gives equality, the milestone states it on the open region, and its Formalization Note says so.

No library beyond Mathlib's real arithmetic and Real.sqrt is needed. Lemmas about the threshold curves, for example that $k^{(AB)}_1(\alpha)$ lies in $(\alpha,(1-\alpha)/2)$, are reusable across milestones. Contributions of intermediate lemmas, including the region inclusion $\Omega^{(BC)}_1\subseteq\{k>k^*\}$, are welcome.

Selected references

• D. Wang, X. Wu, C. S. Tang, Y. Dai, Endogenous Merger Decisions Among Competitors: Impact of Limited Capacity and Loyal Segments, Management Science, 2024. https://doi.org/10.1287/mnsc.2022.01943
• H. R. Varian, A Model of Sales, American Economic Review 70(4), 1980. https://www.jstor.org/stable/1803558
• S. W. Salant, S. Switzer, R. J. Reynolds, Losses from Horizontal Merger: The Effects of an Exogenous Change in Industry Structure on Cournot–Nash Equilibrium, Quarterly Journal of Economics 98(2), 1983. https://doi.org/10.2307/1885626

Motivation

In centralized labour markets such as the US National Resident Matching Program, doctors are assigned to hospital residency positions by a mechanism that produces a stable matching. There are more positions than doctors, so some hospitals end up with empty positions; these are typically rural hospitals, which are less sought after than urban ones. This raised the question of whether a different mechanism could help these hospitals (Roth 1986). The rural hospitals theorem answers this negatively, provided all preferences are strict.

Timeline.

• 1970: McVitie and Wilson prove the one-to-one case (each hospital has one position): all stable matchings match the same doctors and the same hospitals (doi:10.1007/BF01934199).
• 1984: Roth proves Part 1 for many-to-one markets: the set of assigned doctors and the number of filled positions at each hospital are the same in all stable matchings (doi:10.1086/261272).
• 1986: Roth proves Part 2: a hospital with an empty position in some stable matching receives exactly the same doctors in all stable matchings (doi:10.2307/1913160).
• 2014: Klijn and Yazıcı extend the theorem to many-to-many matching (doi:10.1016/j.jmateco.2014.09.003).

Setting

A market has a finite set $D$ of doctors and a finite set $H$ of hospitals; hospital $h$ has $q_h$ positions. Every doctor strictly ranks the hospitals together with the option of staying unmatched, and every hospital strictly ranks the doctors together with the option of leaving a position empty. An assignment $\mu$ sends each doctor to a hospital or to nothing; $\mu(h)$ is the set of doctors at $h$. It is a matching if $|\mu(h)|\le q_h$ for every $h$.

A matching is stable if (i) no doctor is placed at a hospital she ranks below staying unmatched, and no hospital holds a doctor it ranks below an empty position, and (ii) there is no blocking pair $(d,h)$: a doctor $d$ who prefers $h$ to her assignment, while $h$ finds $d$ acceptable and either has an empty position or prefers $d$ to one of its current doctors.

Formalization targets

Goal: the rural hospitals theorem

For any two stable matchings $\mu,\nu$:

$$\mu(d)\ne\varnothing \iff \nu(d)\ne\varnothing\ \ (d\in D),\qquad |\mu(h)|=|\nu(h)|\ \ (h\in H),\qquad |\mu(h)|<q_h \implies \nu(h)=\mu(h).$$

Milestones

1. One position per hospital: a doctor unmatched in one stable matching is unmatched in every stable matching.
2. One position per hospital: a hospital unmatched in one stable matching is unmatched in every stable matching.
3. Part 1: the same doctors are assigned, and every hospital fills the same number of positions, in all stable matchings.
4. Part 2: a hospital with an empty position in some stable matching receives the same set of doctors in all stable matchings.

Significance

The result itself. Changing the matching mechanism, as long as it outputs stable matchings, cannot give under-subscribed hospitals more doctors or different doctors, and cannot change which doctors are employed. Hence policy aimed at rural hospitals must change preferences, capacities, or abandon stability, not merely switch between stable mechanisms.

Formalizing it. The theorem is classical and proved in the cited papers; this mission asks for a machine-checked proof in Lean 4 with Mathlib, for the general many-to-one model with capacities and acceptability, together with the one-position special case.

Difficulty

Comparing two stable matchings one agent at a time does not work: a single doctor moving between hospitals says nothing about how many positions each hospital fills, and the statements concern every agent of the market simultaneously. Stability of both matchings has to be used at once, and Part 2 is strictly stronger than Part 1 (equal numbers of doctors at an under-filled hospital do not imply equal sets of doctors). The existence of a stable matching is not needed for these statements.

Formalization scope

Doctors and hospitals are finite types D, H. Preferences are injective rank functions on Option H (for a doctor) and Option D (for a hospital), smaller rank meaning more preferred and none meaning unmatched or an empty position; injectivity encodes strictness. Hospital preferences over groups are responsive. Capacities are natural numbers and may be zero. An assignment is μ : D → Option H. Stability is Market.IsStable: capacity constraints, individual rationality, and no blocking pair. All statements quantify over arbitrary stable matchings, so they are not vacuous: stable matchings exist in every such market (Gale–Shapley), though existence is not part of this mission.

Contributions welcome: proofs of the milestones, an existence theorem for stable matchings in this model, and lemmas about stable matchings reusable in other matching missions.

Selected references

• D. G. McVitie, L. B. Wilson, Stable marriage assignment for unequal sets, BIT Numerical Mathematics 10 (1970) 295–309. https://doi.org/10.1007/BF01934199
• A. E. Roth, The evolution of the labor market for medical interns and residents: a case study in game theory, Journal of Political Economy 92 (1984) 991–1016. https://doi.org/10.1086/261272
• A. E. Roth, On the allocation of residents to rural hospitals: a general property of two-sided matching markets, Econometrica 54 (1986) 425–427. https://doi.org/10.2307/1913160
• F. Klijn, A. Yazıcı, A many-to-many 'rural hospital theorem', Journal of Mathematical Economics 54 (2014) 63–73. https://doi.org/10.1016/j.jmateco.2014.09.003
• Wikipedia, Rural hospitals theorem, revision 1064508418. https://en.wikipedia.org/w/index.php?title=Rural_hospitals_theorem&oldid=1064508418

Motivation

The stable matching problem asks for a pairing between two equally sized groups in which no two participants would both rather be matched with each other than with their assigned partners. It was posed and solved by Gale and Shapley in 1962 in the context of college admissions and marriage (Gale–Shapley 1962). Their deferred acceptance algorithm underlies centralized clearinghouses such as the assignment of graduating medical students to hospital residencies, and the theory of stable allocations was recognized by the 2012 Nobel Memorial Prize in Economic Sciences awarded to Shapley and Roth.

Timeline of the results targeted here:

• 1962 — Gale and Shapley: a stable matching always exists, and the men-proposing deferred acceptance algorithm finds one; its outcome is the best stable matching for every man.
• 1971 — McVitie and Wilson: the men-optimal stable matching is simultaneously the worst stable matching for every woman.
• 1981–1982 — Dubins–Freedman and Roth: the men-proposing algorithm is strategy-proof (indeed group strategy-proof) for men, while women can gain by misreporting.
• 1987 — Gusfield (after Knuth and Conway): the stable matchings of an instance form a finite distributive lattice.

Setting

Fix $n \ge 0$. There are $n$ men and $n$ women, both indexed by $\mathrm{Fin}\,n$. Each man $m$ ranks all women strictly: $\mathrm{manRank}_m(w) \in \mathrm{Fin}\,n$ is the position of $w$ in $m$'s list, position $0$ being most preferred; symmetrically each woman $w$ has $\mathrm{womanRank}_w$. Both are bijections. A matching is a bijection $\mu$ from men to women. A pair $(m, w)$ blocks $\mu$ if $\mathrm{manRank}_m(w) < \mathrm{manRank}_m(\mu(m))$ and $\mathrm{womanRank}_w(m) < \mathrm{womanRank}_w(\mu^{-1}(w))$; $\mu$ is stable if no pair blocks it.

The Gale–Shapley algorithm runs in rounds. A state records, for every man, how many women he has proposed to so far, and for every woman, her current provisional fiancé (if any). In each round every unengaged man proposes to the most preferred woman he has not yet proposed to, and every woman keeps the most preferred among her current fiancé and this round's suitors, rejecting the others. The Gale–Shapley outcome is the matching read off from the state after $n^2$ rounds.

Formalization targets

Goal: the algorithm produces a stable matching

$$\forall I,\ \exists \mu,\ \mu \text{ is the Gale–Shapley outcome of } I \ \wedge\ \mu \text{ is stable for } I.$$

This contains termination (all men are engaged after $n^2$ rounds), the fact that the final engagements form a bijection, and stability.

Milestones

1. Termination: after $n^2$ rounds every man is engaged.
2. Existence: every instance has a stable matching.
3. Man-optimality: for the Gale–Shapley outcome $\mu_0$ and every stable $\mu$, $\mathrm{manRank}_m(\mu_0(m)) \le \mathrm{manRank}_m(\mu(m))$ for every man $m$.
4. Woman-pessimality: $\mathrm{womanRank}_w(\mu^{-1}(w)) \le \mathrm{womanRank}_w(\mu_0^{-1}(w))$ for every woman $w$.
5. Truthfulness for men: no single man obtains a strictly better partner (by his true list) by misreporting.
6. Group strategy-proofness for men: no nonempty coalition of men can misreport so that all its members are strictly better off.
7. Weak coalitional manipulation: some coalition can misreport so that some members are strictly better off and the rest keep their partners.
8. Women can manipulate: some woman can obtain a strictly better partner by misreporting.
9. The 3×3 example: the instance $A: YXZ$, $B: ZYX$, $C: XZY$, $X: BAC$, $Y: CBA$, $Z: ACB$ has exactly the three stable matchings $(AY,BZ,CX)$, $(AX,BY,CZ)$, $(AZ,BX,CY)$.
10. Lattice structure: the stable matchings of any instance form a distributive lattice under "every man weakly prefers".

Significance

Existence of stable matchings is the foundation of two-sided matching theory, and the algorithmic proof is constructive. Man-optimality and woman-pessimality show that the proposing side is systematically favored, which is the reason the choice of proposing side matters in practice, as in the 1995 redesign of the residency match. The incentive results (milestones 5–8) explain why participants on the proposing side can safely report their true preferences while the receiving side cannot, and the lattice structure underlies efficient algorithms for enumerating and optimizing over stable matchings.

All results in this mission are classical and proved in the literature. The work here is formalization: a precise model of the round-based algorithm, machine-checked proofs of its correctness and optimality, and the incentive properties, which are usually argued informally.

Difficulty

The goal requires reasoning about an iterated state transformer rather than an abstract existence statement. The step that is usually waved away is the invariant that an unengaged man still has a woman left to propose to, which is what makes the $n^2$ bound and the bijectivity of the final engagements work. Man-optimality needs the invariant that no man is ever rejected by a woman who is his partner in some stable matching, which is not visible from the output alone. Group strategy-proofness is substantially harder than individual truthfulness: the known proofs go through a "blocking lemma" about matchings that are weakly preferred by all men.

Formalization scope

Men and women are Fin n; preferences are strict total orders given as rank bijections Fin n ≃ Fin n; matchings are bijections Fin n ≃ Fin n. The algorithm is the round-based version described in the source: all unengaged men propose simultaneously in each round. The algorithm's output is fixed as the state after exactly $n^2$ rounds; termination within that bound is itself a milestone, so a wrong bound would make the goal false rather than vacuous. The case $n = 0$ is included and is trivial. Incentive results compare Gale–Shapley outcomes of two instances that differ only in the lists of the deviating participants, with gains measured by the deviators' true lists.

The definitions are reusable for further missions on the same article (rural hospitals theorem, hospitals/residents problem). Contributions welcome: invariants of the algorithm, the blocking lemma, and alternative proofs of existence.

Selected references

• D. Gale, L. S. Shapley, College Admissions and the Stability of Marriage, American Mathematical Monthly 69(1), 1962, 9–14. https://doi.org/10.2307/2312726
• D. G. McVitie, L. B. Wilson, The stable marriage problem, Communications of the ACM 14(7), 1971, 486–490. https://doi.org/10.1145/362619.362631
• L. E. Dubins, D. A. Freedman, Machiavelli and the Gale–Shapley Algorithm, American Mathematical Monthly 88(7), 1981, 485–494. https://doi.org/10.2307/2321753
• A. E. Roth, The Economics of Matching: Stability and Incentives, Mathematics of Operations Research 7(4), 1982, 617–628. https://doi.org/10.1287/moor.7.4.617
• D. Gusfield, Three fast algorithms for four problems in stable marriage, SIAM Journal on Computing 16(1), 1987, 111–128. https://doi.org/10.1137/0216010
• Wikipedia, Stable matching problem. https://en.wikipedia.org/wiki/Stable_matching_problem

Motivation

In a game, each participant chooses a strategy while the cost of that choice depends on what everyone else does. A network user may choose a route, for example, but its travel time depends on the routes chosen by other users. The price of anarchy compares the cost of self-interested outcomes with the best joint outcome. A guarantee restricted to a Nash equilibrium leaves open what happens when players repeatedly adapt their choices without settling on any equilibrium. Roughgarden's extension theorem addresses sequences produced by players whose accumulated costs are asymptotically competitive with fixed alternatives. Its bound depends on a property of the game, rather than on a particular learning algorithm or on convergence of play. Roughgarden, §§1 and 3.2.

Setting

There is a finite set of players $i$, and player $i$ has a strategy set $S_i$. These sets may be infinite. An outcome $s$ specifies one strategy $s_i\in S_i$ for every player. The real number $C_i(s)$ is player $i$'s cost, and the joint cost is $C(s)=\sum_i C_i(s)$. The paper treats this objective as nonnegative. If player $i$ alone changes to the strategy $s'_i$ of another outcome $s'$, its cost is written $C_i(s'_i,s_{-i})$; every other player's strategy stays as in $s$. Roughgarden, §2.1.

A game is $(\lambda,\mu)$-smooth if every pair $s,s'$ satisfies $\sum_i C_i(s'_i,s_{-i})\leq\lambda C(s')+\mu C(s)$. The robust price of anarchy $\rho(G)$ is the infimum of $\lambda/(1-\mu)$ over all such smoothness pairs with $\mu<1$. This number packages every bound obtainable from the same smoothness condition. It is taken in the extended reals, with value $+\infty$ when no pair exists; the mission assumes an admissible pair exists, so it is below $+\infty$. Roughgarden, Definitions 2.1–2.2.

For a played outcome $s^t$ at time $t$ and a comparison outcome $s'$, define the hypothetical improvement $\delta_i(s^t;s')=C_i(s^t)-C_i(s'_i,s^t_{-i})$. A player has vanishing average external regret when its average cost, up to an error tending to zero, is no greater than the average cost it would have paid by using any one fixed strategy throughout the first $T$ rounds. The comparison strategy is held fixed across time, while the other players' strategies may change on every round. Each player may have its own error function. Roughgarden, (22), (24).

Formalization targets

Additive bound

The paragraph following equation (25) asserts a bound with a vanishing additive error. For any comparison outcome $s'$ and every horizon $T\geq1$, there is a function $\eta(T)\to0$ with

$$\frac1T\sum_{t=1}^{T}C(s^t)\leq\rho(G)C(s')+\eta(T).$$

This target includes the case $C(s')=0$. The paper states the conclusion for an optimal outcome; the same displayed relations also apply to any comparison outcome. Relations (23) and (25) are separate milestones: the former bounds one outcome using the players' hypothetical improvements, and the latter averages that bound over time. Roughgarden, §3.2, pp. 13–14.

Multiplicative repeated-play bound

The mission goal is Theorem 3.3's multiplicative presentation. For a comparison outcome with $C(s')>0$, there is a function $\eta(T)\to0$ such that

$$\frac1T\sum_{t=1}^{T}C(s^t)\leq\bigl(\rho(G)+\eta(T)\bigr)C(s')\qquad(T\geq1).$$

The positive-cost condition is needed to make the printed statement true. Consider one player with strategies of costs $1$ and $0$, playing the costly strategy once and the zero-cost strategy thereafter. Its average regret tends to zero, but its average cost is $1/T>0$ at every finite horizon. Taking the zero-cost strategy as $s'$ makes the right-hand side of the printed multiplicative bound zero for any $\eta$. The additive milestone preserves the valid zero-cost case. Roughgarden, Theorem 3.3 and the paragraph preceding it.

Significance

The result transfers a bound defined by the game's smoothness condition to repeated play even when the sequence does not converge. It therefore gives a welfare guarantee for the behavior captured by vanishing external regret without identifying which learning rule generated the sequence. The additive statement also records exactly what remains true when an optimal outcome has zero cost. Roughgarden, §3.2.

Formalizing the result makes the quantifiers behind $o(1)$ explicit: for each fixed game, sequence, and comparison outcome, one error sequence works across all positive horizons and tends to zero. The development also distinguishes the paper's valid additive consequence from its multiplicative display at zero cost. The paper proves the result mathematically; the Lean files in this mission are theorem statements for solvers and do not yet contain machine-checked proofs.

Difficulty

For a fixed smoothness pair, a finite-time inequality controls average joint cost by the comparison cost and players' average hypothetical improvements. Regret controls those improvements asymptotically, but the robust price of anarchy takes an infimum over all admissible pairs. Passing from bounds for individual pairs to that infimum requires the sign and boundedness conditions on the joint cost to be tracked correctly. A direct replacement of the fixed pair's ratio by $\rho(G)$ does not itself justify the limit. The zero-cost example also shows why an additive error cannot simply be displayed as a multiplicative $o(1)$ term in every case. Roughgarden, (23)–(25) and Theorem 3.3.

Formalization scope

Lean uses a finite type of players, arbitrary strategy types, and real-valued player costs. It defines the joint objective by the finite sum $\sum_i C_i(s)$; it does not assume that each individual cost is nonnegative. The goal and additive milestone assume that the joint objective is nonnegative at every outcome, matching the paper's standing convention. They also assume at least one smoothness pair with $\mu<1$, the case in which $\rho(G)=+\infty$ and the page's bound is vacuous. $\rho(G)$ is an extended-real infimum and the inequalities are compared in the extended reals. For a nonnegative game with an admissible pair, $\rho(G)$ is a real number at least 1 when some outcome has positive cost; if all outcomes cost zero, the target cost bounds are zero. Roughgarden, §§1, 2.1, 3.2.

Time indices are $1,\ldots,T$, with $T\geq1$. The Lean sequence is infinite so that the asymptotic assertion concerns prefixes of one sequence; its value at index zero is unused. The regret definition quantifies over every fixed alternative strategy rather than assuming a minimum is attained when a strategy set is infinite. A separate vanishing error sequence may be chosen for each player. The conclusion chooses one vanishing error sequence after the game, play sequence, and comparison outcome, and uses it at every horizon. These choices make the $o(1)$ terms genuine limits, rather than unconstrained values chosen separately for each $T$. Roughgarden, (24), Theorem 3.3.

The game objective, smoothness predicate, robust price of anarchy, deviation improvement, and regret predicate are the reusable definitions. Solvers can contribute proofs of the one-step bound, its averaged form, the additive conclusion, and the main theorem. Mixed-outcome sequences from Remark 3.4 are outside this mission's core; their probability and integrability conventions would require another definition layer.

Selected references

• Tim Roughgarden, Intrinsic Robustness of the Price of Anarchy, Journal of the ACM 62(5), Article 32, 2015. DOI: 10.1145/2806883. Statements and page numbers follow the author's final version dated July 14, 2015.

Motivation

The price of anarchy (POA) of a game measures how much selfish behaviour costs: it is the ratio between the largest cost of an equilibrium and the cost of an optimal outcome, for a nonnegative objective such as the sum of the players' costs. Since Koutsoupias and Papadimitriou (1999) and Roughgarden and Tardos (2002), POA bounds have been proved for routing, scheduling, facility location, auctions and many other models, mostly for pure Nash equilibria.

Pure Nash equilibria need not exist, are hard to compute in general, and are not what players running learning algorithms converge to. A bound that holds only at pure Nash equilibria therefore says little about realized play. Roughgarden's paper (J. ACM 62(5), 2015; conference version STOC 2009) observes that most known POA proofs follow one template, the smoothness argument, and proves that any bound obtained this way extends automatically to much broader equilibrium concepts. This mission formalizes the static half of that result: the extension to coarse correlated equilibria (Theorem 3.2) and to their approximate versions (Theorem 4.1).

Timeline:

• 1999: Koutsoupias and Papadimitriou introduce the worst-case ratio of equilibria to optimum.
• 2005: Awerbuch–Azar–Epstein and Christodoulou–Koutsoupias prove the bound 5/2 for linear congestion games; their arguments are smoothness arguments in hindsight.
• 2009: Roughgarden (STOC) isolates smoothness and proves the extension theorems; the journal version (2015) adds the tightness results for congestion games.
• 2009–2015: smoothness is adapted to auctions (Syrgkanis–Tardos 2013) and to local and approximate variants.

Setting

A cost-minimization game has finitely many players $i$. Player $i$ chooses a strategy $s_i$ from an arbitrary set $S_i$; an outcome is a vector $s = (s_i)_i$, and player $i$ pays a real cost $C_i(s)$. Write $(s_i', s_{-i})$ for the outcome in which player $i$ switches to $s_i'$ and the others stay put. The joint cost is $C(s) = \sum_i C_i(s)$, assumed nonnegative.

An outcome $s$ is a pure Nash equilibrium if $C_i(s) \le C_i(s_i', s_{-i})$ for every $i$ and $s_i' \in S_i$. For $\epsilon \ge 0$ it is an $\epsilon$-Nash equilibrium if $C_i(s) \le (1+\epsilon) C_i(s_i', s_{-i})$.

A coarse correlated equilibrium is a probability distribution $\sigma$ over outcomes with

$$\mathbf{E}_{s\sim\sigma}[C_i(s)] \le \mathbf{E}_{s\sim\sigma}[C_i(s_i', s_{-i})] \quad\text{for every } i \text{ and } s_i' \in S_i,$$

and an $\epsilon$-coarse correlated equilibrium satisfies the same with a factor $(1+\epsilon)$ on the right. Every pure Nash, mixed Nash and correlated equilibrium is a coarse correlated equilibrium, and coarse correlated equilibria are exactly the limits of play in which every player has vanishing external regret.

The game is $(\lambda,\mu)$-smooth if for every two outcomes $s, s^*$

$$\sum_i C_i(s_i^*, s_{-i}) \le \lambda\, C(s^*) + \mu\, C(s).$$

The robust price of anarchy is $\rho(G) = \inf\{\lambda/(1-\mu) : \mu < 1,\ G \text{ is } (\lambda,\mu)\text{-smooth}\}$.

Formalization targets

Goal: Theorem 3.2 (static extension theorem)

For every game $G$ with robust POA $\rho(G)$, every coarse correlated equilibrium $\sigma$ and every outcome $s^*$,

$$\mathbf{E}_{s\sim\sigma}[C(s)] \le \rho(G)\cdot C(s^*).$$

Milestones

1. Claim (3)–(5), p. 5: in a $(\lambda,\mu)$-smooth game with $\lambda > 0$, $\mu < 1$, every pure Nash equilibrium $s$ satisfies $C(s) \le \frac{\lambda}{1-\mu} C(s^*)$ for an optimal $s^*$.
2. §4.1, p. 16: every $\epsilon$-Nash equilibrium satisfies $C(s) \le \frac{(1+\epsilon)\lambda}{1-\mu(1+\epsilon)} C(s^*)$ for an optimal $s^*$.
3. The chain (16)–(21), p. 13: for one fixed pair $(\lambda,\mu)$ with $\mu < 1$, $\mathbf{E}_{s\sim\sigma}[C(s)] \le \frac{\lambda}{1-\mu} C(s^*)$ for every coarse correlated equilibrium $\sigma$ and every outcome $s^*$.
4. Theorem 4.1, p. 16: for every $\epsilon$-coarse correlated equilibrium,

$$\mathbf{E}_{s\sim\sigma}[C(s)] \le \frac{(1+\epsilon)\lambda}{1-\mu(1+\epsilon)}\cdot C(s^*).$$

Significance

Theorem 3.2 says that the robust POA of a game bounds the expected cost of every coarse correlated equilibrium, which contains every other equilibrium concept in the hierarchy. Combined with the companion result for no-regret sequences (Theorem 3.3, mission II of this series), it makes POA bounds meaningful for learning dynamics: whenever players use no-regret algorithms, their average cost is within the robust POA of optimal. For linear congestion games, which are $(5/3, 1/3)$-smooth, it yields the bound $5/2$ for all coarse correlated equilibria at once. Theorem 4.1 shows that the bounds degrade gracefully when the equilibrium condition holds only approximately, which covers equilibria computed to finite accuracy.

The results are proved in the paper; their proofs are short. No machine-checked version is known to exist. The mission's value is a reusable, platform-wide definition layer for cost-minimization games, smoothness, the robust POA and the equilibrium hierarchy, on which later results can be stated: the bicriteria bounds of §4.2, the tightness theorem for congestion games (mission III), and smoothness bounds for specific models such as auctions, routing and scheduling.

Difficulty

The mathematics is linear: it uses only linearity of expectation and one rearrangement. The difficulty lies in the encoding. The robust POA is an infimum over a set that may be empty (then $\rho(G) = +\infty$ on the page) and need not be attained. Passing from the fixed-pair bound to the infimum uses $C(s^*) \ge 0$. Theorem 4.1's printed side condition $\epsilon < 1/\mu - 1$ is meaningless when $\mu = 0$ and reverses its meaning when $\mu < 0$. Each of these must be handled so that the formal statement is neither false nor vacuous.

Formalization scope

Players form a finite type with decidable equality, and strategy sets are arbitrary types with no finiteness assumed. Outcomes are dependent functions, and the deviation $(s_i', s_{-i})$ is Function.update s i s'ᵢ. Costs are real-valued, and $\lambda, \mu$ are unconstrained reals except $\mu < 1$. Probability distributions are finitely supported weight functions that are nonnegative with total mass $1$. Expectations are therefore finite sums with no integrability side conditions. This covers all finite games and all mixed and correlated equilibria of finite games, but not distributions with infinite support.

The robust POA is an extended-real (EReal) infimum over the smoothness pairs with $\mu < 1$, so it is $+\infty$ when no such pair exists, and the goal compares the expected cost with $\rho(G)\cdot C(s^*)$ in EReal. The goal carries two explicit hypotheses:

• the joint cost is nonnegative, which is the paper's standing assumption (§1, p. 2; §2.4, p. 10);
• some smoothness pair with $\mu < 1$ exists, so that $\rho(G) < +\infty$.

Without the second, a game with no smoothness pair and $C(s^*) = 0$ would be claimed to have expected cost at most $0$ (EReal sets $(+\infty)\cdot 0 = 0$), which the page does not assert. A formalization in which the distribution may have total mass $0$, or in which $\rho(G)$ is an infimum over all pairs rather than over the smoothness pairs with $\mu < 1$, trivializes or falsifies the goal, and is ruled out by the definitions.

In Theorem 4.1 and the $\epsilon$-Nash bound:

• "$\epsilon < 1/\mu - 1$" is encoded as $\mu(1+\epsilon) < 1$, which agrees with it for $0 < \mu < 1$;
• $\epsilon \ge 0$ is assumed, the implicit domain of an approximation parameter.

The $\epsilon$-coarse correlated equilibrium is the extension of (15) that the paper says is "defined in the same way" as $\epsilon$-Nash equilibria (p. 15). Remark 4.4 writes out the payoff analogue.

Claim (3)–(5) and the $\epsilon$-Nash bound keep the paper's hypotheses $\lambda > 0$ and optimality of $s^*$, although the inequalities hold without them. Example 4.2 is not posed: its printed bound $(5-5\epsilon)/(2-\epsilon)$ should read $(5+5\epsilon)/(2-\epsilon)$.

Contributions welcome:

• proofs of the four milestones and of the goal;
• a measure-theoretic version for distributions with infinite support, with explicit integrability hypotheses;
• reuse of the definitions in other smoothness results.

Selected references

• T. Roughgarden, Intrinsic Robustness of the Price of Anarchy, J. ACM 62(5), Article 32, 2015. https://doi.org/10.1145/2806883
• T. Roughgarden, Intrinsic Robustness of the Price of Anarchy, Proc. 41st ACM STOC, 513–522, 2009. https://doi.org/10.1145/1536414.1536485
• E. Koutsoupias, C. Papadimitriou, Worst-Case Equilibria, Proc. STACS, LNCS 1563, 404–413, 1999. https://doi.org/10.1007/3-540-49116-3_38
• G. Christodoulou, E. Koutsoupias, The Price of Anarchy of Finite Congestion Games, Proc. 37th ACM STOC, 67–73, 2005. https://doi.org/10.1145/1060590.1060600
• B. Awerbuch, Y. Azar, A. Epstein, The Price of Routing Unsplittable Flow, Proc. 37th ACM STOC, 57–66, 2005. https://doi.org/10.1145/1060590.1060599
• V. Syrgkanis, É. Tardos, Composable and Efficient Mechanisms, Proc. 45th ACM STOC, 211–220, 2013. https://doi.org/10.1145/2488608.2488635