Algorithmic Game Theory

Motivation

Rank-order competitions — sports tournaments, poker final tables, golf tours, crowdsourcing contests, sales leagues — end with a ranking of the participants and a pot of prize money that has to be split according to that ranking. Organisers publish prize tables that change with the number of entrants and with the size of the purse, and these tables are usually justified only by tradition. Dietzenbacher and Kondratev (arXiv:2008.08985v2, published in Management Science 2023, doi:10.1287/mnsc.2022.4520) take the axiomatic approach of fair-division theory and ask which prize allocation rules are characterised by natural requirements of fairness and coherence across competitions of different sizes.

Consistency — invariance of a rule under "re-running the allocation" for a subgroup with the money it collectively received — has a long history in axiomatic allocation: bankruptcy problems (Aumann and Maschler 1985), taxation (Young 1987), bargaining (Lensberg 1987, 1988) and cooperative games (Peleg 1986; Hart and Mas-Colell 1989). The paper applies it to competitions. Full consistency together with order preservation and endowment monotonicity yields the interval rules (Theorem 1); weakening consistency to local consistency yields the single-parametric rules (Theorem 2). This mission concerns the weakest version, top consistency, which only constrains the top segment of the ranking and describes real prize schemes such as the golf tournament of Table 1(b) of the paper. It is the third mission of a series on this paper; the first two treat Theorems 1 and 2.

Setting

Fix a countable set $U$ of at least three potential competitors. A competition $(N,\mathcal R,E)$ consists of a finite nonempty set $N\subseteq U$, a ranking $\mathcal R:N\to\{1,\dots,|N|\}$ (a bijection; competitor $i$ is ranked above $j$ when $\mathcal R(i)<\mathcal R(j)$), and a prize endowment $E\ge0$. For $S\subseteq N$ the subranking $\mathcal R_S:S\to\{1,\dots,|S|\}$ orders $S$ as $\mathcal R$ does.

A prize allocation rule $\varphi$ assigns to each competition a vector $\varphi(N,\mathcal R,E)\in\mathbb R_+^N$ with $\sum_{i\in N}\varphi_i(N,\mathcal R,E)=E$. The axioms are:

• anonymity: $\varphi_i(N,\mathcal R,E)=\varphi_j(N',\mathcal R',E)$ whenever $|N|=|N'|$ and $\mathcal R(i)=\mathcal R'(j)$;
• order preservation: $\mathcal R(i)<\mathcal R(j)$ implies $\varphi_i\ge\varphi_j$;
• winner strict endowment monotonicity: if $E<E'$ then $\varphi_i(N,\mathcal R,E)\le\varphi_i(N,\mathcal R,E')$ for all $i$, strictly for the winner $\mathcal R(i)=1$;
• top consistency: for each $S\subseteq N$ with $\mathcal R(i)\le|S|$ for every $i\in S$, and each $i\in S$,

$$\varphi_i(N,\mathcal R,E)=\varphi_i\Big(S,\mathcal R_S,\sum_{j\in S}\varphi_j(N,\mathcal R,E)\Big).$$

A rule is parametric if there are continuous non-decreasing $f_1,f_2,\dots:\mathbb R_+\to\mathbb R_+$ with $f_1(x)=x$ and $f_{k+1}(x)\le f_k(x)$ such that $\varphi_i(N,\mathcal R,E)=f_{\mathcal R(i)}(x)$, where $x\ge0$ solves $\sum_{k=1}^{|N|}f_k(x)=E$. The winner gets $x$ and position $k$ gets $f_k(x)$. Equal Division ($f_k(x)=x$) and Winner-Takes-All ($f_k=0$ for $k\ge2$) are parametric.

Formalization targets

Goal: Theorem 3 (p. 22)

$$\varphi \text{ is anonymous, order preserving, winner strictly endowment monotonic and top consistent}\iff\varphi\text{ is a parametric rule.}$$

Both directions are part of the goal.

Milestones (proof of Theorem 3, pp. 32–33)

1. Every parametric rule satisfies the four axioms (the "readily checked" direction).
2. Under order preservation, endowment continuity and winner strict endowment monotonicity, the winner's prize $E\mapsto\varphi_1(N,\mathcal R,E)$ is strictly increasing, continuous and unbounded on $\mathbb R_+$, so each $x\ge0$ is the winner's prize for exactly one $E$.
3. The induction step: a representation $f_1,\dots,f_n$ valid on all competitions with at most $n$ competitors extends, by a new continuous non-decreasing $f_{n+1}\le f_n$, to all competitions with $n+1$ competitors.

Lemma 1 of the paper (endowment monotonicity implies endowment continuity, p. 10) is used in the proof; it is formalized in the first mission of this series and will be referenced from there.

Companion: Corollary 8 (p. 22)

Replacing winner strict endowment monotonicity by endowment additivity (equivalently scale invariance) characterises the proportional rules $\varphi_i=\lambda_{\mathcal R(i)}E/\sum_{k\le|N|}\lambda_k$ with $\lambda_1>0$ and $\lambda_{k+1}\le\lambda_k$.

Significance

Theorem 3 says that the four axioms leave exactly one degree of freedom per position: a monotone function of the winner's prize. This gives organisers a complete menu of prize schemes that are fair in the anonymous, order-preserving sense and that keep the top of the table unchanged when lower-ranked entrants leave — the property that matters when competitors are eliminated one at a time and paid at the moment of elimination. It contains the single-parametric rules of Theorem 2, the Winner-Takes-Surplus rules, the geometric rules and the proportional rules (Corollary 8) as special cases, and the paper shows in a Remark (p. 33) that the four axioms are logically independent.

