Algorithmic Game Theory

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

Motivation

Financial firms owe each other money. When some firms cannot meet their obligations, the payments that actually clear in the network are a fixed point: what a firm can pay depends on what it receives, which depends on what others can pay. Eisenberg and Noe (Management Science, 2001) introduced this clearing model under a fixed pro-rata payment rule. Later work asked what happens when firms choose how to pay their creditors, which turns the clearing problem into a game.

Bertschinger, Hoefer and Schmand (arXiv:1908.01714v3; Mathematics of Operations Research, 2025) study this game in an abstract form, the flow allocation game. Each node of a directed network receives a fixed external supply plus whatever flows in, and decides how to split its total supply among its outgoing edges, subject to edge capacities. Each node wants to maximize its own total outflow (its payments, which in the financial reading is what keeps it solvent). The paper's first main result is that, when strategies rank single units of flow, there is always a strong equilibrium, stable against every coalition, which is at the same time socially optimal for the total flow.

Timeline:

• 2001: Eisenberg and Noe, clearing payments under pro-rata rules, existence of a greatest clearing vector.
• 2018: Csóka and Herings (Management Science): decentralized clearing with integral monotone allocation rules; the feasible flows form a complete lattice (restated for all monotone profiles as Theorem 2 of the present paper).
• 2019–2025: Bertschinger, Hoefer and Schmand, strategic allocation; existence of optimal strong equilibria for unit-ranking strategies (Theorem 9), strong price of anarchy bounded by the min-max cycle length (Theorem 16), hardness results for other welfare functions and for edge-ranking strategies.

Setting

A flow allocation game $\Gamma = (G, (b_v)_{v\in V}, (c_e)_{e\in E})$ consists of a finite directed multigraph $G = (V, E)$, a fixed supply $b_v \in \mathbb N_0$ at each node and a capacity $c_e \in \mathbb N_0$ on each edge. $E^+(v)$ and $E^-(v)$ are the outgoing and incoming edges of $v$, and $c^+_v = \sum_{e\in E^+(v)} c_e$.

Every node is a player. A strategy profile $\mathbf a = (a_e)_{e\in E}$ assigns to each edge an allocation function $a_e : \mathbb N_0 \to \mathbb N_0$: when the tail of $e$ has total supply $y$, it forwards $a_e(y)$ units on $e$. The profile is unit-ranking if for all $y$, $e$, $v$: $a_e(y) \le c_e$ (1); $\sum_{e\in E^+(v)} a_e(y) \le y$ (2); $\sum_{e\in E^+(v)} a_e(y) = \min\{c^+_v, y\}$ (no fraud, (3)); and each $a_e$ is non-decreasing (5). Equivalently, every node ranks the single units of its outgoing capacity.

