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

Motivation

A seller who must auction one item without knowing how buyers value it needs a mechanism that performs acceptably against every plausible value distribution. Anunrojwong, Balseiro and Besbes (arXiv:2204.10478, Operations Research 2025) measure performance by regret: the expected revenue lost relative to a seller who knows the realized valuations and extracts the highest one. Their main result (Theorem 1, the subject of mission I of this series) shows that against independent and identically distributed valuations the minimax-regret mechanism is a second-price auction whose reserve price is random, drawn from an explicit distribution.

Practitioners rarely randomize reserves. The natural benchmark is the familiar second-price auction with a fixed deterministic reserve $r$, and the question this mission addresses is how much is lost by insisting on a deterministic reserve: what is the worst-case regret of that auction, and which reserve minimizes it? The paper answers this exactly in Proposition 5 (§5.2.1, p. 24, proof in Appendix D, pp. App-10–11). For a single buyer, regret-optimal posted pricing was studied by Bergemann and Schlag (2008), where a deterministic price $1/2$ has worst-case regret $1/2$; Proposition 5 is the $n$-buyer version of that benchmark.

Setting

There are $n\ge1$ buyers with valuations $v=(v_1,\dots,v_n)$ in the type cube $[0,1]^n$, drawn from a joint distribution $\mathbf F$ unknown to the seller. Write $v^{(1)}=\max_i v_i$ and $v^{(2)}$ for the second-highest valuation. A direct mechanism charges buyer $i$ a payment $p_i(v)$, and its regret under $\mathbf F$ is

$$R_n(m,\mathbf F)=\mathbb E_{v\sim\mathbf F}\Big[v^{(1)}-\sum_{i=1}^n p_i(v)\Big].$$

The second-price auction with reserve $r$, $\mathrm{SPA}(r)$, gives the item to the highest bidder if the highest bid is at least $r$, at price $\max(v^{(2)},r)$, and otherwise does not sell. Its revenue is $\max(v^{(2)},r)\,\mathbf 1(v^{(1)}\ge r)$.

Three classes of distributions on $[0,1]^n$ are considered:

• $\mathcal F_{\mathrm{iid}}$: product laws $G^{\otimes n}$, with $G$ a law on $[0,1]$;
• $\mathcal F_{\mathrm{aff}}$: exchangeable laws (invariant under permuting buyers) that are affiliated, meaning $\Pr(A\cap B\mid S)\ge\Pr(A\mid S)\Pr(B\mid S)$ for all increasing sets $A,B$ and every sublattice $S$ (a set closed under coordinatewise minimum and maximum);
• $\mathcal F_{\mathrm{mix}}$: mixtures of i.i.d. laws, whose joint CDF is $\mathbf F(v)=\int\prod_i G(v_i)\,d\mu(G)$ for a probability measure $\mu$ on distributions.

The worst-case regret of $\mathrm{SPA}(r)$ over a class $\mathcal F$ is $\sup_{\mathbf F\in\mathcal F}R_n(\mathrm{SPA}(r),\mathbf F)$. The closed form found by the paper is

$$W_n(r)=\begin{cases}\max(1-r,\,r), & n=1,\\[2pt] \dfrac{(1-r)^n(n-1)^{n-1}}{((1-r)n-r)^{n-1}}, & n\ge 2,\ r\le\tfrac12,\\[4pt] r, & n\ge2,\ r>\tfrac12,\end{cases}$$

called wcFixed n r in the Lean development.

Formalization targets

Goal: Proposition 5

For every $n\ge1$, every class $\mathcal F\in\{\mathcal F_{\mathrm{iid}},\mathcal F_{\mathrm{aff}},\mathcal F_{\mathrm{mix}}\}$ and every $r\in[0,1]$,

$$\sup_{\mathbf F\in\mathcal F}R_n(\mathrm{SPA}(r),\mathbf F)=W_n(r),$$

the no-reserve auction has $W_n(0)=1$ for $n=1$ and $\big(\frac{n-1}{n}\big)^{n-1}$ for $n\ge2$, and