The theorem is proved in the paper; to our knowledge no part of it has been machine-checked. The formalization adds a reusable layer for variable-population allocation problems — rankings of finite subsets of a fixed universe, subrankings, and consistency axioms restricted to families of subsets — that is not in Mathlib. Formal proofs of both directions, of the milestones, and of Corollary 8 are all welcome.

Difficulty

The "if" direction is a computation, but it requires showing that the parameter $x$ is well defined and moves monotonically with $E$, which uses $f_1(x)=x$ and the intermediate value theorem. The "only if" direction must construct the functions $f_k$ from an abstract rule. The natural first idea — define $f_k(x)$ as the prize of position $k$ when the winner receives $x$ — needs the winner's prize to be invertible as a function of $E$, which uses continuity (supplied by Lemma 1, not assumed), strict monotonicity only for the winner, and unboundedness, which comes from order preservation together with exhaustion of the endowment. Top consistency then has to transfer the representation from competitions of size $n$ to size $n+1$, and anonymity has to transfer it from one ranked set to every other one of the same size; the induction over the number of competitors must keep all smaller sizes, since top consistency reduces to every top segment.

Formalization scope

• A ranked set $(N,\mathcal R)$ is a duplicate-free nonempty List U, best competitor first; $\mathcal R(i)$ is the 1-based index pos l i, and $\mathcal R_S$ is the sublist of entries in $S$. $U$ is an arbitrary type with decidable equality; the paper's standing assumptions (countable, at least three elements) are hypotheses of the goal and of Corollary 8, and are omitted from milestones that do not use them.
• A rule is a function φ : List U → ℝ → U → ℝ; it is required to be a prize allocation rule (nonnegative prizes summing to $E$) on rankings and $E\ge0$, and every axiom quantifies only over that domain. Endowments are reals with $E\ge0$.
• The representation $f_1,f_2,\dots$ is f : ℕ → ℝ → ℝ, indexed from 1 as on the page ($f_0$ unused); continuity, monotonicity, nonnegativity and $f_1(x)=x$ are required on $[0,\infty)$. The parameter $x$ is given existentially; it is unique, so this is the page's "where $x\in\mathbb R_+$ is such that".
• Endowment continuity is coordinatewise continuity on $[0,\infty)$.

Trivializing formalizations are ruled out: rules act on every finite ranked subset of $U$, not on a fixed competitor set; top consistency quantifies over exactly the top segments (full or local consistency would change the theorem — the rule of Example 6 is parametric but not locally consistent); the goal is a biconditional; the parametric family includes $f_1=\mathrm{id}$, the decreasing chain $f_{k+1}\le f_k$, and continuity of every $f_k$.

Corollary 7 of the paper is not included: its "only if" parts ("for each $k$") fail as written when $U$ is finite, since $f_k$ for $k>|U|$ is not determined by the rule.

Selected references

• B. J. Dietzenbacher and A. Y. Kondratev, Fair and Consistent Prize Allocation in Competitions, arXiv:2008.08985v2, 2021; Management Science, 2023. https://arxiv.org/abs/2008.08985v2, https://doi.org/10.1287/mnsc.2022.4520
• R. J. Aumann and M. Maschler, Game theoretic analysis of a bankruptcy problem from the Talmud, Journal of Economic Theory 36(2):195–213, 1985. https://doi.org/10.1016/0022-0531(85)90102-4
• S. Hart and A. Mas-Colell, Potential, value, and consistency, Econometrica 57(3):589–614, 1989. https://doi.org/10.2307/1911054

Motivation

Sports leagues, tournaments, esports events and research competitions all end with a ranking of the participants and a sum of prize money to divide among them. How the money is split according to the ranking is a design choice with visible consequences: Winner-Takes-All schemes reward only the top, equal division ignores the ranking, and most real prize schedules sit in between. The economics of tournaments has studied prize structures as incentive devices, but it has not asked which schedules follow from principles of fairness and coherence.

Dietzenbacher and Kondratev (arXiv:2008.08985, Management Science 2023) take the axiomatic approach of fair allocation theory to this question. The central axiom is consistency, the variable-population principle that has characterized solutions in bankruptcy, taxation, bargaining and cooperative games (Aumann and Maschler 1985; Young 1987; Lensberg 1988; Thomson 1988; Hart and Mas-Colell 1989): if any subgroup of competitors pools its prizes and re-divides them among themselves by the same rule, nobody's prize changes. This mission formalizes the paper's first main result, which identifies exactly the rules that are consistent, weakly respect the ranking, and never take money away when the endowment grows.

Setting

Let $U$ be a countable set of at least three potential competitors. A competition is a triple $(N, \mathcal R, E)$: a nonempty finite set $N \subseteq U$, a ranking $\mathcal R : N \to \{1, \dots, |N|\}$ (a bijection; $i$ is ranked above $j$ if $\mathcal R(i) < \mathcal R(j)$), and a prize endowment $E \ge 0$. For a nonempty $S \subseteq N$, the subranking $\mathcal R_S$ lists $S$ in the order of $\mathcal R$.

A prize allocation rule $\varphi$ assigns to every competition an allocation $\varphi(N, \mathcal R, E) \in \mathbb R^N_+$ with $\sum_{i \in N} \varphi_i(N, \mathcal R, E) = E$. Two basic rules are Equal Division, $\mathrm{ED}_i = E/|N|$, and Winner-Takes-All, $\mathrm{WTA}_i = E$ if $\mathcal R(i) = 1$ and $0$ otherwise.

The axioms of the main theorem are, for every competition and $i, j \in N$:

• order preservation: $\mathcal R(i) < \mathcal R(j) \Rightarrow \varphi_i(N, \mathcal R, E) \ge \varphi_j(N, \mathcal R, E)$;
• endowment monotonicity: $E < E' \Rightarrow \varphi_i(N, \mathcal R, E) \le \varphi_i(N, \mathcal R, E')$;
• consistency: for every nonempty $S \subseteq N$ and $i \in S$,

$$\varphi_i(N, \mathcal R, E) = \varphi_i\Big(S, \mathcal R_S, \sum_{j \in S} \varphi_j(N, \mathcal R, E)\Big).$$

Anonymity (prizes depend only on $|N|$, the position and $E$) and endowment continuity are auxiliary properties.

An interval rule is given by pairwise disjoint open intervals $(a_k, b_k)$, $k = 1, 2, \dots$, with $a_k \in \mathbb R_+$ and $b_k \in \mathbb R_+ \cup \{+\infty\}$. With $n = |N|$ and $r = \mathcal R(i)$,

$$\varphi_i(N, \mathcal R, E) = \begin{cases} a_k & \text{if } n a_k \le E \le (n - r + 1) a_k + (r - 1) b_k; \\ E - (n - r) a_k - (r - 1) b_k & \text{if } (n - r + 1) a_k + (r - 1) b_k \le E \le (n - r) a_k + r b_k; \\ b_k & \text{if } (n - r) a_k + r b_k \le E \le n b_k; \\ E / n & \text{otherwise.} \end{cases}$$

At endowment $n a_k$ everyone receives $a_k$; as $E$ grows, prizes are raised to $b_k$ one competitor at a time from the top; when $E/n$ lies in no $[a_k, b_k]$ the endowment is divided equally. ED has $a_k = b_k = 0$; WTA has $a_1 = 0$, $b_1 = +\infty$.

Formalization targets

Goal: Theorem 1 (p. 13)

$$\varphi \text{ satisfies order preservation, endowment monotonicity and consistency} \iff \varphi \text{ is an interval rule.}$$

Both directions are part of the goal.

Milestones, in the order the proof uses them

1. Lemma 1 (p. 10): endowment monotonicity implies endowment continuity.
2. Lemma 2 (p. 11): order preservation, endowment monotonicity and consistency imply anonymity.
3. Lemma 3 (p. 11): two endowment monotonic, consistent rules that agree on all two-competitor competitions agree on all competitions.
4. The "if" direction (p. 28): every interval rule satisfies the three axioms.
5. Step 1 (p. 28): for two competitors, if $\varphi(N, \mathcal R, x_1 + x_2) = (x_1, x_2)$ then $\varphi(N, \mathcal R, 2x_1) = (x_1, x_1)$ or $\varphi(N, \mathcal R, 2x_2) = (x_2, x_2)$.
6. Step 2 (p. 29): the two-competitor restriction has the interval form (9),

$$\varphi(N, \mathcal R, E) = (E - a_k, a_k) \text{ on } [2a_k, a_k + b_k], \quad (b_k, E - b_k) \text{ on } [a_k + b_k, 2b_k], \quad (E/2, E/2) \text{ otherwise.}$$

Further statements of §2.3

Lemma 4 (endowment additivity ⇔ scale invariance) and Corollaries 1–4, which single out WTA (winner-loser strict order preservation), ED (strict endowment monotonicity), the Winner-Takes-Surplus rules (winner strict endowment monotonicity) and the pair {ED, WTA} (additivity) inside the family of Theorem 1, are included as supporting theorems.

Significance

Theorem 1 replaces three qualitative requirements by an explicit, countably parametrized family. The family is broad (Equal Division, Winner-Takes-All, the "dollar at a time" rule of Example 1, and their concatenations along the endowment axis), so the theorem is the starting point for every sharper characterization in the paper: strengthening one axiom at a time selects WTA, ED or a Winner-Takes-Surplus rule (Corollaries 1–4), and the second and third missions of this series replace consistency by its local and top variants to obtain the single-parametric and parametric rules. Lemma 3 also isolates a general principle: a monotone consistent rule is determined by its behaviour on pairs.

On the formal side, Mathlib and the platform have no model of variable-population allocation with rankings. This mission provides one (competitions over a universe, subrankings, prize allocation rules and the consistency family of axioms) together with the first machine-checkable statement of a characterization theorem in this area. The paper's proofs are complete; nothing here is open mathematics, and none of it has been formalized before.

Difficulty

Consistency only constrains the rule across competitions; on its own it says nothing about how two competitors share a given endowment. The obvious plan, to read the intervals off the two-competitor allocation path and extend by Lemma 3, fails at the first step: an order preserving, monotone two-competitor path need not be a staircase of horizontal and vertical segments, and nothing about two competitors alone forces it to be. The staircase shape (Step 1) is a genuinely multi-competitor phenomenon that also relies on anonymity, which is not assumed and must be derived (Lemma 2, a six-case analysis over how two competitions share competitors). The countable family of intervals then has to be extracted from the path (Step 2), including endpoints at $+\infty$ and the gaps where the rule is equal division.

Formalization scope

A ranked set $(N, \mathcal R)$ is a duplicate-free nonempty List U, best first; $|N|$ is its length and $\mathcal R(i)$ = pos l i, the 1-based index. The subranking is the sublist of members of $S$. A rule is a function φ : List U → ℝ → U → ℝ; its values on non-rankings, negative endowments and non-members are irrelevant, and every axiom and the interval-rule definition quantify only over rankings, $E \ge 0$ and $i \in N$. The standing assumption on $U$ is carried as [Countable U] plus three distinct elements on every statement whose proof needs a third competitor (Lemma 2, Steps 1–2, Theorem 1, Corollaries 1–4); it is unnecessary for Lemmas 1, 3, 4 and for the "if" direction. Interval endpoints $b_k$ are extended reals (EReal), the intervals are indexed by $\mathbb N$ (finitely many intervals are padded with $a_k = b_k = 0$), $a_k \le b_k$, and disjointness is of the open intervals. The four cases are implications; "otherwise" means $E \notin [n a_k, n b_k]$ for every $k$.