A flow $\mathbf f \in \mathbb N_0^E$ gives node $v$ the total supply $f_v = b_v + \sum_{e\in E^-(v)} f_e$, and is feasible for $\mathbf a$ if $f_{(v,w)} = a_{(v,w)}(f_v)$ on every edge (4). The clearing state $\hat{\mathbf f}$ of $\mathbf a$ is the coordinatewise supremum of the feasible flows. 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 unit-ranking profile $\mathbf a$ is a strong equilibrium if no non-empty coalition $C \subseteq V$ has a joint deviation $\mathbf a'_C$ such that $(\mathbf a'_C, \mathbf a_{-C})$ is unit-ranking and $u_v(\mathbf a'_C, \mathbf a_{-C}) > u_v(\mathbf a)$ for all $v \in C$.

The circulation network $G'$ adds a node $s$, an uncapacitated edge $(v, s)$ and an edge $(s, v)$ of capacity $b_v$ for every $v$. An optimal circulation $f^*$ maximizes the total flow over all edges of $G'$.

Formalization targets

Goal: Theorem 9 (first sentence)

$$\exists\, \mathbf a:\quad \mathbf a \text{ is a strong equilibrium} \ \text{ and } \ \mathrm{Flow}(\mathbf a') \le \mathrm{Flow}(\mathbf a) \text{ for every unit-ranking } \mathbf a'.$$

Milestones (in the order of the proof)

1. Theorem 2 (p. 12, integral version p. 13): for a monotone profile the feasible flows form a non-empty complete lattice; the clearing state is its greatest element.
2. Proposition 5 (p. 17): a feasible flow, with the non-forwarded flow $\max\{0, f_v - c^+_v\}$ sent to $s$, is a circulation of $G'$, and $\sum_v \max\{0, f_v - c^+_v\} = \sum_v b_v$.
3. Proof of Theorem 9, p. 23, first display: an optimal circulation saturates every $(s, v)$ and

$$\sum_{e\in E'} f^*_e = 2\sum_v b_v + \mathrm{Flow}(f^*) \ge 2\sum_v b_v + \mathrm{Flow}(\mathbf a).$$

4. Proof of Theorem 9, p. 23: with thresholds $\tau_e = f^*_e$ and arbitrary rankings, the threshold-ranking profile $\mathbf a^*$ is unit-ranking and its clearing state is $f^*$.
5. Proof of Theorem 9, pp. 23–24: a profitable coalitional deviation from a unit-ranking profile produces a cycle of $G$ on which the new clearing state carries strictly more flow.

Companion: Corollary 12

For every flow-monotone $Q$ (if $\hat{\mathbf f} > \hat{\mathbf f}'$ then $Q(\mathbf a) \ge Q(\mathbf a')$) there is a strong equilibrium maximizing $Q$ over all unit-ranking profiles.

Significance

Strong equilibria rarely exist in network games, and when they do they are usually not efficient. Theorem 9 gives both at once: every unit-ranking game has a strong equilibrium, and one of them maximizes the total flow, so the price of stability for $\mathrm{Flow}$ is $1$. Corollary 12 extends this to every flow-monotone welfare function, including egalitarian welfare, Nash social welfare and the number of solvent firms. In the financial reading, a coalition of firms cannot jointly reorder its payments to make every member better off, and the stable payment pattern can be chosen to clear the largest possible volume of debt.

The results are proved in the paper and, to our knowledge, have no machine-checked proof. Formalizing them yields a reusable Lean development of clearing states (the Knaster–Tarski structure of feasible flows), the circulation representation of feasible flows, and integral maximum circulations with a cycle-augmentation argument. The second mission of this series (strong price of anarchy, Theorem 16) builds on the same model.

Difficulty

The obvious argument fails at the deviation step. After a coalition deviates, the clearing state of the new profile is an implicit object: the greatest fixed point of a map that mixes the deviators' new strategies with everyone else's old ones. Nothing ties it pointwise to the optimal circulation, and comparing utilities alone gives no contradiction, because a deviator's gain can be paid for by flow that appears elsewhere in the network. The increase of flow has to be traced through deviators and non-deviators alike, and the two kinds of node obey different constraints.

A second difficulty is that the threshold profile built from an optimal circulation $f^*$ has clearing state exactly $f^*$. The clearing state is a supremum over all feasible flows, so it is not enough that $f^*$ is feasible. The claim depends on optimality: for a circulation that is not optimal it is false, as a two-node cycle carrying one unit on edges of capacity two already shows.

Formalization scope

All data are natural numbers: supplies, capacities, strategies $a_e : \mathbb N \to \mathbb N$ and flows, as the paper prescribes for unit-ranking games (p. 13). The graph is a finite type of edges with tail and head maps, so multi-edges and self-loops are allowed. A profile is one function on edges. The clearing state is the coordinatewise sSup in $\mathbb N$; the definition does not assume that the supremum is a feasible flow, which is milestone 1. Optimal circulations are optimal among integral circulations, which the paper justifies by integrality of capacities (p. 23). Natural-number subtraction is used only where it is the page's $\max\{0,\cdot\}$.

Coalitions are non-empty. With $C = \emptyset$ the condition "every member strictly gains" holds vacuously and no profile would be a strong equilibrium; the paper reads it the same way (Proposition 4, Proposition 17). Deviations must again be unit-ranking profiles; the broader deviations of Remark 10 are not formalized. The maximization in the goal ranges over all unit-ranking profiles, not over threshold-ranking ones. A goal maximizing only over threshold profiles, or one that drops the optimality conjunct, is a strictly weaker theorem and is ruled out.

Out of scope: the second sentence of Theorem 9 (polynomial-time computation and polynomial-space representation) and the polynomial-space sentence of Corollary 12. Both need a model of computation. The threshold representation behind them is milestone 4.

A complete development needs: Knaster–Tarski on a finite product of intervals (Mathlib's OrderHom fixed-point lattice), flow conservation bookkeeping on finite multigraphs, existence of integral optimal circulations, and extraction of a cycle from an infinite backward walk in a finite graph. The last two are reusable beyond this mission. Proofs of any milestone, and sorry-free lemmas about clearing states, are welcome.

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.01714v3
• 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
• P. Csóka, P. J.-J. Herings, Decentralized Clearing in Financial Networks, Management Science 64(10), 4681–4699, 2018. https://doi.org/10.1287/mnsc.2017.2847
• A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics 5(2), 285–309, 1955. https://doi.org/10.2140/pjm.1955.5.285

Motivation

Firms that sell to the same customers over time learn who bought from whom. Behavior-based pricing (BBP) — charging a firm's own past customers one price and the rival's past customers another — has been studied since Fudenberg and Tirole (2000) and Villas-Boas (1999). A second instrument is the disclosure of product quality: free samples, demonstrations and trial versions reveal the quality of a new product, at a cost per customer reached. With purchase histories, a firm can disclose differently to its own customers and to the rival's: behavior-based disclosure (BBD). The classical disclosure model is Jovanovic (1982), in which costly disclosure leads a firm to reveal quality only above a threshold.

Zhang and Li (2025) combine the two instruments in a two-period Hotelling duopoly and compare BBD with uniform disclosure. Their Proposition 1 shows that BBD always raises second-period profits; this mission is about the whole game, where the answer depends on the disclosure cost.

Setting

A unit mass of customers is uniformly distributed on $[0,1]$; firm A is at $0$, firm B at $1$, the transportation cost is $1$, marginal costs are $0$ and the market is fully covered.

Period 1. The firms charge prices $p_{a1},p_{b1}\ge 0$. The first-period purchase splits the line at $x_1$: A's old customers are $[0,x_1]$ (A's turf), B's are $[x_1,1]$ (B's turf).

Period 2. Each firm $i$ launches a new product of quality $q_i$, with $q_a,q_b$ independent and uniform on $[0,1]$. A firm discloses its quality to a segment iff it exceeds a disclosure threshold $\hat q$; disclosing costs $c$ per customer reached. A segment that sees no disclosure believes the quality is $\hat q/2$. Under uniform disclosure each firm has one threshold $\hat q_i$ for the whole line; under BBD it has $\hat q_{io}$ for its own customers and $\hat q_{in}$ for the rival's. On each turf the two firms then play a price game (A charges $p_{ao}$ and B charges $p_{bn}$ on A's turf; $p_{an}$ and $p_{bo}$ on B's turf), and customers stay or switch according to their beliefs and prices.

Forward-looking customers. The share $x_1$ is the location of the marginal consumer, who compares the two first-period options including the expected second-period surplus of staying or switching ((6) for uniform disclosure, (15) for BBD):

$$-x_1-p_{a1}+\max\{-(1-x_1)+E(\tilde q_{bn}-p^*_{bn}),\,-x_1+E(\tilde q_{ao}-p^*_{ao})\}=-(1-x_1)-p_{b1}+\max\{-x_1+E(\tilde q_{an}-p^*_{an}),\,-(1-x_1)+E(\tilde q_{bo}-p^*_{bo})\}.$$

Two-period profits (8) are $\Pi_a=p_{a1}x_1+E(\pi_{a2})$ and $\Pi_b=p_{b1}(1-x_1)+E(\pi_{b2})$, with $E(\pi_{i2})$ the ex ante second-period profit at share $x_1$. A symmetric subgame-perfect equilibrium is a common first-period price $p^*$ together with a second-period equilibrium at every share and a consistent share at every price pair, such that neither firm gains from any other nonnegative first-period price. Its total profits are $\Pi^*_a,\Pi^*_b$.

The standing assumption is $0<c<5/36$ (p. 8515).

Formalization targets

Goal: Proposition 3(a)

There is a cutoff $c_l\in(0,5/36)$ such that for every $c\in(0,5/36)$, symmetric subgame-perfect equilibria exist under both regimes and, for any two of them,

$$c>c_l\;\Rightarrow\;\Pi^{*,U}_i<\Pi^{*,BBD}_i,\qquad c<c_l\;\Rightarrow\;\Pi^{*,BBD}_i<\Pi^{*,U}_i\qquad (i=a,b).$$

The value of $c_l$ is left unfixed, as in the paper.

Milestones

1. (5) and (14): the ex ante second-period profit as a function of $x_1$ and the equilibrium thresholds, in region 1, e.g. under BBD

$$E(\pi_{a2})=\tfrac{(1+2x_1)^2+(3-4x_1)^2}{18}+\tfrac{4-\hat q_{ao}^3-\hat q_{an}^3-\hat q_{bo}^3-\hat q_{bn}^3}{216}-c\,[1-x_1\hat q_{ao}-(1-x_1)\hat q_{an}].$$

2. (7) and (16): in region 1 the first-period share is $x_1=\tfrac12+\tfrac38(p_{b1}-p_{a1})$ under both regimes.
3. (9) and (17): existence of symmetric equilibria, and their prices

$$p^{*,U}=\tfrac23\big(2-c+\tfrac{c}{\sqrt{1+27c}}\big),\qquad p^{*,BBD}=\tfrac43-\tfrac{c(5+54c)}{3\sqrt{1+12c}}+\tfrac{c(5+162c)}{3\sqrt{1+108c}},$$

with share $x_1^*=\tfrac12$. 4. Table 1, total profits, both regimes, in closed form. 5. Proposition 2: a cutoff $c_h\in(0,5/36)$ across which the comparison of first-period prices and profits reverses.

Significance

Proposition 3(a) is the paper's answer to the managerial question in its title. BBD lets a firm disclose to its own customers more often than to the rival's (retention-focused disclosure), which improves the efficiency of disclosure and raises second-period profits. In the first period, however, BBD changes how hard firms compete for customers, and when disclosure is cheap the first-period loss dominates. The result locates the sign change of the total effect at a single cutoff, and together with Proposition 2 ($c_l<c_h$) it separates three regimes of $c$: total profits fall, total profits rise despite lower first-period profits, and both rise.

None of these results is formalized anywhere. The paper's proofs are in an Online Appendix and its displayed formulas are the end points of long computations. A complete development would produce:

• a machine-checked solution of a two-period Hotelling model with behavior-based pricing, including corner regions of the second-period price game;
• a costly-disclosure equilibrium in the Jovanovic style;
• a verified single-crossing analysis of algebraic functions of $c$.

Difficulty

The model nests three equilibrium notions: a clamped price game on each turf, threshold disclosure as a best response to the rival and to the induced beliefs, and first-period pricing with forward-looking customers. The first-order condition behind (9) and (17) involves the derivative of $E(\pi_{a2})$ in $x_1$, and every threshold, including the rival's, moves with $x_1$; treating the rival's thresholds as fixed gives a wrong price.

The symmetric first-order condition alone does not settle the equilibrium. A deviation in first-period price can push the share outside the region where all second-period prices are interior, into the corner regions 2 and 3 of Lemma 1/2, where the second-period profit has a different form. The paper checks these deviations only in its Online Appendix.

The final comparison is a sign analysis of an expression with three different square roots on $(0,5/36)$. The difference of total profits is small throughout: for example, about $-5\cdot10^{-4}$ at $c=0.01$ and $3.5\cdot10^{-3}$ at $c=0.1$.

Formalization scope

• Representation. Qualities are integrated by iterated interval integrals over $[0,1]$. The base value $v$ cancels and is omitted; full coverage is built in. Prices are nonnegative, turf shares are clamped to the turf, and the nondisclosure belief stays $\hat q/2$ when a firm considers a deviation.
• Equilibria, not formulas. Second-period prices are Nash equilibria of the clamped turf games for every belief pair in $[0,1]^2$. Thresholds are best responses ("disclose iff $q>\hat q$" is optimal), never roots of the indifference equation. The share satisfies (6)/(15) as printed, a maximum of two expectations, with corner shares $x_1\in\{0,1\}$ read through nearby interior shares (at an endpoint one turf is empty and its second-period prices are not pinned down, so (6)/(15) is not evaluated there). First-period deviations range over all nonnegative prices, and the second-period profile is an equilibrium at every share, including shares reached only after a deviation.
• Readings. "In region 1" for (5), (7), (14), (16) means that every belief pair on the support is in region 1: $\tfrac12-\hat q_{bn}/8<x_1<\tfrac12+\hat q_{an}/8$ (BBD), $\tfrac12-\hat q_b/8<x_1<\tfrac12+\hat q_a/8$ (uniform). Table 1's uniform total profit is used; the sentence on p. 8517 prints $\sqrt{1+72c}$ for $\sqrt{1+27c}$.
• Ruled out. Hard-wiring $x_1=\tfrac12$, defining thresholds or prices by their closed forms, or stating the goal on the Table 1 formulas alone would each trivialize the mission; the cutoff is quantified before $c$ and lies strictly inside $(0,5/36)$, and existence of equilibria is part of the goal.
• Not posed. Proposition 3(b), (c) (consumer surplus and welfare are defined in the paper only by their Table 1 values) and Proposition 4.
• Needed. Piecewise-quadratic integrals over the belief support; Nash equilibria of clamped linear-demand games; existence of a consistent first-period share (an intermediate-value argument on a suitable equilibrium selection); and sign analysis with square roots. The second-period model is the same as in the companion mission on Proposition 1, and lemmas about it are reusable there. Contributions of any of the milestones, of Lemma 1/2 in all regions, or of the corner-region versions of (4), (5), (13), (14) are welcome.

Selected references

• J. Zhang and K. J. Li, Retention or Acquisition? Behavior-Based Quality Disclosure, Management Science 71(10), 8510–8525, 2025. https://doi.org/10.1287/mnsc.2022.01081
• D. Fudenberg and J. Tirole, Customer Poaching and Brand Switching (cited in Zhang and Li as "Customer poaching and firm switching"), RAND Journal of Economics 31(4), 634–657, 2000.
• J. M. Villas-Boas, Dynamic Competition with Customer Recognition, RAND Journal of Economics 30(4), 604–631, 1999.
• B. Jovanovic, Truthful Disclosure of Information, Bell Journal of Economics 13(1), 36–44, 1982.