$$\min_{r\in[0,1]}W_n(r)=W_n\Big(\frac1{n+1}\Big)=\Big(\frac n{n+1}\Big)^n,$$

with $r^*=1/(n+1)$ the unique minimizer.

Milestones

1. The regret of $\mathrm{SPA}(r)$ under an i.i.d. law with marginal CDF $F$: $rF_-(r)^n-\int_0^rF^n+\int_r^1(nF^{n-1}-nF^n)$.
2. For $n\ge2$, the maximum of $rc^n+(1-r)(nc^{n-1}-nc^n)$ over $c\in[\frac{n-1}{n},1]$ equals $W_n(r)$.
3. For $n=1$, the maximum of $rc+(1-r)(1-c)$ over $c\in[0,1]$ is $\max(1-r,r)$.
4. $W_n$ is minimized on $[0,1]$ exactly at $1/(n+1)$, with value $(n/(n+1))^n$.
5. For $n\ge2$, every exchangeable affiliated law gives $\mathrm{SPA}(r)$ regret at most $W_n(r)$.

Significance

The result. Proposition 5 gives the exact price of determinism. The optimal fixed reserve $1/(n+1)$ has worst-case regret $(n/(n+1))^n$: $1/2$ for one buyer, $4/9$ for two. The minimax regret of the optimal randomized auction is about $0.368$ and $0.324$ for the same cases, so the benchmark shows how much of the paper's improvement comes from randomizing the reserve. Both values converge to $1/e$ as $n\to\infty$. Proposition 5 also shows that the worst case does not change when valuations are positively dependent (affiliated, or mixtures of i.i.d.), the same robustness the paper establishes for its optimal mechanism.

Formalizing it. The result is proved on paper in the paper's Appendix D, and no machine-checked version is known. A formal proof needs an expression of the expected revenue of a second-price auction through the order-statistic CDFs, a careful treatment of atoms at the reserve, two elementary but fiddly one-variable optimizations, and, for $\mathcal F_{\mathrm{aff}}$ and $\mathcal F_{\mathrm{mix}}$, the reduction to the i.i.d. case.

Difficulty

The supremum over $\mathcal F_{\mathrm{iid}}$ is not attained. The auction's revenue jumps at the reserve: a buyer valued exactly at $r$ buys, while one valued just below does not. Nature exploits this with two-point laws placing mass just below $r$ and the rest at $1$, and the regret approaches $W_n(r)$ only in the limit. So the first idea, exhibiting a maximizing distribution, fails, and any formalization must treat the worst case as a least upper bound. The upper bound over $\mathcal F_{\mathrm{aff}}$ is the real difficulty: it rests on an order-statistic identity and on an inequality between the CDFs of the maxima of $n-1$ and $n$ affiliated valuations, which in turn needs properties of affiliation that are quoted from Milgrom and Weber (1982) rather than proved in the paper. For $\mathcal F_{\mathrm{mix}}$ the bound needs the regret to be linear in the mixing measure, i.e. a disintegration of the mixture law through its joint CDF.

Formalization scope