The following formalizations would trivialize or change the theorem and are ruled out: a fixed competitor set or a finite $U$ of size two (consistency then has no reduced competitions to act on, and Corollary 1(i) fails); consistency restricted to two-element subsets or to some subsets only; a one-directional goal; interval rules without $+\infty$ endpoints (which excludes WTA and makes the "only if" direction false); and anonymity as an extra hypothesis.

The definitions are reusable by the two companion missions of this series (local and top consistency), which use the same model. Contributions welcome: proofs of the milestones, a general lemma that consistent monotone rules are determined by pairs, and proofs that ED, WTA and the Example 1 rule are interval rules.

Selected references

• B. J. Dietzenbacher and A. Y. Kondratev, Fair and Consistent Prize Allocation in Competitions, arXiv:2008.08985v2, 2021; Management Science 69 (2023). https://arxiv.org/abs/2008.08985, https://doi.org/10.1287/mnsc.2022.4520
• R. J. Aumann and M. Maschler, Game theoretic analysis of a bankruptcy problem from the Talmud, Journal of Economic Theory 36 (1985), 195–213. https://doi.org/10.1016/0022-0531(85)90102-4
• W. Thomson, A study of choice correspondences in economies with a variable number of agents, Journal of Economic Theory 46 (1988), 237–254. https://doi.org/10.1016/0022-0531(88)90131-7
• T. Lensberg, Stability and the Nash solution, Journal of Economic Theory 45 (1988), 330–341. https://doi.org/10.1016/0022-0531(88)90274-8
• S. Hart and A. Mas-Colell, Potential, value, and consistency, Econometrica 57 (1989), 589–614. https://doi.org/10.2307/1911054

Why blockchain adoption in supply chains is an economic question

A permissioned blockchain is a shared ledger that only invited parties may write to. In supply chains it is promoted as a way to make the provenance and quality of goods verifiable by the end consumer: a manufacturer who joins records how a good was produced, and consumers can read that record. Joining is costly, and the parties who pay the cost are not the parties who benefit most from the information. Whether such a technology is adopted at all is therefore a question about incentives, not engineering.

G. Iyengar, F. Saleh, J. Sethuraman and W. Wang, Economics of Permissioned Blockchain Adoption (SSRN 3602376; Management Science, 2023, DOI 10.1287/mnsc.2022.4532), build a stylised supply chain with vendors, price-competing manufacturers and consumers with an outside option, and show that welfare-improving adoption can fail to arise in equilibrium. This mission formalizes the first of the paper's two main results, Proposition 4.8, together with the welfare comparisons it rests on. A companion mission formalizes the second, the self-financing transfers of Proposition 4.9.

The supply chain

There are two vendors, of high and low quality $h > l \ge 0$, and a set $M$ of $4m$ manufacturers, $m \ge 2$ of each type $(q_i,\xi_i) \in \{A,B\}\times\{h,l\}$. A consumer of horizontal type $t_k$ obtains utility $H$ from a good with $q_i = t_k$ and $L$ otherwise, plus the vertical utility $\xi_i$; here $0 \le L < H$, and $\Delta := H - L > 0$ measures horizontal differentiation. Consumers can always take an outside option $\varphi_k$, drawn from a continuous distribution $G$ supported on $[0,\infty)$. The high type vendor produces at cost $c_h(x) = \gamma x$, $\gamma > 0$; the low type vendor at a strictly increasing convex cost $c_l$ with $c_l(0)=0$ and strictly increasing derivative $c_l'$ (Assumption 1, items 1–2).

Manufacturer $i$ may join the blockchain at cost $\chi_i > 0$ ($a_i = 1$) or not ($a_i = 0$). Three scenarios are compared: full adoption $F$ (all adopt), partial adoption $P$ (exactly the high type manufacturers adopt) and non-adoption $N$. The paper's Proposition A.1 gives each scenario's equilibrium in closed form: every consumer's best manufacturer offers utility

$$u^F = u^P = H + h - \gamma,\qquad u^N = \tfrac{H+L+h+l}{2} - \gamma,$$

