Algorithmic Game Theory

Motivation

Financial networks are webs of liabilities: firm $u$ owes firm $v$ an amount $c_{(u,v)}$, and every firm holds some external assets. When firms cannot pay in full, how much money actually moves through the network depends on how each firm splits its available funds among its creditors. The classical clearing model of Eisenberg and Noe (2001) fixes this split by a proportional rule. Flow allocation games, introduced by Bertschinger, Hoefer and Schmand (arXiv:1908.01714, Mathematics of Operations Research, 2025), make it strategic: every firm chooses how to allocate whatever it receives, and the resulting payments are the clearing state of the chosen strategies.

Because money that circulates comes back, the total amount of flow in such a network is driven by cycles, and cycles require several firms to cooperate. The natural solution concept is therefore the strong equilibrium, which is stable against joint deviations of coalitions. The paper shows that in unit-ranking games a strong equilibrium maximizing total flow always exists (Theorem 9, price of stability $1$). This mission concerns the other side: how much total flow can the worst strong equilibrium lose, and which structural parameter of the network controls the loss.

Setting

A flow allocation game $\Gamma=(G,(b_v)_{v\in V},(c_e)_{e\in E})$ consists of a finite directed graph $G=(V,E)$ (parallel edges allowed), a fixed supply $b_v\in\mathbb N_0$ at each node and a capacity $c_e\in\mathbb N_0$ on each edge. Every node is a player. $E^+(v)$ and $E^-(v)$ denote the outgoing and incoming edges of $v$, and $c_v^+=\sum_{e\in E^+(v)}c_e$.

In a unit-ranking game, player $v$ chooses for each edge $e\in E^+(v)$ a non-decreasing function $a_e:\mathbb N_0\to\mathbb N_0$ with $a_e(y)\le c_e$ and $\sum_{e\in E^+(v)}a_e(y)=\min\{c_v^+,y\}$: given a total supply $y$, it forwards all of it until its outgoing edges are full, one unit at a time according to a ranking of unit capacities. A flow $f$ is feasible for a profile $\mathbf a$ if $f_{(v,w)}=a_{(v,w)}(f_v)$ with $f_v=b_v+\sum_{e\in E^-(v)}f_e$. The clearing state $\hat f$ is the coordinatewise largest feasible flow; player $v$'s utility is $u_v(\mathbf a)=\sum_{e\in E^+(v)}\hat f_e$, and the total flow is

$$\mathrm{Flow}(\mathbf a)=\sum_{e\in E}\hat f_e .$$

A profile is a strong equilibrium if no non-empty coalition $C\subseteq V$ can jointly switch to other unit-ranking strategies so that every member of $C$ strictly gains.