• Representation. Buyers are Fin n; valuations are vectors Fin n → ℝ; a distribution is a probability measure on Fin n → ℝ whose complement of the cube $[0,1]^n$ is null. $\mathcal F_{\mathrm{iid}}$ is the set of products Measure.pi (fun _ => G) of a probability law G on $[0,1]$. $\mathcal F_{\mathrm{mix}}$ uses a probability measure on Measure ℝ with the Giry σ-algebra and states the CDF identity of Definition 6 for every $v$.
• The auction. $\mathrm{SPA}(r)$ is the random-reserve auction SPA ρ at ρ = Measure.dirac r; the winner pays $\max(v^{(2)},r)$ when its bid is at least $r$. Ties go to the lowest index (the paper breaks them arbitrarily; revenue does not depend on the rule).
• Affiliation is stated cross-multiplied, $\mu(A\cap S)\mu(B\cap S)\le\mu(A\cap B\cap S)\mu(S)$, for measurable increasing $A,B$ and measurable sublattices $S$.
• Conventions committed to. The reserve ranges over $[0,1]$ (the page leaves this implicit; for $r>1$ the closed form is false). Worst-case regret is IsLUB of the set of regrets, not a maximum and not sSup. "The optimal reserve" is IsLeast of $W_n$ on $[0,1]$, its value at $1/(n+1)$, and uniqueness of the minimizer.
• Ruled out. A statement with IsGreatest would be false (the supremum is not attained); sSup of the regret image would be a junk value if the image were unbounded; classes without the $[0,1]^n$ support condition, or $r$ unconstrained, change the theorem.
• Infrastructure. Expected revenue of a second-price auction via order statistics, the CDF of the maximum and second maximum of i.i.d. variables, and the reduction of mixtures to their components are reusable for the rest of this series and for auction theory generally. Contributions to the affiliation inequalities (Milgrom–Weber) are particularly welcome.

Selected references

• J. Anunrojwong, S. R. Balseiro, O. Besbes, On the Robustness of Second-Price Auctions in Prior-Independent Mechanism Design, arXiv:2204.10478v5, 2024; Operations Research, 2025. https://arxiv.org/abs/2204.10478
• D. Bergemann, K. Schlag, Pricing without Priors, Journal of the European Economic Association 6(2–3), 560–569, 2008. https://doi.org/10.1162/JEEA.2008.6.2-3.560
• P. R. Milgrom, R. J. Weber, A Theory of Auctions and Competitive Bidding, Econometrica 50(5), 1089–1122, 1982. https://doi.org/10.2307/1911865

Motivation

Large online marketplaces such as Amazon, JD.com and Walmart.com act both as a sales channel for third-party sellers and as a retailer of their own. A platform watches which third-party products sell well and may start selling the same product itself, a move called platform entry. Over ten months of 2013–2014, Amazon entered about 3% of the products first offered only by third-party sellers, and its entry lowered the affected products' sales rankings, that is, raised their total sales (Zhu & Liu, Strategic Management Journal 2018). The conventional view is that a seller should deter entry, since the platform becomes a competitor that also collects a referral fee on every sale the seller makes.

L. Qi, H. Song and W. Xiao (Management Science 2025) build a two-stage model with three features: the platform charges a referral rate on the seller's revenue, the platform's marketing effort spills over to the seller's product, and the two parties compete in quantities with differentiated products. Their Proposition 2 identifies exactly when the seller is better off if the platform enters. This mission formalizes that result together with the equilibrium analysis it rests on.

Setting

There are five parameters: the degree of spillover $\delta \in [0,1]$, the referral rate $f \in [0,1)$, the competition intensity $\beta \in [0,1]$, the seller's effort-cost coefficient $c_S$ and the platform's entry cost $K$. The product has base value $a$. The platform's effort-cost coefficient is normalized to $1/2$.

Stage 1. The seller chooses an effort $e_S$ at cost $c_S e_S^2$, which raises the product value to $a + e_S$, and a quantity $q_1$. The price is $p_1 = a + e_S - q_1$, and the seller earns $q_1 p_1 (1-f) - c_S e_S^2$ after paying the referral fee $f q_1 p_1$.

Stage 2 without entry. The seller alone sells $q_S$ at price $p_S = a + e_S - q_S$ and earns $q_S p_S(1-f)$.

Stage 2 with entry. The platform chooses an effort $e_P \ge 0$ at cost $e_P^2/2$. Its own product's value becomes $a + e_S + e_P$, and the seller's product's value becomes $a + e_S + \delta e_P$. The two then choose quantities simultaneously, with prices

$$p_S = a + e_S + \delta e_P - q_S - \beta q_P, \qquad p_P = a + e_S + e_P - q_P - \beta q_S .$$