the low type vendor price is $\Psi^F_l = \max\{\gamma-(h-l),0\}$, $\Psi^P_l = \max\{\gamma-(h-l)-\frac{H-L}{2},0\}$, $\Psi^N_l = \gamma$ (the high type price is always $\gamma$), the low type market shares are $s^F_l = (c_l')^{-1}(\gamma-(h-l))$, $s^P_l = (c_l')^{-1}(\gamma-(h-l)-\frac{H-L}{2})$, $s^N_l = (c_l')^{-1}(\gamma)$, and $s^X_h = G(u^X) - s^X_l$. Manufacturers earn zero gross profit $\Pi$ in every scenario because of price competition.

Welfare in scenario $X$ is the sum $W^X = W^X_V + W^X_M + W^X_C$ of vendor welfare $W^X_V$ (revenue minus production cost of both vendors, (10)), manufacturer welfare $W^X_M = \sum_{i}(\Pi - \chi_i a^X_i)$ and consumer welfare $W^X_C = \mathbb E[\max\{u^X,\varphi\}]$ ((12)). The adoption game (8) lets each manufacturer choose $a_i$ to maximise $\Pi(a_i,a_{-i}) - \chi_i a_i$. An adoption failure is a situation in which full adoption raises total welfare, $W^F > W^N$, but is not an equilibrium of the adoption game.

Formalization targets

Goal: Proposition 4.8 (p. 19)

With $L$ fixed and $H = L + \Delta$,

$$\exists\,\underline\Delta\ \ \forall\,\Delta > \underline\Delta:\quad W^F(\Delta) > W^N(\Delta)\ \text{ and full adoption is not an equilibrium},$$

at every such $\Delta$ at which Assumption 1 holds. The threshold $\underline\Delta$ is left unspecified, as in the paper.

Milestones

• Proposition 4.1 (pp. 15–16): $W^F_C \ge W^P_C > W^N_C$.
• Proposition 4.3 (p. 17): $W^F_M < W^P_M < W^N_M$.
• Proposition 4.4 (p. 17): $W^F_V,\ W^P_V < W^N_V$.
• Proposition 4.6 (p. 18): $W^F, W^P > W^N$ for all sufficiently large $\Delta$; at fixed $\Delta$, $W^F < W^N$ once $\sum_{i\in M}\chi_i$ is large and $W^P < W^N$ once $\sum_{i:\xi_i=h}\chi_i$ is large.
• Proposition 4.7 (p. 19): neither full nor partial adoption is an equilibrium.

What the result gives

The proposition isolates a mechanism: blockchain information raises consumer surplus, which grows without bound in $\Delta$, while Bertrand competition prevents the manufacturers who pay for adoption from capturing any of it. The conclusion is a market failure that persists however valuable the information is, and it motivates the paper's transfer scheme (Proposition 4.9), in which a consumer access fee finances the adopters. The welfare comparisons of Propositions 4.1–4.6 are reusable on their own: they quantify who gains and who loses from information disclosure in a vertically and horizontally differentiated market.

The results are proved in the paper (App. A.2, pp. 33–36). None is machine-checked. This mission produces a checked version of the welfare comparisons and of the failure result in the reduced form described below; the proofs as printed use a density for $G$ and a second derivative of $c_l$, neither of which the model assumes, so a formal proof has to avoid both.

Where the difficulty lies

The equilibrium part is light once the gross profit is zero. The substance is in the welfare comparisons. Consumer welfare is an expectation $\mathbb E[\max\{u,\varphi\}]$ of an outside option with an arbitrary continuous law: strict monotonicity in $u$ needs positive mass of $\varphi$ below $u^N$, which is a consequence of Assumption 1 rather than an assumption, and the growth in $\Delta$ of $W^F - W^N$ has to be bounded below without a density. Vendor welfare involves the generalised inverse $(c_l')^{-1}$, which is $0$ below $c_l'(0)$: the comparison $W^F_V < W^N_V$ must handle the regime where the low type vendor's share collapses to zero and the regime where it is interior, and must obtain continuity of $c_l'$ from convexity rather than from a second derivative.

Formalization scope

The paper describes a signalling and pricing game but does not define its equilibrium concept precisely; Proposition A.1 states the outcomes and every proof in App. A.2 uses only those closed forms. The mission adopts the same reduced form, disclosed in every item: welfare is evaluated at Proposition A.1's prices, shares and utilities; the manufacturers' gross profit $\Pi$ is the constant $0$ for every adoption profile (the paper's statement in the proof of Proposition 4.3, p. 34); an equilibrium of the adoption stage is a pure Nash equilibrium of (8) with that payoff, expressed with AGT.IsPureNash from the published agt_games vocabulary. The signal accuracy is fixed at $\alpha = 1/2$, as in the paper's main text.

Conventions: manufacturers are Fin 2 × Bool × Fin m (the Boolean records $\xi_i = h$), adoption profiles are Boolean functions, $G$ is ProbabilityTheory.cdf μ for a probability measure $\mu$ on $\mathbb R$, $\Delta$ is an argument of every statement with $H = L + \Delta$, and $(c_l')^{-1}(x) = \sup\{s \ge 0 : c_l'(s) \le x\}$. The standing assumptions are bundled in Model.Standing: $m \ge 2$, $0 \le L$, $0 \le l < h$, $\gamma > 0$, $\chi_i > 0$, $\mu$ an atomless probability measure with $\mu((-\infty,0)) = 0$ and positive mass on every interval $(a,b) \subseteq [0,\infty)$, $c_l$ strictly increasing and convex on $[0,\infty)$ with $c_l(0) = 0$ and a strictly increasing derivative there. One hypothesis is added to the paper's: $\varphi$ has a finite mean, which the paper uses (its proof of Proposition 4.1 integrates $v\,p(v)$) without stating it. Assumption 1, item 3, depends on $\Delta$ through $H$ and is a hypothesis at each $\Delta$; it is satisfiable (for instance with $c_l(x) = x^2$, $\varphi \sim \mathrm{Exp}(1)$, $\gamma = 1/2$, $h=1$, $L=l=0$, $\Delta = 4$) and monotone in $\Delta$.

The formalization rules out the trivializing readings: the equilibrium predicate is concrete, not an abstract hypothesis; the integrals are of integrable functions, so no junk value $0$ enters; the inverse of $c_l'$ is the explicit supremum, not Function.invFun; and $L$, not $H$, is held fixed as $\Delta$ grows.

Needed infrastructure: expectations of $\max\{c,\varphi\}$ as a function of $c$ (monotonicity, growth), and the generalised inverse of a strictly increasing derivative of a convex function. Both are reusable beyond this mission. Proofs of the milestones in any order are welcome, as are alternative arguments that avoid the density and the second derivative of the printed proofs.

Selected references

• G. Iyengar, F. Saleh, J. Sethuraman, W. Wang, Economics of Permissioned Blockchain Adoption, SSRN 3602376, version of 2022-08-19. https://ssrn.com/abstract=3602376
• G. Iyengar, F. Saleh, J. Sethuraman, W. Wang, Economics of Permissioned Blockchain Adoption, Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4532
• N. Nisan, T. Roughgarden, É. Tardos, V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Ch. 1 (pure Nash equilibrium). https://doi.org/10.1017/CBO9780511800481

Interoperability and dominant platforms

Digital markets with strong network effects (messaging, social networks, app stores) tend to concentrate: a platform with more users is worth more to each user. Interoperability, the ability of a platform's users to interact with the users of rival platforms, is a central remedy in current competition policy; the EU Digital Markets Act (2022) mandates it for messaging services offered by designated gatekeepers. Whether interoperability actually reduces the market share of a dominant platform is a question about equilibria of a pricing game.

Ekmekci, White and Wu (Management Science, 2025) answer it in a model of platform competition built on net fees. Their Proposition 6 shows, for a Logit duopoly, that lowering interoperability always admits an equilibrium with an even larger dominant platform; equivalently, interoperability may mitigate dominance. This mission formalizes that result and the steps of its proof.

Setting

There are two platforms $j\in\{1,2\}$ and one side of users. Platform $j$ chooses a net fee $t^j\in\mathbb R$: the price a user pays, net of the interaction value the platform extracts once the user has joined. With Logit demand and no outside option, platform $j$'s market share at the fee profile $t=(t^1,t^2)$ is

$$n^j(t)=\frac{e^{-t^j}}{e^{-t^1}+e^{-t^2}} .$$

Both platforms have marginal cost $c$, and each user values each other user of the same platform at $\gamma$, the network externality. The degree of interoperability $\lambda\in[0,1]$ lets a user of platform $j$ also enjoy $\lambda\gamma$ per user of the rival platform (the paper's (19)), and the platform extracts this value too. Platform $j$'s profit is

$$\pi^j(t)=\bigl(t^j+\gamma n^j+\lambda\gamma n^{-j}-c\bigr)\,n^j,\qquad n^{-j}=1-n^j .$$

A fee profile $t$ is a Nash equilibrium in net fees under $\lambda$ if no platform can raise its profit by changing its own fee to any other real number. In an equilibrium with $n^j(t)>1/2$, platform $j$ is the dominant platform.

The Lean development (namespace NetFeePlatform.InteropDominance) writes $n^j(t)$ as demand 0 t j (the 0 is the weight of the absent outside option), $\pi^j$ as profit 0 c γ lam t j, and equilibrium as IsEquilibrium 0 c γ lam t, with t : Fin 2 → ℝ.

Formalization targets

Goal: Proposition 6 (p. 23)

Let $\gamma>0$, $0\le\underline\lambda<\overline\lambda\le1$ and $\gamma(1-\underline\lambda)\le 27/8$. If $t$ is an equilibrium under $\overline\lambda$ and $n^j(t)>1/2$, then there is an equilibrium $t'$ under $\underline\lambda$ with

$$n^j(t')>n^j(t).$$

The equilibrium $t'$ is not unique in general, and the statement does not say which one; it asserts existence, exactly as the paper does.

Milestones

1. Logit derivative (p. 13): $\partial n^j/\partial t^j=-n^j(1-n^j)$.
2. First-order condition (20) (p. 23): every equilibrium satisfies $t^j=c+\frac1{1-n^j}-2\gamma n^j-\gamma\lambda(1-n^j)+\gamma\lambda n^j$.
3. Sufficiency (Appendix E.1.3 with (36)): if $\gamma(1-\lambda)\le 27/8$, a fee satisfying (20) is a best response.
4. Equivalence (p. 24): the market $(c,\gamma,\lambda)$ has the equilibria of the market $(c-\gamma\lambda,\ \gamma(1-\lambda),\ 0)$.
5. Characterization (p. 51): equilibrium shares are the zeros of $\zeta(n;\lambda)=\ln\frac{n}{1-n}+\frac1{1-n}-\frac1n-2\gamma(1-\lambda)(2n-1)$, and conversely under the bound of item 3.
6. Comparison (p. 52): $\zeta(n;\underline\lambda)-\zeta(n;\overline\lambda)=2\gamma(\underline\lambda-\overline\lambda)(2n-1)<0$ for $n>1/2$.
7. Boundary behaviour (p. 52): $\zeta(n;\lambda)\to\infty$ as $n\to1^-$.

Significance

The result. Proposition 6 is the paper's argument that interoperability mandates can reduce concentration without any change in the platforms' cost or quality: at a fixed network externality, every equilibrium with a dominant platform under a higher degree of interoperability is outsized by an equilibrium under a lower degree, so the largest dominant share an equilibrium can sustain does not increase as interoperability rises. The proof rests on the equivalence of item 4, under which interoperability acts as a reduction of the effective network externality from $\gamma$ to $\gamma(1-\lambda)$; Figure 2 of the paper plots the resulting largest equilibrium share as $\lambda$ varies at $\gamma=3.375$.

Formalizing it. The paper's proof is three paragraphs, and it identifies equilibria with zeros of $\zeta$. A formal proof has to supply what the text takes for granted: that the first-order condition is necessary at a global Nash equilibrium, that it is sufficient in the stated range, and that a zero of $\zeta$ can be turned back into a fee profile. No part of the result has been machine-checked before. A complete development also gives a reusable treatment of Logit demand and of best responses in one-variable concave games.

Difficulty

The algebra of $\zeta$ and the intermediate value step are short. The work lies in the equilibrium notion. A Nash equilibrium is a global condition over every unilateral deviation $s\in\mathbb R$, and profit is not concave in the platform's own fee. Measured against the platform's own share $n\in(0,1)$, profit has second derivative $-1/(n(1-n)^2)+2\gamma(1-\lambda)$; it is concave exactly when $2\gamma(1-\lambda)$ does not exceed the minimum $27/4$ of $1/(n(1-n)^2)$. Outside that range the first-order condition is not sufficient, and a zero of $\zeta$ need not be an equilibrium; the paper does not treat that case.

Formalization scope

• Model. One side ($S=1$), two platforms indexed by Fin 2, Logit demand with no outside option (outside weight $w=0$, literally), common $c$ and $\gamma$, interoperability $\lambda$ written lam. The Setting file states the general $J$-platform objects (demand with an outside-option weight $w\ge0$, profit with the interoperability term $\lambda\gamma\sum_{k\ne j}n^k$, equilibrium, the diversion ratio of (32)); this mission uses them at $J=2$, $w=0$.
• Hypotheses. The paper assumes $\gamma>0$ and $\lambda\in[0,1]$. The goal adds $\gamma(1-\underline\lambda)\le 27/8$, the range in which the paper proves that the first-order condition is sufficient (Appendix E.1.3 with (36), the $3.375$ of Proposition 2′); the paper's own proof stops at the first-order condition and is not complete without it.
• Correction. The paper prints $\zeta(\overline n^1;\underline\lambda)-\zeta(\overline n^1;\overline\lambda)=4(\underline\lambda-\overline\lambda)\gamma\overline n^1$; the correct value is $2\gamma(\underline\lambda-\overline\lambda)(2\overline n^1-1)$. Its sign is the same, and milestone 6 states the correct value.
• Ruled out. Equilibrium is never replaced by "the pricing formula (20) holds": that would reduce the goal to an intermediate value argument and remove its substance. Shares are always demand 0 t j at a fee profile, never free variables. Profit keeps the interoperability term; without it $\lambda$ would not enter the model at all.
• Out of scope. General (non-Logit) demand and Assumptions A1–A2, $S\ge2$ sides, $J\ge3$ platforms (Proposition 12), platform-specific $c^j,\gamma^j$, the microfoundation of Appendix A, and the numerical Figure 2.
• Welcome contributions. Proofs of the milestones, in particular the Logit change of variable from fees to shares and the concavity bound, which are reusable in the two companion missions of this series.

Selected references

• M. Ekmekci, A. White, L. Wu, Platform Competition and Interoperability: The Net Fee Model, Management Science, 2025; accepted working-paper version of December 12, 2024 (the version cited here). https://doi.org/10.1287/mnsc.2023.02810
• J. Crémer, P. Rey, J. Tirole, Connectivity in the Commercial Internet, Journal of Industrial Economics 48(4), 2000. https://doi.org/10.1111/1467-6451.00129
• Regulation (EU) 2022/1925 (Digital Markets Act), Official Journal of the European Union L 265, 2022. https://eur-lex.europa.eu/eli/reg/2022/1925/oj

Motivation

Markets organized by platforms (social networks, marketplaces, messaging services) exhibit network effects: a user values a platform more when more users join it. A standing concern in competition policy is that such markets "tip" towards one dominant platform, and the usual remedy proposed is to foster entry. Ekmekci, White and Wu (Platform Competition and Interoperability: The Net Fee Model, Management Science, 2025) develop a tractable model of platform oligopoly in which platforms compete in net fees, the price a user pays net of the interaction value the platform delivers, and use it to examine policy interventions. Their Proposition 4 shows that the intuition "more platforms, less dominance" can fail: with strong network effects, adding a third platform to a duopoly can produce an equilibrium whose leader is larger than any platform of any duopoly equilibrium.

The net-fee approach is the authors' alternative to the "insulated equilibrium" of White and Weyl (2016); the paper's §5 specializes it to Logit demand, where pricing formulas are explicit.

Setting

There are $J$ platforms and one side of users. Platform $j$ charges a net fee $t^j\in\mathbb R$; write $t=(t^1,\dots,t^J)$. Demand has the Logit form (13): with outside-option weight $w=e^{z}\ge0$,

$$n^j(t)=\frac{e^{-t^j}}{w+\sum_k e^{-t^k}},$$

and in this mission there is no outside option, $w=0$, so the shares sum to one. Platforms are ex ante identical: common marginal cost $c$ and common interaction value $\gamma$. Platform $j$'s profit ((8) with one side) is

$$\pi^j(t)=\big(t^j+\gamma\,n^j(t)-c\big)\,n^j(t),$$

the net fee plus the interaction value the platform extracts per user, less cost, times its share. A net-fee equilibrium is a pure-strategy Nash equilibrium: no platform $j$ can raise $\pi^j$ by changing its own net fee to any $s\in\mathbb R$. Duopoly is $J=2$, triopoly $J=3$.

At an equilibrium, each net fee satisfies the Logit pricing formula (14), $t^j=c+\frac{1}{1-n^j}-2\gamma n^j$. For equilibria with one dominant platform of share $1-n$ and $J-1$ equal small platforms of share $n/(J-1)$, the paper reduces the equilibrium conditions to a zero of the characterization function

$$g(n;J)=\ln n-\ln(J-1)-\ln(1-n)+\frac{1}{1-\frac{n}{J-1}}-2\gamma\frac{n}{J-1}-\Big(\frac1n-2\gamma(1-n)\Big),\qquad 0<n<1.$$

Formalization targets

Goal: Proposition 4 (competition may increase dominance)

For $2\ln2+\tfrac43<\gamma\le\tfrac{27}{8}$: duopoly has an equilibrium, and there exist a triopoly equilibrium $t_3$ and a platform $i$ with

$$n^k(t_2)<n^i(t_3)\quad\text{for every duopoly equilibrium }t_2\text{ and every platform }k.$$

The comparison is against every duopoly equilibrium and every platform in it, not against one selected equilibrium.

Milestones

1. The Logit derivative $\partial n^j/\partial t^j=-n^j(1-n^j)$ (p. 13).
2. Proposition 1 in Logit form (14): every equilibrium satisfies $t^j=c+\frac1{1-n^j}-2\gamma n^j$ (pp. 12–13).
3. The Logit concavity bound (36): for $\gamma\le27/8$, the pricing formula gives a global best response (p. 43).
4. The zeros of $g(\cdot;J)$ are exactly the equilibria with one dominant and $J-1$ equal small platforms (p. 49).
5. $\lim_{n\to0^+}g(n;J)=-\infty$ (p. 49).
6. $g(n;3)-g(n;2)=-\ln2+\frac1{1-n/2}-\frac1{1-n}+\gamma n$ (p. 50).
7. For $2\ln2+\tfrac43<\gamma\le\tfrac{27}{8}$, $g(n;3)>0$ at every zero $n\in(0,\tfrac12]$ of $g(\cdot;2)$ (p. 50).

Significance

The result. Proposition 4 is a counterexample to a policy presumption: entry need not reduce concentration in markets with network effects. With a third platform, the two small platforms can split the fringe so thinly that the leader's share rises above anything sustainable in a duopoly. The result identifies an explicit parameter window; together with the companion results on interoperability (Propositions 6 and 7 of the same paper), it frames which interventions reduce dominance in this model.

Formalizing it. The proposition is proved in the paper partly by a numerical check ("we can verify", p. 50), and its printed interval $(2.71,3.375]$ is slightly too wide at the bottom: at the symmetric duopoly equilibrium the paper's own criterion requires $\gamma>2\ln2+\tfrac43\approx2.7196$. A machine-checked proof would settle the corrected statement, replace the numerical step by an argument, and make the equilibrium characterization through $g(n;J)$ (including the step from first-order conditions to global Nash equilibrium) available for the other results of the series. None of these statements is formalized anywhere to our knowledge.

Difficulty

Three steps resist the obvious argument.

• First-order conditions are not equilibria. The pricing formula is necessary; that it is sufficient requires profit to be concave in the platform's own share, which holds only for $2\gamma\le 1/(n(1-n)^2)$, i.e. for $\gamma\le 27/8$. Without this, zeros of $g$ need not be equilibria.
• "Any duopoly equilibrium" is universal. Duopoly may have asymmetric equilibria for $\gamma$ near the top of the range, so the triopoly leader must beat the smallest zero of $g(\cdot;2)$ in $(0,\tfrac12]$, not only the symmetric one.
• The positivity of $g(n;3)$ at duopoly zeros is an inequality between transcendental functions of $n$ on a $\gamma$-dependent set; the paper checks it numerically. Its margin vanishes as $\gamma$ approaches $2\ln2+\tfrac43$ at $n=\tfrac12$, and the paper's rewriting $\gamma=f(n,J)$ is $0/0$ exactly there.

Formalization scope

• Lean namespace NetFeePlatform.Competition. The definitions file Setting declares the Logit demand demand w t j, the profit profit w c γ lam t j (with an interoperability term $\lambda\gamma\sum_{k\ne j}n^k$, set to $\lambda=0$ throughout this mission), the global Nash predicate IsEquilibrium, and the diversion ratio; GChar declares $g(n;J)$. Platforms are indexed by Fin J.
• Committed conventions: one side ($S=1$), Logit demand, common $c$ and $\gamma$, no outside option ($w=0$, literally, not a limit $z\to-\infty$), real-valued net fees with deviations over all of $\mathbb R$.
• The goal's lower bound is $2\ln2+\tfrac43$ instead of the printed $2.71$ (see Difficulty and the goal's Formalization Note); the upper bound $27/8=3.375$ is exact. The goal adds the conjunct "duopoly has an equilibrium", the existence claim of Proposition 2′ in this case, so that "any duopoly equilibrium" is not vacuous.
• Trivializing formalizations are ruled out: equilibrium is the global Nash condition, never the first-order condition; the comparison quantifies over all duopoly equilibria; the dominant platform's index is existential, not fixed.
• Out of scope: general (non-Logit) demand and Assumptions A1–A2, $S\ge2$ sides, platform-specific $\gamma^j$ and $c^j$, the microfoundation of Appendix A, Propositions 2, 2′, 3, 5 and 13.
• Infrastructure: one-variable calculus (derivatives, concavity, the intermediate value theorem, limits) from Mathlib. The Logit derivative and the concavity-based best-response lemma (milestones 1–3) are reusable for any Logit oligopoly with network effects. Contributions of alternative proofs of milestone 7 (interval arithmetic or monotonicity arguments) are welcome.

Selected references

• M. Ekmekci, A. White, L. Wu, Platform Competition and Interoperability: The Net Fee Model, Management Science, 2025 (accepted working-paper version of December 12, 2024). https://doi.org/10.1287/mnsc.2023.02810
• A. White, E. G. Weyl, Insulated Platform Competition, SSRN working paper, 2016. https://ssrn.com/abstract=1694317