The circulation network $G'$ adds an auxiliary node $s$ with edges $(v,s)$ of unbounded capacity and $(s,v)$ of capacity $b_v$ for every $v$. An optimal circulation $f^*$ of $G'$ maximizes $\sum_{e\in E'}f^*_e$. A decomposition $\mathcal C(f^*)=\{C_1,\dots,C_k\}$ of $f^*$ into cycles of unit flow is a list of simple directed cycles of $G'$ that uses each edge exactly as often as $f^*$ has units on it. The parameter of this mission is

$$d=\min_{f^*,\ \mathcal C(f^*)}\ \max_{C_i\in\mathcal C(f^*)}|C_i| ,$$

the smallest possible size of the longest cycle, over all decompositions of all optimal circulations; sizes count auxiliary edges.

Formalization targets

Goal: Theorem 16 (p. 30)

In unit-ranking games, the price of anarchy for strong equilibria in terms of Flow is at most $d$: for every strong equilibrium $\mathbf a$ and every unit-ranking profile $\mathbf a'$,

$$\mathrm{Flow}(\mathbf a')\le d\cdot\mathrm{Flow}(\mathbf a).$$

The statement fixes no constant beyond the structural parameter $d$ and holds for all capacities and supplies.

Milestones (proof of Theorem 16, p. 30)

1. An optimal circulation yields the optimal total flow, and

$$\mathrm{Flow}(\mathbf a^*)=\sum_{C_i\in\mathcal C(f^*)}|C_i|-2\sum_{v}b_v\le\sum_{C_i\in\mathcal C(f^*)}d .$$

2. In a strong equilibrium every simple cycle of $G$ contains an edge with $\hat f_e=c_e$.
3. $\mathrm{Flow}(\mathbf a)$ is at least the number of cycles of $\mathcal C(f^*)$ that avoid $s$.

Companions

• Theorem 16 for games without fixed supplies ($b\equiv0$), the setting of Propositions 15 and 17.
• Proposition 17 (p. 30). For every $d\ge2$ there is a unit-ranking game with parameter $d$ and a strong equilibrium $\mathbf a$ with $\mathrm{Flow}(\mathbf a)>0$ and $(d-1)\,\mathrm{Flow}(\mathbf a)\le\mathrm{Flow}(\mathbf a^*)$.

Significance

The bound identifies the length of the circulating cycles as the quantity that governs the efficiency of coalition-stable payment behaviour. In networks whose optimal circulation decomposes into short cycles, such as bilateral or triangular netting of liabilities, every strong equilibrium clears at least a $1/d$ fraction of the optimal total payments; Proposition 17 shows that long cycles genuinely cost efficiency, so the bound is tight up to one. For pure Nash equilibria no such bound exists (Proposition 15, the price of anarchy is unbounded), so the result separates coalitional from unilateral stability.

The results are proved on paper; none of them is machine-checked. A formalization adds a precise account of the model (clearing state as a supremum of feasible flows, unit-ranking strategies as functions on $\mathbb N_0$, cycle decompositions of the circulation network) and checks a proof whose last step, as printed, needs repair. The printed last display, $\mathrm{Flow}(\mathbf a)\ge\sum_{C_i\in\mathcal C(f^*)}1$, does not hold for cycles passing through the auxiliary node $s$: with a single node $v$, $b_v=1$ and no outgoing edges, $\mathcal C(f^*)=\{(s,v,s)\}$ but $\mathrm{Flow}(\mathbf a)=0$. The theorem itself is not contradicted by this example, and the printed argument is complete for games without fixed supplies. The cycles through the auxiliary node need a separate count, which is part of the work this mission asks for.

Difficulty

The upper bound compares an arbitrary strong equilibrium with an optimum that may look nothing like it. The obvious approach, counting the units of each optimal cycle that also carry equilibrium flow, fails: the clearing state is a fixed point of all strategies at once, so whether a unit reaches an edge depends on decisions all around the network, and the equilibrium may route its flow along entirely different cycles. A single player cannot complete a cycle on its own, which is why the Nash price of anarchy is unbounded; any argument has to use coalitional deviations, and a deviation changes the clearing state globally, so its effect on each member's utility must be controlled through the fixed point.

The second difficulty is the auxiliary node. A cycle of the optimal decomposition that passes through $s$ contains a node that is not a player, so no coalition of players can claim it, and the unit of flow it represents may sit on an auxiliary edge that $\mathrm{Flow}$ does not count. These cycles are exactly where the printed argument stops short.

Formalization scope

Supplies, capacities, strategies and flows are natural numbers, as the paper prescribes for unit-ranking games. The graph is a finite type of nodes $V$ and a finite type of edges $E$ with tail and head maps, so parallel edges and loops are allowed. The clearing state is the coordinatewise sSup of the feasible flows. Coalitions are non-empty, and deviations range over unit-ranking profiles. Optimal circulations are optimal among integral circulations. Cycles of $G'$ are lists of edges with pairwise distinct start nodes, and decompositions are lists of cycles counted with multiplicity. Nodes of $G'$ are Option V, with none the node $s$.

The price of anarchy is stated multiplicatively, $\mathrm{Flow}(\mathbf a')\le d\cdot\mathrm{Flow}(\mathbf a)$, with no division, so a zero-flow equilibrium cannot satisfy the goal vacuously through a junk quotient. The parameter $d$ enters as a hypothesis, "some decomposition of some optimal circulation has all cycles of size at most $d$", which is equivalent to the bound for the min-max $d$ and avoids an infimum that would be $0$ on an empty set. In Proposition 17 the strong equilibrium is required to have positive flow, since otherwise the lower bound would hold trivially.

Not formalized: the complexity results of the paper, the bounds for other quality measures (Proposition 18) and for Nash equilibria (Proposition 15). A complete development needs the integral version of the lattice theorem for feasible flows (Theorem 2), the existence of a Flow-optimal profile from the proof of Theorem 9, and integral cycle decomposition of circulations; the last two are reusable beyond this mission. Contributions are welcome on each milestone, on a separate count for cycles through $s$, and on the explicit construction of Proposition 17.

Selected references

• N. Bertschinger, M. Hoefer, D. Schmand, Flow Allocation Games, Mathematics of Operations Research, 2025; preprint arXiv:1908.01714v3, 2023. https://arxiv.org/abs/1908.01714
• L. Eisenberg, T. H. Noe, Systemic Risk in Financial Systems, Management Science 47(2), 236–249, 2001. https://doi.org/10.1287/mnsc.47.2.236.9835

Motivation

Music streaming platforms collect a subscription fee from each user and pass a large share of the revenue to the artists. How that money is divided has become a policy question. Most platforms use the pro-rata rule: all fees are pooled and each artist is paid in proportion to their share of all streams. The main alternative is the user-centric rule: each user's fee is divided only among the artists that user played, in proportion to that user's own streams. The choice decides whether a heavy listener's tastes count for more than a light listener's, and it has been debated by platforms, rights holders and regulators.

G. Bergantiños and J. D. Moreno-Ternero, Revenue Sharing at Music Streaming Platforms (arXiv:2310.11861, Management Science, 2025), study the question axiomatically and through cooperative game theory. This mission formalizes their Theorem 3: once one asks that no group of artists can be paid less than the money of the users who only listened to that group, the user-centric rule is the only homogeneous and additive option. Two sibling missions treat Theorem 1 (axiomatic characterizations of pro-rata and user-centric) and Theorem 2 (the core of the streaming game).

Setting

There are $n$ artists $N$. A streaming problem $(N, M, t)$ consists of a finite set $M$ of users and the numbers $t_{ij} \in \mathbb N$ of times user $j$ played artist $i$; every user has played at least one artist. For a user $j$ let

$$T^j = \sum_{i\in N} t_{ij}, \qquad L^j = \{i \in N : t_{ij} > 0\},$$

the user's total streams and the list of artists the user played. Each user pays $1$, so the amount to be shared is $m = |M|$.

A popularity index $I$ assigns to each problem a nonnegative vector $I(N,M,t) \in \mathbb R^N$ with positive total. Artist $i$ is then paid

$$R^I_i(N,M,t) = \frac{I_i(N,M,t)}{\sum_{i'\in N} I_{i'}(N,M,t)}\, m .$$

Indices that are positive multiples of each other pay the same, and are identified. The user-centric index is $U_i(N,M,t) = \sum_{j\in M} t_{ij}/T^j$.

The streaming game of a problem is the cooperative game on the artists with worth $v(S) = |\{j \in M : L^j \subseteq S\}|$, the money of the users who only played artists in $S$. Its core is

$$C(N,v) = \Big\{x \in \mathbb R^N : \sum_{i\in N} x_i = v(N),\ \sum_{i\in S} x_i \ge v(S) \text{ for all } S \subseteq N\Big\}.$$

The axioms are:

• homogeneity: if $\lambda \ge 0$ and $t_{ij} = \lambda t_{i'j}$ for every user $j$, then $I_i = \lambda I_{i'}$;
• additivity: the index of the union of two problems with disjoint sets of users is the sum of their indices;
• core selection: $R^I(N,M,t) \in C(N,v)$.

The domain $\mathcal P^*$ consists of the problems in which no user has played every artist, $L^j \neq N$ for all $j\in M$.

Formalization targets

Goal: Theorem 3 (p. 14)

On $\mathcal P^*$, an index satisfies homogeneity, additivity and core selection if and only if there is $c > 0$ with

$$I_i(N,M,t) = c\, U_i(N,M,t) \qquad \text{for every } (N,M,t) \in \mathcal P^*,\ i \in N.$$

Milestones

1. The user-centric rewards belong to $A(N,M,t)$, the vectors $\sum_{j\in M} x^j$ with each $x^j$ a probability vector on $L^j$; and they belong to the core $C(N,v)$, on every problem (p. 14).
2. The user-centric index satisfies homogeneity, additivity and core selection on $\mathcal P^*$ (p. 23).
3. Display (1): under core selection, the index of a one-user problem vanishes outside the user's list (pp. 23–24).
4. On a one-user problem, $I_i = \big[\sum_{i'} I_{i'}\big] U_i$ (p. 24).
5. The Claim: two distinct users with disjoint lists have one-user problems with equal index totals (p. 24).
6. The same equality for any two distinct users (p. 25).

Significance

The theorem singles out the user-centric rule by a stability property rather than by a fairness postulate about users. Core selection says that no coalition of artists receives less than the payments of the users who listen exclusively to that coalition; the pro-rata rule violates it already in a two-user example (p. 14). Together with Theorem 1 of the same paper, it gives two independent routes to the user-centric rule, which is the form in which the result enters the policy discussion.

The paper proves the theorem in its appendix (pp. 23–25). Nothing about streaming problems, popularity indices or this characterization has been formalized before; the mission produces a machine-checked version of the model, of the user-centric index's membership in the core, and of the characterization. The model layer (problems as finitely supported stream tables, rewards, the streaming game) is shared in shape with the two sibling missions.

Difficulty

Each axiom is easy to verify for the user-centric index; the content is the converse. Homogeneity and additivity alone allow every weighted index, where each user's streams are weighted by an arbitrary positive function of the user and the profile, and pro-rata is one of them. The difficulty is to extract from core selection, which only constrains ratios of index values through the reward normalization, that every user carries exactly the same total weight. Core selection on a single user only fixes the shape of the index on that user's list; comparing two users requires problems with several users, and the comparison of two users whose lists overlap cannot be made directly.

Formalization scope

Artists are Fin n (0-based). Users are natural numbers, and a problem is a finitely supported map t : ℕ →₀ (Fin n → ℕ) whose support is the user set $M$. This builds in three standing assumptions of the paper: every user of a problem has played some artist ($L^j \neq \emptyset$), streams are natural numbers, and an index can depend only on the columns of the users of the problem. The core is the published Supermodularity.Cooperative.Core on Finset.univ. Rewards use $m = |M|$; at the empty problem the reward vector is $0$ and the core of the zero game is $\{0\}$.

Two readings are committed to and disclosed:

• Additivity is for disjoint user groups. The page's "$M = M^1 \cup M^2$" without disjointness would force $I = 2I$ and no index would satisfy it; every proof in the paper splits users disjointly.
• The domain $\mathcal P^*$. The page defines $\mathcal P^*$ as the problems with at least three users in which no user played every artist. The proof applies core selection and additivity to one- and two-user problems "in $\mathcal P^*$" and draws a third user from outside the problem. The formalization follows the proof: $\mathcal P^*$ is every problem in which no user played every artist, the axioms and the conclusion are quantified over it, and "at least three users" is a property of the user population $\mathbb N$, which is infinite. A version restricting the axioms to problems with at least three users is a different statement not covered by the paper's proof.

The index requirements (nonnegativity, positive total) are imposed on nonempty problems of $\mathcal P^*$ only; demanding a positive total at the empty problem would make every index impossible and the theorem vacuous. "Is the user-centric index" is one global $c > 0$, not a constant depending on the problem: a problem-dependent constant would turn the conclusion into a much weaker statement. With one artist $\mathcal P^*$ holds only the empty problem and the theorem is vacuous, as on the page; no hypothesis on $n$ is added. The milestones on one-user problems are stated for arbitrary nonzero profiles of a user, which is the same as the page's columns of a problem in $\mathcal P^*$.

A complete development needs finite-sum manipulation over Finsupp supports and the decomposition of a problem into its one-user problems. Proofs of any milestone are welcome, as are proofs of Theorem 2's inclusion $A \subseteq C$, which milestone 1 needs.

Selected references

• G. Bergantiños, J. D. Moreno-Ternero, Revenue Sharing at Music Streaming Platforms, arXiv:2310.11861v1, 2023; Management Science, 2025. https://arxiv.org/abs/2310.11861
• V. A. Vasil'ev, On a class of imputations in cooperative games, Soviet Mathematics Doklady 23, 53–57, 1981 (used by the paper's Theorem 2, from which milestone 1 is drawn).
• J. C. Harsanyi, A bargaining model for cooperative n-person games, in A. W. Tucker, R. D. Luce (eds.), Contributions to the Theory of Games IV, Princeton University Press, 1959, pp. 325–355 (dividends, used by Theorem 2).

Motivation

Optimal auction theory in the tradition of Myerson (1981) assumes that the seller knows the distribution of the buyers' valuations. In practice that distribution is estimated, misspecified, or simply unknown. Prior-independent mechanism design asks for a mechanism that performs well across a whole class of distributions, without being tuned to any one of them. A natural yardstick is regret: the gap between the revenue the seller would extract if she knew the valuations, namely the highest valuation, and the revenue her mechanism actually collects. The seller chooses a mechanism to minimize the worst case of this gap over all distributions Nature may pick.

For a single buyer, Bergemann and Schlag (2008) showed that the minimax regret over valuations supported on $[0,1]$ is $1/e$, attained by a posted price drawn at random with CDF $\log v + 1$ on $[1/e, 1]$. Whether a comparably explicit answer exists for $n$ buyers, and whether the familiar second-price auction remains optimal among all dominant-strategy mechanisms, was open. Anunrojwong, Balseiro and Besbes (arXiv:2204.10478v5, Operations Research 2025) answer both questions for i.i.d. valuations. This mission formalizes that answer: their Theorem 1.

Setting

A seller has one indivisible item and $n \ge 1$ buyers with valuations $v = (v_1, \dots, v_n) \in [0,1]^n$. A mechanism $m = (x, p)$ assigns to every valuation profile allocation probabilities $x_i(v) \in [0,1]$ and expected payments $p_i(v)$. It is dominant-strategy incentive compatible (DSIC), written $m \in \mathcal M$, if for all $i$, all $v$ and every misreport $\hat v_i$:

$$v_i x_i(v) - p_i(v) \ge 0 \;\;\text{(IR)}, \qquad v_i x_i(v) - p_i(v) \ge v_i x_i(\hat v_i, v_{-i}) - p_i(\hat v_i, v_{-i}) \;\;\text{(IC)}, \qquad \textstyle\sum_i x_i(v) \le 1 \;\;\text{(AC)}.$$

For a joint distribution $F$ of $v$, the regret is

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

and the minimax regret over a class $\mathcal F$ of distributions is $\mathcal R^*_n(\mathcal F) = \inf_{m \in \mathcal M} \sup_{F \in \mathcal F} \mathrm{Regret}(m, F)$. Here $\mathcal F_{\mathrm{iid}}$ is the class of product laws $G^{\otimes n}$ whose marginal $G$ is supported on $[0,1]$.

A second-price auction with random reserve $\mathrm{SPA}(\Phi)$ draws a reserve price $q$ from a distribution $\Phi$. The highest bidder wins if her bid is at least $q$ and pays $\max(v^{(2)}, q)$, where $v^{(1)} \ge v^{(2)}$ are the two highest valuations. Otherwise nothing is sold.

Two explicit functions enter the answer. For $r \in (0,1)$, let

$$\mathrm{rEq}_n(r) = (1-r)^{n-1} + \log r + \sum_{k=1}^{n-1} \frac{(1-r)^k}{k},$$

and, for $r < v \le 1$,

$$\Phi^*_n(v) = \Big(\frac{v}{v-r}\Big)^{n-1}\log\Big(\frac vr\Big) - \sum_{k=1}^{n-1} \frac1k \Big(\frac{v}{v-r}\Big)^{n-1-k},$$

with $\Phi^*_n = 0$ below $r$ and $1$ above $1$. The isorevenue marginal $F^*_n(v) = 1 - r/v$ on $[r, 1)$, $F^*_n(1) = 1$, is the law under which every posted price in $[r,1]$ earns the same revenue $r$.

Formalization targets

Goal: Theorem 1

Let $r^*_n$ be the root of $\mathrm{rEq}_n$ in $(0, 1/n)$; it is the only root in $(0,1)$. A reserve distribution on $[r^*_n, 1]$ with CDF $\Phi^*_n$ exists. The auction $\mathrm{SPA}(\Phi^*_n)$ is DSIC and minimax-regret optimal, and

$$\mathcal R^*_n(\mathcal F_{\mathrm{iid}}) = (1-r^*_n)^{n-1} - \int_{r^*_n}^1 \Big(1 - \frac{r^*_n}{v}\Big)^{n-1} dv.$$

The Lean goal states the location and uniqueness of the root, the existence of the reserve law, the DSIC property, the upper bound for $\mathrm{SPA}(\Phi^*_n)$ against every i.i.d. law, the matching lower bound for every DSIC mechanism, and the literal identity for $\mathcal R^*_n(\mathcal F_{\mathrm{iid}})$.

Milestones

1. Lemma B-1 (p. App-4): an integration-by-parts identity for $\int h\,dG$, split at $r^*$.
2. Proposition 1 (p. 16): the regret of $\mathrm{SPA}(\Phi)$, for $\Phi$ with a density on $[r^*, 1]$, in terms of the order-statistic CDFs; joint and i.i.d. forms.
3. Proposition A-3 (p. App-2): the root $r^*_n$; $\Phi^*_n$ equals a power series, solves the ODE $(\Phi^*)' + \frac{(n-1)r^*_n}{v(v-r^*_n)}\Phi^* = \frac1v$, and satisfies $\Phi^*_n(r^*_n) = 0$ and $\Phi^*_n(1) = 1$; the regret at the candidate saddle point equals the value.
4. Step 1 of the proof of Theorem 1 (p. 17): against $\mathrm{SPA}(\Phi^*_n)$, the i.i.d. isorevenue law is a worst case.
5. Step 2 (p. 17): against the i.i.d. isorevenue law, $\mathrm{SPA}(\Phi^*_n)$ has the least regret among all DSIC mechanisms.

A companion item states Corollary 1 (p. 14): for $n = 1$, $r^*_1 = 1/e$, $\Phi^*_1(v) = \log v + 1$ on $[1/e, 1]$, and the minimax regret is $1/e$.

Significance

The theorem gives, for every number of buyers, a closed-form description of the minimax-regret optimal mechanism among all DSIC mechanisms, together with its value. The optimum is a familiar format, a second-price auction, but its reserve price must be randomized. The same saddle point is the starting point for the paper's results on affiliated and arbitrary joint valuations, which are separate missions of this series.

The result is proved on paper. To our knowledge none of it has been formalized. A complete development would supply machine-checked versions of several tools that recur in robust mechanism design: DSIC mechanisms with randomized allocations, the regret functional, order-statistic CDFs of product measures, Myerson-type revenue characterizations under distributions with atoms, and saddle-point arguments for inf–sup problems over mechanisms and distributions.

Difficulty

The upper bound (Step 1) is a pointwise optimization once the regret of $\mathrm{SPA}(\Phi)$ is written through the CDFs of the order statistics. Writing it that way already requires integration by parts against arbitrary distributions on $[0,1]$, which may have atoms.

The lower bound (Step 2) is the hard direction. One must show that no DSIC mechanism beats $\mathrm{SPA}(\Phi^*_n)$ against the isorevenue law. The standard route through Myerson's virtual values does not apply directly: the isorevenue law is a mixture of a density and a point mass at $1$, so the revenue of a general DSIC mechanism has to be characterized from first principles. That characterization starts from the payment identity for dominant-strategy mechanisms. The closed forms also involve a transcendental root $r^*_n$ and a logarithmic ODE solution, so the monotonicity and boundary facts about $\Phi^*_n$ (it is a CDF, $\Phi^*_n(1) = 1$) need real analysis rather than numerics.

Formalization scope

Buyers are indexed by Fin n, valuations are functions Fin n → ℝ, and distributions are measures on that space. (IR), (IC) and (AC) are imposed for valuations in $[0,1]^n$, which is all the seller considers. Two conditions are added to DSIC so that the expectation in the regret is meaningful: the allocation and payment rules are measurable, and payments are bounded on the cube. The second-price auction breaks ties in favour of the lowest index; the revenue does not depend on the rule. A reserve law or an isorevenue law is described by a hypothesis on its CDF. $\Phi^*_n$ is defined piecewise, so its closed form is never evaluated at the singular point $v = r^*_n$, and "$\Phi^*_n(r^*_n) = 0$" is stated as a one-sided limit. The minimax regret is a real infimum over the nonempty class of DSIC mechanisms of real suprema of bounded families. Uniqueness of $r^*_n$ is stated on $(0,1)$, which is what the paper's proof establishes.

Trivializing formalizations are ruled out explicitly. The regret is not a Bochner integral of a possibly non-integrable payment, which Lean would set to $0$. The mechanism class is not restricted to second-price auctions. The value is the explicit integral, not a sSup. The root's location in $(0, 1/n)$ is part of the claim.

Contributions are welcome at every level. These include the DSIC property of $\mathrm{SPA}(\Phi)$, order-statistic CDFs of product measures, Lemma B-1 and Proposition 1, the analytic facts about $\mathrm{rEq}_n$ and $\Phi^*_n$, the payment identity for DSIC mechanisms with randomized allocations, and the revenue bound of Step 2. The analytic and mechanism-design infrastructure is reusable beyond this paper.

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), 2008. https://doi.org/10.1162/JEEA.2008.6.2-3.560
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58

Motivation

Large online retailers such as Amazon run two businesses on one storefront. They sell products themselves, and they host a marketplace on which third-party sellers sell, paying the platform a percentage of their revenue. A retailer that also runs the marketplace can decide which products to sell itself, and it controls which offer most consumers see. Competition authorities have asked whether this dual role lets the platform appropriate third-party sellers' business, and empirical work (Zhu and Liu, 2018) finds that Amazon enters only a small, high-performing subset of marketplace products.

Hervas-Drane and Shelegia (Retailer-Led Marketplaces, Management Science, 2025) give a model in which these choices can be computed. Its main result, Proposition 2, says which products the platform sells itself when its assortment is limited. This mission formalizes that proposition together with the pricing and entry results it rests on.

Setting

There is a unit mass of products. Each product is an independent market indexed by its consumers' valuation $v$. Valuations are distributed according to a probability measure $\mu$ on $[c,\infty)$ with CDF $G(v)=\mu((-\infty,v])$. Every unit costs $c>0$ to supply. Each market has a unit mass of unit-demand consumers, who buy at a price $p$ only if $p\le v$.

The monopolist retailer $M$ sets an ad valorem fee $f\in[0,1]$ on the third-party seller's revenue. He can steer a share $\lambda$ of consumers (the inattentive ones) to the seller of his choice; the remaining $1-\lambda$ buy from the cheapest offer, with ties going to $M$. He has capacity $k\in[0,1]$: he can supply at most a fraction $k$ of all products.

The game has three stages. In Stage 1 $M$ sets $f$. In Stage 2 each product's third-party seller $T$ decides whether to enter, and then $M$ chooses which products to enter. In Stage 3, in each market both present firms price sequentially: $T$ quotes first, then $M$ quotes and steers. The solution concept is subgame perfect equilibrium.

Proposition 1 solves Stage 3. A product supplied by $M$ alone (SBM) earns him $\pi_M^{SBM}=v-c$. A product supplied by $T$ alone (SBT) earns her $(1-f)v-c$ and earns him the fee $\pi_M^{SBT}=fv$. When both supply it (SBMT), $T$ charges

$$\bar p_T=\frac{\lambda v+c(1-\lambda)}{1-f(1-\lambda)},$$

and $M$ earns $\pi_M^{SBMT}=\lambda(v-c)+(1-\lambda)f\bar p_T$. Lemma 1 says $T$ enters exactly the products $v\ge v_T=c/(1-f)$, the marketplace products. An allocation of $M$ is any measurable set $A$ of products with $\mu(A)\le k$. His total profit is the SBM profit on $A$ below $v_T$, plus the SBMT profit on $A$ above $v_T$, plus the fee on marketplace products outside $A$.

Formalization targets

Goal: Proposition 2

Assume $\lambda\ge\tfrac12$ (Assumption 1) and $f<1$. Let $\Delta\pi(v)=\pi_M^{SBMT}(v)-\pi_M^{SBT}(v)$ and

$$v^*=\frac{c\lambda}{(1-f)^2(\lambda-f(1-\lambda))},\qquad \underline k=1-G(v^*).$$

Then:

• Mode I. If $k\le\underline k$, the optimal allocation is unique up to $\mu$-null sets and equals $[v_K,\infty)$ with $1-G(v_K)=k$ (empty if $k=0$).
• Mode II. If $k>\underline k$, it is $[v_L,v_T)\cup[v_H,\infty)$, where

$$\pi_M^{SBM}(v_L)=\Delta\pi(v_H),\qquad (1-G(v_H))+(G(v_T)-G(v_L))=k.$$

Milestones

1. Proposition 1, its three supply configurations: the SBM monopoly price, the SBT equilibrium, and the SBMT subgame perfect equilibrium, which is unique for $0<\lambda<1$ and $v(1-f)>c$.
2. Lemma 1 with (1) and Property 1: the entry threshold $v_T$.
3. The closed form of $\Delta\pi$, its positivity above $v_T$, and its monotonicity in $v$ and in $f$.
4. (A.2): $\Delta\pi(v^*)=\pi_M^{SBM}(v_T)$, and $v^*\ge v_T$.
5. The $(v_L,v_H)$ system has a unique solution when $k>\underline k$.

Significance

Proposition 2 is the step that the rest of the paper builds on. Display (4) writes the monopolist's profit as a function of the fee by plugging in the thresholds $v_L$, $v_T$, $v_H$, $v_K$ of Proposition 2. The optimal fee (Lemma 2, Proposition 3) and the policy comparisons of §6 (a pure-retailer response, fee regulation, steering bans) are all statements about that function. The two modes are also the paper's empirical prediction. A platform with little capacity, effective steering and a high fee competes only in the top marketplace products. With more capacity it also takes products no third party sells.

The paper proves Proposition 2 in Appendix A. The proof is an informal capacity-allocation argument. No machine-checked version exists. A formal proof has to turn the argument about entering the products of highest marginal profitability first into a statement about all measurable allocations of mass at most $k$. It must also prove uniqueness up to null sets, and handle the corners $k=0$, $k=1$ and $f=0$ that the prose passes over.

Difficulty

The obvious argument ranks products by the marginal profitability of entry and fills capacity from the top. Two facts make this harder than it looks. First, the ranking is not monotone in $v$. Below $v_T$ the gain is $v-c$; above $v_T$ it is $\Delta\pi(v)$, which starts again from $0$ at $v_T$. So the optimal set is an upper level set of a piecewise function, and in Mode II it has two components. Second, the claim is about every measurable set of mass at most $k$, not about thresholds. Optimality needs an exchange argument against arbitrary sets, and uniqueness needs the level sets of the gain to be $\mu$-null. Locating the thresholds also needs continuity and strict monotonicity of $G$, which come from the density and the full-support hypothesis.

Proposition 1 has its own subtlety. At $p_T=\bar p_T$ the monopolist is indifferent between matching $T$'s price and charging $v$. $T$'s best price exists only if $M$'s strategy breaks this tie in $T$'s favour, so the equilibrium has to be stated for strategies defined at every price of $T$.

Formalization scope

Products form a probability measure μ : Measure ℝ. The standing hypotheses are:

• $\mu((-\infty,c))=0$, $\mu\ll$ Lebesgue (the density $g$), and Integrable (fun v => v) μ, which the paper never states but which is needed for profits to be finite;
• $\mu$ charges every nonempty open interval of $[c,\infty)$, the reading of $G^{-1}$ in (3);
• $c>0$, $f\in[0,1)$, $\lambda\in[\tfrac12,1]$, $k\in[0,1]$.

The foreclosed corner $f=1$ ($v_T=\infty$) is not covered. Marketplace products are encoded as $\{v: c\le v(1-f)\}$. Optimal allocations quantify over all measurable sets of mass at most $k$, and uniqueness is up to $\mu$-null sets. Restricting allocations to intervals or to unions of two intervals would assume the conclusion, and the formalization does not do it.

In Proposition 1, $M$'s strategy is a function of $T$'s price that is a best response at every price, and $T$'s price is optimal against it. Uniqueness of the SBMT outcome is stated only for $0<\lambda<1$ and $v(1-f)>c$, where it holds. Lemma 1's duopoly clause likewise needs $0<\lambda<1$.

Two definition files carry the model:

• Model: $G$, the marketplace set, the Proposition 1 payoffs, $\Delta\pi$, $v^*$, $\underline k$, allocations and profit;
• PricingGame: the three pricing games and their equilibria.

The bathtub-type lemma behind Proposition 2 is reusable beyond this mission: among measurable sets of mass at most $k$, an upper level set of a weight maximizes its integral. Contributions of that lemma, of the milestones, and of alternative proofs are welcome.

Selected references

• A. Hervas-Drane, S. Shelegia, Retailer-Led Marketplaces, Management Science, Articles in Advance, 2025. https://doi.org/10.1287/mnsc.2023.00315
• F. Zhu, Q. Liu, Competing with Complementors: An Empirical Look at Amazon.com, Strategic Management Journal 39:2618–2642, 2018. https://doi.org/10.1002/smj.2932
• A. Hervas-Drane, S. Shelegia, Price Competition with a Stake in Your Rival, International Journal of Industrial Organization 84:102862, 2022 (the simultaneous-pricing variant of the pricing game). https://doi.org/10.1016/j.ijindorg.2022.102862

Motivation

During the COVID-19 pandemic most U.S. payers began reimbursing a telehealth consultation at the same rate as the corresponding office visit, a policy called pay parity. Many states have since made it permanent, on the stated ground that it improves patients' access to care. In acute care (primary and urgent care) a telehealth visit sometimes cannot resolve the problem and the patient must also come to the office: a duplicate visit. Duplicate visits are paid as well, and they consume office capacity.

Çakıcı and Mills (MSOM 2024; this mission follows the SSRN working-paper version of August 19, 2024) model a provider who splits capacity between an office and a telehealth channel, and patients who choose a channel strategically. Their main finding for the setting in which demand exceeds capacity is that pay parity can make the provider's revenue-maximizing choice and the access-maximizing choice disagree: for a moderate duplicate-visit probability the provider prefers telehealth while patients are better served by an office-only practice. This mission formalizes that result and the equilibrium analysis on which it rests.

Setting

A provider serves at total rate $\mu$ and devotes the fraction $\theta\in[0,1]$ of its capacity, the telehealth commitment, to telehealth. Episodes of care arrive at rate $\lambda$. Each patient balks (value $0$), visits the office, or uses telehealth; a telehealth visit needs a duplicate office visit with probability $q$. A resolved episode is worth $V$; waiting costs $h$ per unit of sojourn time; the co-payments are $c_O$ and $c_T$; an office visit costs an extra inconvenience $\tau$. With $\pi^O,\pi^T$ the proportions choosing the office and telehealth, the expected sojourn times are

$$W^O=\frac{1}{(1-\theta)\mu-(\pi^O+q\pi^T)\lambda},\qquad W^T=\frac{1}{\theta\mu-\pi^T\lambda},$$

and the expected utilities are $V-c_O-\tau-hW^O$ (office) and $V-c_T-hW^T-q(c_O+\tau+hW^O)$ (telehealth). A patient equilibrium is a split $(\pi^B,\pi^O,\pi^T)$ in which every action used is a best response.

The paper assumes $V>h/\mu+c_O+\tau$, $c_T<c_O+\tau$, and, with $\kappa(q)=\frac{h/\mu}{V-c_T-q(c_O+\tau)}$, that $0<\kappa(q)\le 1/(1+\sqrt q)^2$. In the large-market setting some patients balk at every $\theta$. There the equilibrium is of one of four types, by region of $\theta$: balk/office on $[0,\theta^T]$, balk/office/telehealth on $(\theta^T,\theta^O)$, balk/telehealth on $[\theta^O,\bar\theta)$, all-balk on $[\bar\theta,1]$, with explicit thresholds $\theta^T,\theta^O,\bar\theta$ and explicit proportions $\pi^O(\theta),\pi^T(\theta)$. The patient access rate and the provider's revenue rate under telehealth reimbursement $r$ (office revenue $R$) are

$$A(\theta)=\bigl(\pi^O(\theta)+\pi^T(\theta)\bigr)\lambda,\qquad F(r,\theta)=\bigl(R\pi^O(\theta)+(r+Rq)\pi^T(\theta)\bigr)\lambda .$$

The commitment that maximizes telehealth usage in the balk/telehealth region is $\theta^*=\bigl(1-\kappa(q)(1-q)\sqrt q\bigr)/(1+q)$.

Formalization targets

Goal: Proposition 4 with the thresholds of Proposition 3

Fix all parameters except $\theta$ and $q$, with $R>0$. There are thresholds $0<q^\dagger<q^*<1$ such that, for every admissible $q$, pay-parity revenue $F(R,\cdot)$ is maximized over $[0,1]$ at $\theta^*$ when $q<q^*$ and at $0$ when $q>q^*$; access $A$ is maximized at $\theta^*$ when $q<q^\dagger$ and at $0$ when $q>q^\dagger$; and for $q^\dagger<q<q^*$

$$A(\theta^*)<A(0)\qquad\text{and}\qquad F(R,0)<F(R,\theta^*).$$

The thresholds are existential; no closed form is fixed, so the statement survives any later computation of them.

Milestones

In attack order: Lemma 2 (order of $\theta^T,\theta^O$); Theorems 1–3 (where each equilibrium type occurs) and Lemma 3 ($\bar\theta<1$); Theorem 4 (shape of $F$ in $\theta$); Corollaries 1–2 (the maximizers of $F$ and $A$ are $0$ or $\theta^*$); Proposition 3 (the two thresholds). Two further items are not milestones: the uniqueness of the large-market equilibrium proportions, and Proposition 5 (the reimbursement $\tilde r=R(1-q)$ aligns the two objectives).

Significance

The result is the paper's argument against pay parity in acute care: when duplicate visits are neither rare nor frequent, paying telehealth at parity induces the provider to adopt it although fewer patients are then seen. Proposition 5 shows the misalignment disappears under the less-than-parity reimbursement $R(1-q)$, which pays the same per patient seen through either channel. The thresholds $q^*$ and $q^\dagger$ are what turn this into a policy statement about measurable duplicate-visit rates.

The paper proves these results by hand. None of them has a machine-checked proof, and nothing about strategic channel choice with duplicate service exists on Prove2Me. Formalizing them checks a case analysis with four regions, two square-root closed forms and an intermediate-value argument in $q$. The formalization has already exposed two places where the printed statements need a hypothesis (see Formalization scope).

Difficulty

Each step is elementary; the difficulty is bookkeeping. The equilibrium characterization requires solving the indifference conditions in each region and choosing the root of a quadratic that gives stable queues. The shape results require continuity of $A$ and $F$ across region boundaries and concavity of a function of the form $c\theta-\sqrt{\kappa^2+(a-b\theta)^2}$. The obvious comparison of the closed-form values at $0$ and at $\theta^*$ does not suffice on its own: the closed-form value at $\theta^*$ is the revenue only when $\theta^*$ lies in the balk/telehealth region, which fails for some admissible parameters. Whether that failure matters for the maximization is the central question.

Formalization scope

All objects are real-valued closed forms in the namespace TelehealthParity.Access. The definition Setting holds the parameters (the arrival rate is lam, since λ is a Lean keyword), $\kappa,\theta^T,\theta^O,\bar\theta,\theta^*$, the region-wise proportions, $A$, $F$, the large-market condition and the predicate Admissible p q. The definition Equilibrium holds the sojourn times, utilities and the equilibrium predicate. Conventions:

• Lemma 1 (the sojourn times) is adopted as the model, as in the paper; no queueing theory is formalized.
• A channel whose queue is unstable is unavailable: it cannot be used and constrains nothing. This is how the paper discards the unstable root in the balk/telehealth region.
• "Large market" (stated verbally on p. 12) is encoded as $A(\theta)<\lambda$ for all $\theta\in[0,1]$.
• Admissible p q collects $0<q<1$, assumption (6), Lemma 2's ordering condition, the large market, and $(1-q)V-c_T>0$. The last is not printed; the proof of Lemma 2 presumes it, and Lemma 2 fails without it.
• $R>0$ is added where strictness needs it: Theorem 4, the goal, and Proposition 5. The paper allows $R\ge0$.
• Corollary 1 carries the added hypothesis "$r\le R$ or $\theta^O\le\theta^*$". As printed, for every $r>0$, it is false for some $r>R$, where the maximizer is $\theta^O$.
• "Maximized at" is IsMaxOn over $[0,1]$; "linear" is affine.

Excluded trivializations. $A$, $F$ and $\theta^*$ are closed forms, not suprema or argmaxes. The goal states the strict misalignment and the full threshold characterization, not a comparison with one point. A sorry-free sanity check shows that the hypotheses hold on an admissible instance in the misaligned range ($V=4$, $c_T=c_O=\tau=1$, $h=1/2$, $\mu=1$, $\lambda=2$, $q=1/25$).

Welcome contributions are proofs of any milestone. The real-analysis lemmas (concavity of $c\theta-\sqrt{\kappa^2+(a-b\theta)^2}$, maximization of piecewise functions that are continuous across region boundaries) are reusable beyond this mission.

Selected references

• Ö. E. Çakıcı and A. F. Mills, Telehealth in Acute Care: Pay Parity and Patient Access, Manufacturing & Service Operations Management, 2024. https://doi.org/10.1287/msom.2022.0345 (SSRN working paper, version of August 19, 2024, followed here).

Motivation

Online marketplaces such as Amazon are both the storefront of third-party sellers and a retailer in their own right. A platform that observes how well a seller's product sells can later launch a competing product in the same space, and empirical work finds that it does so selectively: Zhu and Liu (2018, Strategic Management Journal) report that Amazon is more likely to enter product spaces with high sales and ratings. A seller who anticipates this faces a strategic choice about how much to invest in her product before the platform decides.

Qi, Song and Xiao (Management Science, 2025) model this interaction as a two-stage game and ask how the seller's investment responds to the threat of entry. Their answer depends on whether the seller ultimately benefits from the platform's entry, which can happen through spillovers: the platform's own investment in the product space also raises the value of the seller's product. This mission formalizes the case in which the seller does not want the platform to enter, the protective regime, and the paper's characterization of her optimal effort there (Proposition 3).

Setting

The parameters are a degree of spillover $\delta\in[0,1]$, a referral rate $f\in[0,1)$ (the share of the seller's revenue paid to the platform), a competition intensity $\beta\in[0,1]$, the seller's effort-cost coefficient $c_S>1/2$, and the platform's fixed entry cost $K>0$. The platform's own cost coefficient is normalized to $c_P=1/2$.

In the first stage the seller's product has base value $a$; she chooses an effort $e_S$ at cost $c_Se_S^2$, raising the value to $a+e_S$, and sells a quantity $q_1$ at price $a+e_S-q_1$, keeping the fraction $1-f$ of revenue. In the second stage the platform, having inferred $a+e_S$, decides whether to enter. If it does, it invests in the product space and the two compete in quantities.

The paper reduces the second stage to closed forms. Write $N_5$ for the left side of condition (5),

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

which says that the seller stays in the market after entry and is assumed throughout. With an explicit polynomial denominator $D$, set $H=N_5^2/D^2$ (equation (8)). The seller's two-stage profits under non-entry and entry are

$$\Pi^S_N(e_S)=\frac{(1-f)(a+e_S)^2}{2}-c_Se_S^2,\qquad \Pi^S_E(e_S)=\Big(\frac14+H\Big)(1-f)(a+e_S)^2-c_Se_S^2 .$$

The platform enters iff the product value exceeds a threshold $\Delta=\sqrt{-4KD/E_N}$, where $E_N$ is a second explicit polynomial in $(\delta,f,\beta)$ (Proposition 1). Hence the seller's total profit is

$$\Pi^S(e_S)=\begin{cases}\Pi^S_N(e_S)&e_S+a\le\Delta,\\ \Pi^S_E(e_S)&e_S+a>\Delta.\end{cases}$$

The protective regime is $\overline\Omega=\{(\delta,f,\beta): H\le 1/4\}$; there $\Pi^S_N\ge\Pi^S_E$ for every effort. The benchmark efforts $e^B_N(a)=(1-f)a/(f+2c_S-1)$ and $e^B_E(a)=a(1-f)(1+4H)/(4c_S-(1-f)(1+4H))$, equations (9)–(10), maximize $\Pi^S_N$ and $\Pi^S_E$ respectively.

Formalization targets

Goal: Proposition 3

In the protective regime, with $\underline a_1$ defined by $\underline a_1+e^B_N(\underline a_1)=\Delta$, there is $\bar a_1\ge\underline a_1$ such that an optimal effort is

$$e^*_S(a)=\begin{cases}e^B_N(a)&a\le\underline a_1,\\ \Delta-a&a\in(\underline a_1,\bar a_1),\\ e^B_E(a)&a\ge\bar a_1,\end{cases}$$

and the optimal first-stage quantity is $q_1^*=(a+e^*_S(a))/2$.

Milestones

1. Proposition 1: under (5) and $K>0$, $\Delta>0$ and the platform's gain from entry is positive iff $a+e_S>\Delta$.
2. Equations (9)–(10): $e^B_N$ and $e^B_E$ are the unique unconstrained maximizers.
3. $e^B_N(a)\ge e^B_E(a)$ for $a>0$ when $H\le 1/4$.
4. With $M(a)=\Pi^S_N(\Delta-a)-\Pi^S_E(e^B_E(a))$: $dM/da=2c_S(\Delta-a-e^B_E(a))$.
5. $M(\underline a_1)\ge 0$.
6. Cases 1.1, 1.2 and 1.3 of the proof: optimality of each of the three efforts on its region.

Significance

The result identifies strategic underinvestment as the seller's response to an unwelcome entrant: for intermediate base values she chooses less effort than her first-best so that the product's value sits exactly at the entry threshold. For low base values no distortion is needed, and for high ones the required distortion costs more than entry does. This explains why a seller's investment may fall short of what her own costs and demand would justify, and it is the starting point of the paper's analysis of non-entry commitments (Proposition 5).

The result is proved in the paper; nothing here is open. No part of it is formalized. A machine-checked version adds a complete check of a proof that compresses several steps into "verifiable" remarks: the positivity of $D$ and the sign of $E_N$ under (5), and the single sign change of $dM/da$ that defines $\bar a_1$.

Difficulty

The seller's objective $\Pi^S$ is discontinuous at $e_S=\Delta-a$, so the first-order condition alone does not locate the optimum: the candidates are the two unconstrained maximizers and the cutoff, and which one wins depends on $a$. The step that needs care is the existence of a single switching point $\bar a_1$: it requires comparing the value of the constrained non-entry problem with the unconstrained entry optimum as a function of $a$, and showing that the comparison changes sign once. The polynomial sign facts behind $\Delta$, namely $D>0$ and $E_N<0$ on the parameter box under (5), are elementary but involve quartic polynomials in three variables.

Formalization scope

All quantities are real numbers. The standing ranges $\delta,\beta\in[0,1]$, $f\in[0,1)$, $c_S>1/2$ are hypotheses, as are condition (5) (assumed by the paper from p. 12 on) and $K>0$ (not stated by the paper, but presupposed by its formula for $\Delta$; with $K\le 0$ the threshold degenerates to 0). Only the branch of $\Delta$ and $\Pi^P_{E-N}$ for which (5) holds is formalized; the paper's proof also covers the regime where (5) fails, with $H=0$.

The closed forms (6), (7), the entry gain $\Pi^P_{E-N}$ and $\Delta$ are definitions taken from the paper. Their derivation from the second-stage Cournot game (Lemmas 1–2) is the subject of the companion mission On the Platform’s Entry I. The piecewise profit $\Pi^S$ is the printed one, with the tie $e_S+a=\Delta$ assigned to non-entry.

Efforts range over all of $\mathbb R$. This is the paper's implicit domain and it matters: the optimal effort $\Delta-a$ is negative for some parameters (for instance $\delta=f=0$, $\beta=1/2$, $c_S=K=1$ and $a$ slightly above $\Delta$), so a version restricted to $e_S\ge 0$ would be false. "Optimal" means a global maximizer, with ties allowed; at $a=\bar a_1$ two efforts are optimal and at $H=1/4$ the middle interval is empty.

Trivializing formalizations are ruled out: $\underline a_1$ is pinned by its defining equation rather than chosen, every hypothesis is satisfiable (at $\delta=f=0$, $\beta=1/2$ one has $H=676/9409\le 1/4$), and the sign conditions keep $\Delta$ from collapsing to a junk value of division or square root.

A complete development needs only real analysis of quadratics and polynomial inequalities on a box; contributions of reusable lemmas on maximizing concave quadratics under a threshold constraint are welcome.

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
• 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

Motivation

Small third-party sellers on e-commerce marketplaces often lack working capital to buy inventory. Two financing channels compete for them. Under trade credit, the supplier ships now and is paid after sales, bearing the seller's default risk. Under platform financing, the marketplace itself (Amazon Lending, Alibaba's microloans, JD's supply-chain finance) lends the seller the purchase cost at an interest rate it chooses, the supplier is paid upfront, and the platform bears the default risk. A platform that already earns a commission on every sale has a reason to lend that a bank does not: cheaper credit raises orders, and higher orders raise commission income.

R. Huang, G. Lai, X. Wang and W. Xiao study this in Platform Financing vs. Trade Credit for Lending to Third-Party Sellers (Management Science, 2024). Their §5 asks how a platform that can set its loan rate freely would set it. The answer at low demand uncertainty is a clean dichotomy in the production cost: the platform lends at exactly its own capital cost when cost is low, and strictly below its capital cost, subsidizing the loan, when cost is high. This mission formalizes that result, Proposition 8, together with the equilibrium analysis it rests on.

The source is the authors' manuscript on SSRN (abstract 4014045, titled Lending to Third-party Sellers with Platform Loan); every page and label below refers to that manuscript, not to the typeset journal article.

Setting

A seller with no capital buys $q \ge 0$ units from a supplier whose unit production cost is $c > 0$, and sells all of them on a platform at the market-clearing price $p = \tilde a - q$. The market size $\tilde a$ is uniform on $[a - \delta, a + \delta]$ with $0 < \delta < a$; $\delta$ measures demand uncertainty. The platform keeps a share $\varphi \in [0, 1)$ of revenue and passes $(1 - \varphi)pq$ to the seller. The supplier and the platform both have capital cost equal to the risk-free rate $r_f \ge 0$, and selling is profitable in expectation: $(1 - \varphi)a > c(1 + r_f)$.

Under platform financing at loan rate $r > -1$, the game has two stages after $r$ is fixed:

1. the supplier sets an upfront wholesale price $w$ and receives $(w - c)q(1 + r_f)$ in value;
2. the seller, having seen $w$, borrows $wq$ from the platform and chooses $q$ to maximize $\mathbb E\big[((1 - \varphi)(\tilde a - q)q - wq(1 + r))^+\big]$.

The seller has limited liability: if revenue $(1 - \varphi)(\tilde a - q)q$ falls short of the debt $wq(1 + r)$, she hands over all of it. The platform's profit is

$$\Pi^P_p = \mathbb E\big[\varphi(\tilde a - q)q + \min\{(1 - \varphi)(\tilde a - q)q,\ wq(1 + r)\}\big] - wq(1 + r_f).$$

A subgame-perfect equilibrium at rate $r$ is a price $w$ and an order rule $w' \mapsto q(w')$ such that the rule is a best response for the seller at every price, the supplier's price is optimal against the rule, and ties are broken as in the paper. The paper also defines a threshold rate $\hat r_1(\delta)$ (p. 15) below which the seller prefers platform financing to trade credit; the platform chooses $r$ subject to the participation constraint $r \le \hat r_1(\delta)$. Write

$$\delta_2 = \frac{(1 - \varphi)a - c(1 + r_f)}{(2 + \sqrt6)(1 - \varphi)}, \qquad \bar c = \frac{a(1 - \varphi)^2}{1 + r_f}.$$

Formalization targets

Goal: Proposition 8 (p. 22)

Let $\Pi^P_p(r)$ be the platform's profit in a subgame-perfect equilibrium of the stage game at rate $r$, for an arbitrary choice of equilibrium at each feasible rate. If $\delta \le \delta_2$, then

$$c \le \bar c \implies r^* = r_f \text{ is the unique maximizer of } \Pi^P_p \text{ on } \{-1 < r \le \hat r_1(\delta)\},$$ $$c > \bar c \implies \text{a maximizer exists, and every maximizer } r^* \text{ satisfies } r^* < r_f.$$

Milestones

1. Lemma 2 (p. 13): the seller's unique best response to $(w, r)$, with a no-default branch and a default branch.
2. Proposition 2 (p. 13): the stage game has an equilibrium, and in every equilibrium $w^P$ and $q^P$ have the stated closed forms, switching at $\delta_r = \frac{a(1-\varphi) - c(1+r)}{(2+\sqrt6)(1-\varphi)}$.
3. (10) (pp. 35, 41): for $\delta \le \delta_r$, the platform's equilibrium profit is an explicit rational function of $r$.
4. The derivative (p. 43): $\partial \Pi^P_p(r)/\partial r = G_1(r)/(8(1-\varphi)^2(1+r)^2)$ with an explicit cubic $G_1$.
5. Case (a) (p. 43): $c \le \bar c$ implies $G_1 \ge 0$ on $(-1, r_f]$.
6. Case (b) (p. 43): $c > \bar c$ implies $G_1$ is nonnegative up to some $r_7 < r_f$ and negative on $(r_7, r_f]$.

Significance

The result separates two motives for platform lending. At low cost the platform gains nothing by undercutting its own capital cost, so the loan is priced at cost; at high cost the commission earned on the extra units ordered outweighs the interest forgone, so the platform subsidizes. The threshold $\bar c$ is explicit and depends only on the mean market size, the commission share and the risk-free rate. Together with Proposition 7 of the same paper (whether the platform gains relative to trade credit), it is the paper's account of why marketplaces lend below market rates.

The proof in the paper is a chain of closed-form computations whose final steps are stated as "it can be verified". A formalization checks that chain end to end: the equilibrium of a limited-liability Stackelberg game with uniform demand, the reduction of the platform's objective to (10), and the sign analysis of $G_1$. To our knowledge none of these steps has been machine-checked. The model file (uniform expectation, limited-liability payoffs, the equilibrium predicate with tie-breaks) is reusable for the two sister missions on the same paper and for other supply-chain-finance models with a uniform market-clearing price.

Difficulty

The objective is defined through an equilibrium, not a formula. The obvious approach, substituting the closed forms of Proposition 2 into the platform's profit, presupposes that every equilibrium has those closed forms; establishing this means solving the seller's piecewise problem (whose objective changes form where default becomes possible), then the supplier's problem over a piecewise best response, and handling the indifference point $\delta = \delta_r$. Only then does the problem reduce to the one-variable function (10).

On that function, the low-cost case requires a polynomial inequality on a half-open interval in four parameters, and uniqueness needs strict monotonicity, not just a nonnegative derivative. The high-cost case requires both a single sign change of a cubic on $(-1, r_f]$ and the existence of a maximizer on a set that is open at $-1$, where the profit tends to $-\infty$.

Formalization scope

All objects live in the namespace PlatformFinance.EndogRate. Conventions committed to:

• The expectation over $\tilde a$ is $\frac{1}{2\delta}\int_{a-\delta}^{a+\delta}$, an interval integral of a continuous integrand.
• The standing assumptions are hypotheses: $0 < \delta$, $\delta < a$ (the reading of p. 8's "the smallest market size $a - \delta$ is large enough so that the market clearing price is always positive"), $0 \le \varphi < 1$ (the page allows $\varphi = 1$, which $(1 - \varphi)a > c(1 + r_f)$ excludes), $c > 0$, $r_f \ge 0$, $(1 - \varphi)a > c(1 + r_f)$, and for platform financing $r > -1$ and $c(1 + r) < (a + \delta)(1 - \varphi)$ (conditions (iii) and (ii), p. 36).
• The equilibrium carries the paper's two tie-breaks: a seller who cannot earn a positive expected profit orders zero (proofs on pp. 31, 33), and the supplier's equilibrium price is the least optimal one (which puts $\delta = \delta_r$ in Proposition 2's first branch).
• The goal quantifies over an arbitrary family of equilibria, one per feasible rate; Proposition 2 shows such a family exists. The feasible set is $\{r : -1 < r \le \hat r_1(\delta)\}$ with $\hat r_1$ the paper's closed form on p. 15.
• Lemma 2 assumes $w(1 + r) < (1 - \varphi)(a + \delta)$: above it every order earns zero and the maximizer is not unique; the paper's proof restricts to this range.

Corrections relative to the page: (10) is printed under the heading "the equilibrium profits under trade credit" on p. 35, a slip for platform financing; Proposition 8 states $\delta \le \delta_2$ while its proof writes $\delta < \delta_2$, and the statement follows Proposition 8.

A trivializing formalization is ruled out: the goal is stated about the platform's equilibrium profit, not about the closed form (10), and the high-cost clause asserts existence of a maximizer so that "every maximizer is below $r_f$" cannot hold vacuously.

Needed infrastructure: interval integrals of piecewise polynomials, optimization of one-variable piecewise functions, and real-polynomial sign arguments. Proofs of any milestone are welcome, as are alternative proofs of the cubic sign analysis.

Selected references

• R. Huang, G. Lai, X. Wang, W. Xiao, Lending to Third-party Sellers with Platform Loan, SSRN manuscript 4014045. https://ssrn.com/abstract=4014045
• R. Huang, G. Lai, X. Wang, W. Xiao, Platform Financing vs. Trade Credit for Lending to Third-Party Sellers, Management Science, 2024. https://doi.org/10.1287/mnsc.2022.00201