The seller earns $q_S p_S (1-f)$. The platform earns $q_S p_S f + q_P p_P - e_P^2/2 - K$: the referral fee on the seller's revenue plus its own margin.

Backward induction gives closed forms. Write

$$N_5 = 4(1+\delta) - 2\beta(2-\delta+\delta^2) + \beta^3(1+f) - \beta^2(2+f+\delta f)$$

and let $D$ be the quartic denominator of the platform's optimal effort (Lemma 2). Condition (5) is $N_5 > 0$: under it the seller stays in the market after entry. The paper assumes (5) from that point on. Let

$$H = \begin{cases} N_5^2/D^2 & \text{if (5) holds},\\ 0 & \text{otherwise,}\end{cases}$$

so that the seller's two-stage profits as functions of the effort $e_S$ are

$$\Pi^S_N(e_S) = \tfrac12 (1-f)(a+e_S)^2 - c_S e_S^2, \qquad \Pi^S_E(e_S) = \big(\tfrac14 + H\big)(1-f)(a+e_S)^2 - c_S e_S^2 .$$

The receptive regime is $\Omega = \{(\delta,f,\beta) \mid H > 1/4\}$.

Formalization targets

Goal: Proposition 2

$$\Pi^S_E(e_S) > \Pi^S_N(e_S) \iff (\delta,f,\beta) \in \Omega \qquad (a + e_S \ne 0),$$

and the shape of $\Omega$ on the box $[0,1]\times[0,1)\times[0,1]$:

• for fixed $(f,\beta)$ there is $\tilde\delta(f,\beta)$ with $(\delta,f,\beta)\in\Omega \iff \delta > \tilde\delta(f,\beta)$;
• for fixed $(\delta,\beta)$ there is $\tilde f(\delta,\beta)$ with $(\delta,f,\beta)\in\Omega \iff f > \tilde f(\delta,\beta)$;
• for fixed $(\delta,f)$ there are $\beta_1(\delta,f) \le \beta_2(\delta,f)$ with $(\delta,f,\beta)\in\Omega \iff \beta < \beta_1$ or $\beta > \beta_2$.

The thresholds are existentials, as the paper defines them only inside its proof.

Milestones

1. Lemma 1: the stage-2 quantity game after entry has a unique equilibrium, given in closed form.
2. Lemma 2 under (5): the platform's optimal effort $e^*_P$ in closed form, and the seller stays ($q^*_S > 0$). The positivity of $e^*_P$ and of its denominator is a separate milestone.
3. Equations (6)–(8): the seller's equilibrium two-stage profits are $\Pi^S_N$ and $\Pi^S_E$ above.
4. The identity $4N_5^2 - D^2 = P_{11}\cdot S_2$ from the proof of Proposition 2, where $P_{11}$ is the function (11).
5. Under (5) the second factor $S_2$ is positive.
6. Lemma 3, in three parts: the sign pattern of (11) in $\delta$, in $f$ and in $\beta$.

Significance

The result. Proposition 2 says that the seller's preference does not depend on the seller's own effort or on the base value, only on $(\delta, f, \beta)$. It shows that the conventional advice to deter entry is wrong on a nonempty region: a strong enough spillover, or a high enough referral rate (which gives the platform a stake in the seller's sales and so a reason to invest more effort), makes entry welcome. In the competition intensity the regime is not monotone. The seller welcomes entry when products are well differentiated, opposes it at intermediate $\beta$, and can welcome it again near perfect substitutes. The paper's later results on the seller's optimal effort and on entry deterrence (Proposition 3 onward) are stated separately inside and outside $\Omega$, so this classification is their starting point.

Formalizing it. The result is proved in the paper, and nothing about it is machine-checked yet. Its proof leans on "one can verify" claims about quartic polynomials on a box: the positivity of $D$, of the platform's effort and of $S_2$ under (5), and the sign patterns of (11). A formal proof checks each of them. The mission also ties the closed forms (6)–(7) to an explicit game, with equilibria defined as best responses, so the comparison is between equilibrium profits and not between formulas taken on trust.

Difficulty

The first part of the goal is immediate once (6)–(7) are known, since $\Pi^S_E - \Pi^S_N = (H - \tfrac14)(1-f)(a+e_S)^2$. The content lies elsewhere.

• The equilibrium analysis. The platform's payoff includes the referral fee on the seller's revenue, so its best-response slope is $\beta(1+f)/2$, not the textbook $\beta/2$. The seller's quantity has a corner at zero. The platform's effort problem must be solved against every equilibrium after every deviation, and it reduces to a single variable only after uniqueness in Lemma 1.
• Polynomial sign conditions. Positivity of $D$ and $S_2$ under (5), and the threshold structure of (11) in each variable, are statements about polynomials of degree up to four on a box with the semialgebraic side condition (5).
• A step the paper omits. $\Omega$ is defined through $H$, and $H = 0$ off (5). Moving Lemma 3's thresholds from (11) to $\Omega$ therefore also needs "(11) $> 0$ implies (5)", which the paper does not state. It holds numerically: on a $201^3$ grid, wherever (11) is positive the left side of (5) is above $1.01$. A complete proof of the goal must supply it.

Formalization scope

All quantities are real numbers. The parameters are explicit arguments, and the standing ranges $\delta\in[0,1]$, $f\in[0,1)$, $\beta\in[0,1]$ are a hypothesis InBox δ f β. Every polynomial ($N_5$, $D$, the numerator of $e^*_P$, (11), $S_2$) is written term for term as printed. $H$ keeps the case split of (8), so $\Omega$ is false wherever (5) fails. Conventions:

• Defined from the game: the quantity equilibrium (a pure Nash equilibrium over nonnegative quantities, through the published general two-player definition CompetingChains.Cournot.IsPureNash), the entry equilibrium (the platform's effort $e_P \ge 0$ is a global maximizer against every equilibrium after every deviation), and the stage-1 and no-entry problems.
• The paper's closed forms: $H$, $\Omega$, $\Pi^S_N$ and $\Pi^S_E$. Milestone 3 proves that the closed forms equal the equilibrium profits.
• "Optimal" means a global maximizer, ties allowed.
• The platform's effort is nonnegative. The seller's effort $e_S$ is any real number, as in the paper.
• Lemmas 1–2 assume $a + e_S > 0$ (a positive product value), and Lemma 2 assumes (5), the paper's standing assumption.
• Only the branch of Lemma 2 under (5) is formalized.
• The goal's first part assumes $a + e_S \ne 0$. At $a + e_S = 0$ both profits equal $-c_S e_S^2$ and no strict preference exists.
• Condition (5) is not a hypothesis of the goal.

The first part of the goal is near-definitional given (6)–(7). The mission's content is the threshold structure of $\Omega$ and milestones 1–3, which make (6)–(7) the equilibrium profits. A formalization in which the thresholds may depend on the varying parameter, or in which $\Omega$ is taken as $\{(11) > 0\}$ by definition, would not be this theorem.

A complete development needs real polynomial inequalities on boxes (nlinarith/polyrith-style certificates or interval arguments) and elementary concave maximization. A uniqueness lemma for two-player games whose best responses have slopes with product below one would be reusable for other differentiated Cournot models. Contributions are welcome for any milestone, for the step "(11) $> 0$ implies (5)", and for proofs of the sign lemmas by certificates.

Selected references

• L. Qi, H. Song, W. Xiao, Coopetition in Platform-Based Retailing: On the Platform's Entry, Management Science, 2025. https://doi.org/10.1287/mnsc.2023.00260 (formalized from the authors' manuscript with Online Supplement, 2024-08-03).
• F. Zhu, Q. Liu, Competing with complementors: An empirical look at Amazon.com, Strategic Management Journal 39(10), 2018. https://doi.org/10.1002/smj.2932
• N. Singh, X. Vives, Price and quantity competition in a differentiated duopoly, RAND Journal of Economics 15(4), 1984. https://doi.org/10.2307/2555525