Optimization

Motivation

Online marketplaces such as Airbnb, Upwork and eBay match buyers and sellers but do not set transaction prices. They earn revenue through commissions (a fraction of the transaction price) and subscription fees (a fixed charge per transaction), and they often differentiate these fees by participant type. Prices then form endogenously, as a competitive equilibrium of the market the fees induce. Choosing revenue-maximizing fees is therefore a bilevel problem: the platform optimizes over fees, and every choice of fees changes the equilibrium prices and trades. Birge, Candogan, Chen and Saban (SSRN 3259716; published in Manufacturing & Service Operations Management, doi:10.1287/msom.2019.0853) show that, despite its nonconvexity, this problem is solved exactly by a convex program, and they characterize all optimal fee profiles. The rest of their paper, which compares commissions with subscriptions and studies how the network shapes revenue, rests on this result.

Setting

There are finitely many seller types $\mathcal S$ and buyer types $\mathcal B$. A bipartite compatibility network $E\subseteq\mathcal S\times\mathcal B$ says which types can trade; every type has degree at least one. Type $i$ consists of a continuum of sellers of mass $s_i>0$, and type $j$ of buyers of mass $b_j>0$. A type-$j$ buyer's value is distributed according to $F_{b_j}$ on $[0,\bar v_{b_j}]$, and a type-$i$ seller's reservation value according to $F_{s_i}$ on $[0,\bar v_{s_i}]$, with $\bar v\in\mathbb R_+\cup\{\infty\}$. A buyer who trades with a type-$i$ seller incurs a disutility $c_i\ge 0$. Assumption 1 asks that each $F$ be continuous, continuously differentiable and strictly increasing on $(0,\bar v)$, with bounded mean. Its inverse is $F^{-1}$.

The platform picks commissions $\gamma=(\gamma^s,\gamma^b)$ and subscriptions $\mu=(\mu^s,\mu^b)$ in $\Gamma\times\mathcal U$: $\gamma^s_i\in[0,1]$ and $\gamma^b_j,\mu^s_i,\mu^b_j\ge0$. A competitive equilibrium $(p,x,q^s,q^b)\in\mathcal X(\gamma,\mu)$ consists of prices $p\ge 0$, flows $x_{ij}\ge0$ on $E$ and supplies and demands with

$$q^s_i=s_iF_{s_i}\big((1-\gamma^s_i)p_i-\mu^s_i\big),\qquad q^b_j=b_j\Big[1-F_{b_j}\Big(\min_{i':(i',j)\in E}\{(1+\gamma^b_j)p_{i'}+c_{i'}\}+\mu^b_j\Big)\Big],$$

markets clearing ($q^s_i=\sum_jx_{ij}$, $q^b_j=\sum_ix_{ij}$), and buyers trading only with their cheapest compatible sellers. The revenue problem (3) is

$$V_{opt}=\max\ \sum_{(i,j)\in E}(\gamma^s_i+\gamma^b_j)p_ix_{ij}+\sum_{(i,j)\in E}(\mu^s_i+\mu^b_j)x_{ij}\quad\text{s.t. }(p,x,q^s,q^b)\in\mathcal X(\gamma,\mu),\ (\gamma,\mu)\in\Gamma\times\mathcal U.$$

Assumption 2 asks that $uF^{-1}_{b_j}(1-u)$ and $-uF^{-1}_{s_i}(u)$ be strictly concave in $u\in[0,1]$, a regularity condition on both sides of the market. The relaxation (7) is

$$\tilde V_{opt}=\max_{x,q^s,q^b}\ h(q^s,q^b)=\sum_{j}F^{-1}_{b_j}\Big(1-\frac{q^b_j}{b_j}\Big)q^b_j-\sum_iF^{-1}_{s_i}\Big(\frac{q^s_i}{s_i}\Big)q^s_i-\sum_ic_iq^s_i$$

over flows on $E$ with marginals $(q^s,q^b)$, $q^b\le b$ and $q^s\le s$.

Formalization targets

Goal: Theorem 1 (p. 13)

Let $(\bar x,\bar q^s,\bar q^b)$ be an optimal solution of (7). Then (i)

$$V_{opt}\ \text{is attained and}\ V_{opt}=\tilde V_{opt}=h(\bar q^s,\bar q^b),$$

and every optimal solution of (3) has supply-demand vector $(\bar q^s,\bar q^b)$. (ii) For $(\gamma,\mu)\in\Gamma\times\mathcal U$ with $\gamma^s<1$, with $\tilde\gamma^s_i=1/(1-\gamma^s_i)$, $\tilde\mu^s_i=\mu^s_i/(1-\gamma^s_i)$, $\tilde\gamma^b_j=1/(1+\gamma^b_j)$ and $\tilde\mu^b_j=\mu^b_j/(1+\gamma^b_j)$, the pair is optimal if and only if some $p\ge0$ and some optimal flow $x$ of (7) solve the linear system (8a)–(8f).

Milestones

In the order the proof uses them:

• Proposition 1: equilibria exist and are essentially unique.
• Corollary 1: equilibrium revenue is well defined.
• The bound (6): every equilibrium is feasible for (7), with revenue at most $h(q^s,q^b)$.
• Lemma EC.1(ii): regularity of the pieces of $h$.
• Proposition EC.1(i), (iv), (v), (iii) at problem (7): existence, uniqueness of $(\bar q^s,\bar q^b)$, $\bar q^b<b$, and KKT multipliers (EC.3).
• Step (i-2): the subscription-only fees (EC.104) attain $\tilde V_{opt}$.
• Theorem 1(i) on its own.

Significance

The result turns a nonconvex bilevel problem into a convex network-flow problem with separable concave objective: the optimal supply-demand vector is computed without reference to fees or prices. Part (ii) describes the whole set of optimal fees as solutions of a linear feasibility system, which is what the paper uses to compare fee structures: a subscription-only profile is always optimal (Step (i-2)), and the comparisons with homogeneous and one-sided fees (Propositions 4–6) and the analysis of which network positions earn surplus (Theorems 2–3) start from it. No machine-checked version of these results exists on the platform. The mission formalizes the statement chain of the paper's proof (main text and e-companion), including the equilibrium existence and uniqueness of Proposition 1 and the KKT theory of the relaxation.

Difficulty

The bound $V_{opt}\le\tilde V_{opt}$ is a rearrangement. Equality needs an equilibrium that realizes the optimum of (7), and the natural candidate prices are the dual variables of (7). These need not exist with finite values in general: the objective pieces $F^{-1}_{b_j}(1-q/b_j)q$ and $F^{-1}_{s_i}(q/s_i)q$ can have infinite slope at the boundary, for instance for unbounded supports. The proof therefore needs the boundary-slope facts of Lemma EC.1(ii) and a "special" KKT system in derivative form. Proposition 1 needs its own convex program for the equilibrium and is the deepest milestone. In part (ii) the optimal flow of (7) is not unique, so necessity has to use the flow of the equilibrium, not a fixed optimal flow.

Formalization scope

Types are arbitrary finite types; flows are functions $\mathcal S\to\mathcal B\to\mathbb R$ whose values off $E$ are never read. The upper end $\bar v$ of each support is in WithTop ℝ, and $F^{-1}(u)=\inf\{v\ge0:F(v)\ge u\}$ is defined from $F$. The standing assumptions of pp. 7–8 (positive masses, $c\ge0$, degree at least one, each $F$ a continuous CDF extended to $\mathbb R$) are explicit hypotheses. Two conventions concern unbounded supports, where $F^{-1}(1)=\infty$. The feasible set of (7) requires $q^s_i<s_i$ when $\bar v_{s_i}=\infty$, since the paper's objective is $-\infty$ at $q^s_i=s_i$. For the same sellers, Assumption 2 is posed on $[0,1)$; on $[0,1]$ with a finite stand-in value it would be unsatisfiable. "Optimal solutions exist" is stated as attainment (IsGreatest). An optimal fee pair is one for which some equilibrium attains $V_{opt}$. Slopes $g'_j$, $h'_i$ are limits of derivatives from inside the interval (footnote 22). Proposition EC.1 is posed only at the instance (7); the general framework problem (EC.1) is not formalized.

Theorem 1(ii) is stated with an optimal flow of (7), because the printed version with the fixed $\bar x$ is false when optimal flows are not unique. The sentence "the optimal commission-subscription vector is not unique" is not posed. Ruled out as trivializing: defining the revenue of an equilibrium as $h(q^s,q^b)$ instead of (3a); reading "optimal solutions exist" as an unattained supremum; an equilibrium without the buyers' minimum in (2b) or the cheapest-seller restriction (2d); a feasible set of (7) that admits $q^s_i=s_i$ for unbounded sellers at a finite junk cost; and an Assumption 2 that no unbounded seller distribution satisfies.

A complete development needs basic facts on generalized inverses of continuous CDFs, existence and KKT theory for separable concave maximization over a flow polytope (not in Mathlib), and equilibrium existence for Proposition 1. The concave-programming layer is reusable beyond this mission. Proofs of individual milestones, and sanity checks such as uniform or exponential markets, are welcome. The paper's proofs are in its e-companion, which is part of the cited SSRN file (EC.1.1, pp. ec2–ec6; EC.2.1; EC.3.1, pp. ec38–ec44).

Selected references

• J. R. Birge, O. Candogan, H. Chen, D. Saban, Optimal Commissions and Subscriptions in Networked Markets, SSRN abstract 3259716, version of 2019-09-13 (cited version, with e-companion). https://ssrn.com/abstract=3259716
• Same, Manufacturing & Service Operations Management, published version. https://doi.org/10.1287/msom.2019.0853
• L. S. Shapley, M. Shubik, The assignment game I: The core, International Journal of Game Theory 1, 1971. https://doi.org/10.1007/BF01753437

Motivation

Portfolio selection uses observed asset returns to choose weights that balance expected return against variability. Estimates of both quantities can change sharply when the historical sample changes. A distributionally robust model addresses this uncertainty by allowing the return law to vary around the empirical law, then judging a portfolio by its worst variance and worst expected return. In the model of Blanchet, Chen, and Zhou, the allowed laws form a ball defined by an optimal transportation cost. Theorem 1 asks whether this optimization over probability laws can be expressed using only the sample and a norm of the portfolio weights.

The paper presents this equivalence as its first main contribution. Its later sections use statistical assumptions on a return time series to guide the choice of the ball radius and the return target. This mission concerns the finite-sample equivalence itself; those statistical choices are separate results. The distinction matters because the equivalence holds for a given nonnegative radius and target, without imposing a model for how the observations were generated. Theorem 1 and §3 of the preprint make these two roles explicit.

Setting

There are $d$ assets and $n\ge1$ observed return vectors $R_1,\ldots,R_n\in\mathbb R^d$. A portfolio is a vector $\varphi\in\mathbb R^d$ whose weights sum to one. Its return when the asset return vector is $x$ is $\varphi^Tx$. The empirical law is $P_n=n^{-1}\sum_{i=1}^n\delta_{R_i}$, so empirical expectations and variances use the population normalization $1/n$. No independence assumption is needed for this finite-sample problem.

Fix $1\le q<\infty$ and its Hölder conjugate $p$, so $1/p+1/q=1$. The endpoint $q=1$, $p=\infty$ is included. Moving a return vector $u$ to $w$ costs $c(u,w)=\|w-u\|_q^2$. For two probability laws $P,Q$, the transportation cost $D_c(P,Q)$ is the infimum of expected $c(U,W)$ over joint laws whose first marginal is $P$ and second marginal is $Q$. With radius $\delta\ge0$, the ambiguity set is

$$U_\delta(P_n)=\{P\text{ a probability law}:D_c(P,P_n)\le\delta\}.$$

For target return $\bar\alpha$, the feasible region $F_{\delta,\bar\alpha}(n)$ contains portfolios whose weights sum to one and whose expected return under every $P\in U_\delta(P_n)$ is at least $\bar\alpha$. This is the paper's worst-case mean condition. For any such portfolio, the robust objective is the supremum of $\operatorname{Var}_P(\varphi^TR)$ over the same ambiguity set. These objects are defined in §§1–2.2 of the preprint.

Formalization targets

Robust mean and mean-constrained second moment

Proposition 1 identifies the minimum expected return over the ball:

$$\min_{P\in U_\delta(P_n)}E_P(\varphi^TR) =E_{P_n}(\varphi^TR)-\sqrt\delta\,\|\varphi\|_p.$$

Proposition 3 evaluates the maximum second moment subject to a specified mean $\alpha$. Write $m=E_{P_n}(\varphi^TR)$, $N=\|\varphi\|_p$, and $v=\operatorname{Var}_{P_n}(\varphi^TR)$. When $(\alpha-m)^2\le\delta N^2$, its value is

$$h(\alpha,\varphi)=E_{P_n}[(\varphi^TR)^2]+2(\alpha-m)m+\delta N^2 +2\sqrt{\delta N^2-(\alpha-m)^2}\sqrt v.$$

The two displayed steps in the proof of Theorem 1 connect this constrained value to the unconstrained worst variance: $h(\alpha,\varphi)-\alpha^2=(\sqrt v+\sqrt{\delta N^2-(\alpha-m)^2})^2$, whose maximum over allowed $\alpha\ge\bar\alpha$ is $(\sqrt v+\sqrt\delta N)^2$ and is attained at $\alpha=m$. These milestones retain the paper's constants, feasibility range, and attainment claims. Propositions 1 and 3 and the proof of Theorem 1 give the source statements.

Equivalence of the portfolio problems

Theorem 1 is the goal. It says that the robust problem (2) and the empirical problem (9) have both the same optimal portfolios and the same optimal value:

$$\min_{\varphi\in F_{\delta,\bar\alpha}(n)} \sup_{P\in U_\delta(P_n)}\operatorname{Var}_P(\varphi^TR) =\min_{\varphi\in F_{\delta,\bar\alpha}(n)} \left(\sqrt{\operatorname{Var}_{P_n}(\varphi^TR)} +\sqrt\delta\,\|\varphi\|_p\right)^2.$$

The statement also equates the minimizer sets, rather than equating values alone. The paper calls (9) the dual problem; here that name denotes this regularized empirical optimization problem. Theorem 1, p. 6 is the pinned target.

Significance

The theorem replaces an optimization over probability laws with a finite-dimensional portfolio objective containing a norm penalty. It gives a precise interpretation of that penalty: its size and exponent follow from the Wasserstein radius and transport norm. It also preserves which portfolios are optimal, so the reformulation supports the portfolio decision itself, not only its reported objective value. The target-return constraint still depends on the worst expected return; Proposition 1 gives its explicit empirical form. These consequences are stated in §2.2 of the preprint.

A complete formalization would establish the finite-sample equivalence and the attained extrema that underlie it. It would also supply reusable results about finite empirical measures, transport balls with quadratic norm costs, and portfolio moments under those balls. The pinned results are proved in the paper; the work here is to give their statements and proofs in Lean under a shared, audited model. The current local proposal consists of statements with proof placeholders, not machine-checked proofs of those results.

Difficulty

The adversary changes the whole probability law, while the robust objective subtracts the square of the law's own mean from its second moment. Maximizing the second moment alone does not therefore give the worst variance. The mean constraint in Proposition 3 and the subsequent optimization over $\alpha$ are essential to recovering the centered objective. Attainment also matters: the paper states minima and maxima, whereas a bound on an infimum or supremum would be weaker. At the level of Lean definitions, every law in the quadratic transport ball must have sufficiently integrable portfolio returns for the real moment formulas to express the paper's quantities. These are the central obligations of §2.2 and Appendices A–C.

Formalization scope

Return vectors and weights are functions Fin d → ℝ; the sample is indexed by Fin n with $n\ge1$. Exponents are extended nonnegative reals to include $p=\infty$, while $q$ is finite as in the paper's fixed real exponent. The cost takes values in $[0,\infty]$, and the reused transport definition fixes both coupling marginals. The ambiguity set contains all probability laws within the cost radius, with no added moment restriction. The portfolio moments are real Bochner integrals. Showing that the quadratic-cost ball makes these integrals meaningful is part of proving the results.

The robust variance objective uses an extended-real supremum. This represents an empty or unbounded indexing set without the default value of a real supremum. The feasible mean constraint is written as a universal lower bound over the ball, matching the paper's minimum constraint. The goal compares both minimizer sets and infimum values on that feasible region. It cannot be discharged by defining the robust objective to equal the regularized formula, narrowing the ambiguity set, or assuming the desired moment and value identities. Proposition 1 and Proposition 3 retain attainment through IsLeast and IsGreatest.

This mission covers the finite-sample reformulation in §§1–2.2. The time-series assumptions A1–A3, the data-driven choices of $\delta$ and $\bar\alpha$ in §3, Theorem 2, and Proposition 4 are outside its scope. Contributions on transport-ball integrability, the two attained extrema, the scalar maximization, and the final equivalence would all support the goal. The general-cost dual formula of Proposition 2 is omitted because the printed formulation has a boundary counterexample at $\delta=0$; a faithful version needs a separate audit of its duality hypotheses.

Selected references

• José Blanchet, Lin Chen, and Xun Yu Zhou, Distributionally Robust Mean-Variance Portfolio Selection with Wasserstein Distances, arXiv:1802.04885v1, 2018 preprint; published in Management Science, 2022. Pinned preprint.

Motivation

A component supplier may ask two downstream manufacturers to license their improvements to each other. Sharing raises each product's quality, but it can also reduce a manufacturer's reason to invest in its own improvement. The supplier must choose the licensing rule before those investments and before setting the wholesale price. Wang, Huang, and Lee study this choice in a two-manufacturer supply chain with unequal innovation costs. Their 2023 manuscript identifies cost regions in which the supplier gains from committing to cross-licensing and a region in which the choice depends on a further threshold. The question matters whenever a shared component provider controls a contract that changes both downstream competition and the incentive to improve products.

This mission targets Proposition 4 of the authors' SSRN manuscript, version of 2023-04-27. The appendix of that manuscript contains the proof and the explicit equilibrium formulas used here. The manuscript was later published in Manufacturing & Service Operations Management; the theorem and page labels in this mission belong to the held SSRN version.

Setting

There is one supplier and two manufacturers, $M_1$ and $M_2$. Manufacturer $i$ invests at innovation level $T_i\ge0$ and pays the quadratic cost $k_iT_i^2$. Manufacturer 2 has the lower innovation cost: $49/144<k_2<k_1$. If the manufacturers cross-license with effectiveness $\beta\in[0,1]$, the quality improvements of their products are $T_1+\beta T_2$ and $T_2+\beta T_1$. Without cross-licensing the same model uses $\beta=0$. The market-size intercept is normalized to one and unit production costs to zero, as in Section 3 of the manuscript.

After investment, the supplier selects a nonnegative wholesale price $r$. The manufacturers then choose nonnegative Cournot quantities $q_1,q_2$. Manufacturer $i$'s selling price is $1+T_i+\beta T_j-q_i-q_j$, and its operating profit is $(1+T_i+\beta T_j-q_i-q_j-r)q_i$. The supplier receives $r(q_1+q_2)$. A downstream duopoly has both quantities positive; at a downstream monopoly, only one manufacturer produces. The paper solves this sequence backward and distinguishes two equilibrium investment patterns within the duopoly: an interior outcome $T^I$ and a boundary outcome $T^B$. Their dividing cost is $\hat k_2(k_1\mid\beta)$. The paper's named innovation outcome is $T^B$ for $k_2<\hat k_2(k_1\mid\beta)$ and $T^I$ otherwise.

Write $P(k_2,\beta)$ for the supplier's optimal wholesale revenue at that named innovation outcome. Thus $P(k_2,0)$ is the same downstream model with no licensing. The choice to commit to cross-licensing is determined by comparing these two revenues.

Formalization targets

The three cost regions

Proposition 4 divides admissible $k_2$ into three regions. In the boundary region, licensing weakly benefits the supplier:

$$k_2<\hat k_2(k_1\mid\beta)\quad\Longrightarrow\quad P(k_2,0)\le P(k_2,\beta).$$

The threshold $\hat k_2(k_1\mid\beta)$ decreases as $\beta$ rises, and this boundary region eventually has no admissible $k_2$. In the middle region there is a single threshold $\tilde k_2$, fixed by $k_1$ and $\beta$, below which the supplier weakly prefers licensing:

$$\hat k_2(k_1\mid\beta)\le k_2<\hat k_2(k_1\mid0):\qquad P(k_2,0)\le P(k_2,\beta)\ \Longleftrightarrow\ k_2\le\tilde k_2.$$

In the third region the direction of the threshold reverses. For a threshold $\underline k_2$ fixed by $k_1$ and $\beta$,

$$k_2\ge\hat k_2(k_1\mid0):\qquad P(k_2,0)\le P(k_2,\beta)\ \Longleftrightarrow\ \underline k_2\le k_2.$$

When $\beta\ge2/5$, $P(k_2,\beta)\le P(k_2,0)$ throughout that last region. All three displays are restricted to $49/144<k_2<k_1$. The full proposition is the mission goal. The milestone list records the paper's threshold monotonicity, the two explicit supplier-profit formulas, and the cost-region facts used to state the comparison.

Significance

The result makes the supplier's contract decision depend on both innovation asymmetry and the effectiveness of sharing. It separates the direct benefit of higher quality from the loss associated with weaker investment incentives. In particular, the supplier can benefit from cross-licensing when the superior manufacturer's cost is low enough for a boundary investment outcome, yet full effectiveness does not make licensing uniformly attractive. These conclusions are specific to the supplier's choice before investment; the paper's earlier ex post comparison holds the innovations fixed and addresses a different decision.

The mathematical result is already proved in the authors' appendix. The work here is to formalize its exact conditions and the optimization value being compared, then obtain a machine-checked proof. A development can reuse the Cournot quantity response, wholesale-price optimization, and piecewise investment formulas for the paper's later welfare and manufacturer-profit results. The local draft theorem statements compile in Lean; the results themselves remain open proof obligations.

Difficulty

The supplier's price can change which manufacturers remain active, and the manufacturers choose investments while anticipating that price response. A simple comparison of demand intercepts at fixed investments therefore does not decide the initial contract: the investments on the two sides of the comparison can differ, and a cost change can move one side across the boundary between the two equilibrium regimes. The paper expresses the outcomes with rational functions containing $\sqrt3$ and analyzes three regions separated by $\hat k_2(k_1\mid\beta)$ and $\hat k_2(k_1\mid0)$. A faithful formalization must also preserve the order of quantifiers: each single-crossing threshold is chosen once for fixed $k_1,\beta$, before $k_2$ ranges over its region.

Formalization scope

The Lean model uses real parameters and explicit pairs ordered as $M_1,M_2$. It encodes the paper's displayed quantity formula for $T_2\ge T_1$, with $q_i,T_i,r\ge0$ and $0\le\beta\le1$. Its standing cost condition is $49/144<k_2<k_1$. The wholesale-price domain $r\ge0$ makes explicit the economic domain implicit in the manuscript. The two displayed investment formulas use Real.sqrt 3; no decimal approximation enters a statement. The named innovation outcome follows page A.2: boundary below $\hat k_2$, interior otherwise. A separate mission targets its Nash-equilibrium characterization.

Most importantly, the supplier's optimal profit is the supremum of actual revenue over nonnegative prices at that innovation outcome. It is not defined to equal either closed form; a milestone asserts that the maximum is attained and identifies its value. This prevents the preference theorem from becoming a comparison true only by definition. The $\tilde k_2$ and $\underline k_2$ thresholds are existential single-crossing statements because the latter's printed formula on page A.3 is malformed. The proof's weak profit comparisons determine the formal inequality. At $\beta\ge2/5$, the statement uses interior profit on both sides, correcting an apparent $\pi_s^B(\beta)$ slip in the final sentence of the proof.

Useful contributions include a proof of the attained supplier optimum, denominator positivity over the standing domain, exact inequalities involving $\sqrt3$, and the two single-crossing results. The general price-optimization facts and market-response lemmas can be reused beyond this mission.

Selected references

• J. Wang, T. Huang, and J. Lee, Cross-licensing in a Supply Chain with Asymmetric Manufacturers, SSRN manuscript 3053682, version of 2023-04-27, Proposition 4 and Appendix A.1–A.3. SSRN.
• J. Wang, T. Huang, and J. Lee, Cross-licensing in a Supply Chain with Asymmetric Manufacturers, Manufacturing & Service Operations Management, 2023. DOI: 10.1287/msom.2019.0477.

Motivation

Digital platforms earn advertising revenue in proportion to the time users spend on them, and many of their design choices (infinite scroll, autoplay, notifications) raise engagement at the expense of the user's experience. Whether competition between platforms disciplines such addictive design or amplifies it is a question for competition policy and for the regulation of digital markets.

Ichihashi and Kim, Addictive Platforms (Bank of Canada Staff Working Paper 2022-16, 2022; Management Science, 2023) model platforms that compete for a consumer's attention by choosing how addictive to make their services. Without costs of addictiveness they find that competition hurts the consumer when attention is scarce and helps her when it is abundant (a separate mission formalizes that comparison). Section 5 of the paper asks what changes when raising addictiveness is costly, for instance because it requires investment in technology. Its answer, Proposition 5, is that the comparison then depends on the size of that cost rather than on the scarcity of attention: for high costs competition leads to more addictiveness and lower consumer welfare than joint-profit maximization would, whatever the attention cap.

Setting

There are $K \ge 2$ platforms and one consumer. Each platform $k$ chooses an addictiveness $d_k \ge 0$ and pays $\kappa\gamma(d_k)$, with $\kappa > 0$. The consumer observes $d = (d_1,\dots,d_K)$, joins a set $J$ of platforms and allocates attention $a_k \ge 0$ to each $k \in J$, subject to the attention cap $\sum_{k\in J} a_k \le \overline{A}$, where $\overline{A} \in \mathbb{R}_+\cup\{\infty\}$. Her payoff is $0$ if she joins nothing and otherwise

$$\sum_{k\in J} u(a_k, d_k) - C\Big(\sum_{k\in J} a_k\Big).$$

Platform $k$ earns the attention it receives, $a_k$ if $k \in J$ and $0$ otherwise, minus its cost $\kappa\gamma(d_k)$.

The utility has the form $u(a,d) = v(a-d)$: addictiveness lowers the utility of any given amount of attention but raises its marginal value. The primitives satisfy the paper's Assumptions 1–3: $u(\cdot,d)$ is strictly increasing and concave, $u(a,\cdot)$ strictly decreasing, and $u_1 = \partial u/\partial a$ strictly increasing in $d$; the attention cost $C$ is strictly increasing, convex and twice differentiable with $\lim_{a\to0}[u_1(a,0) - C'(a)] > 0$; the cost of addictiveness $\gamma$ is increasing, strictly convex and differentiable with $\gamma'(0^+) = 0$ and $\gamma'(\infty) = \infty$; and with $g$ the inverse of $v'$, the product $g'(C'(x))\,C''(x)$ is weakly decreasing.

Two outcomes are compared.

• The equilibrium is a pure-strategy subgame perfect equilibrium: platforms choose $d$ simultaneously, and the consumer then chooses $J$ and $a$ optimally at every profile, on and off the equilibrium path.
• The joint-profit maximizing outcome (Definition 1) is the outcome when the platforms choose $(d_1,\dots,d_K)$ jointly to maximize the sum of their profits, breaking ties in the consumer's favour, and the consumer only chooses between joining all platforms and joining none.

Consumer surplus $U^E$, respectively $U^J$, is the consumer's payoff at the equilibrium, respectively at the joint-profit maximizing outcome.

Formalization targets

Goal: Proposition 5

For every $\kappa > 0$ and $\overline{A} > 0$ the equilibrium is unique, with all platforms at the same positive addictiveness, and a joint-profit maximizing outcome exists. For every $\overline{A} > 0$, including $\overline{A} = \infty$, there is a $\kappa^* \ge 0$ such that for every $\kappa > 0$

$$\big[\,d^J_k \le d^E_k \ \text{for all } k \ \text{ and } \ U^E \le U^J\,\big] \iff \kappa \ge \kappa^*.$$

The threshold $\kappa^*$ may depend on the cap and the primitives but not on $\kappa$.

Milestones (Appendix D)

1. Lemma D.1. With $D = \sum_k d_k$, a consumer who has joined all $K$ platforms allocates $a_k = \frac1K[\min\{A(D),\overline{A}\} - D] + d_k$, where $A(\cdot)$ is concave and uniquely solves $A(D) - D = K\,g(C'(A(D)))$.
2. Lemma D.2. The unique equilibrium has every platform at $\min\{d^1(\kappa), d^2\}$, where $d^1(\kappa)$ is the fixed point (A.9) of a platform's marginal trade-off and $d^2$ the cost-free equilibrium addictiveness. $d^1(\kappa)$ decreases from $\infty$ to $0$, and the equilibrium is at $d^2$ exactly when $\kappa \le \kappa^E$.
3. Lemma D.3. The unique joint-profit maximizing outcome has every platform at $\min\{d^1_J, d^2_J\}$, where $d^1_J$ solves $\max_{d\ge0}[\min\{A(Kd),\overline{A}\} - K\kappa\gamma(d)]$ and $d^2_J$ makes the consumer's payoff from joining all platforms zero.
4. Lemma D.4. If the equilibrium addictiveness is $d^1(\kappa)$, then $U^E \le U^J$.

Significance

Proposition 5 separates two forces. When addictiveness is cheap, the consumer's participation constraint pins down the outcome under joint-profit maximization, and the platforms push her payoff to zero; competition then helps her because she can leave one platform. When addictiveness is expensive, each platform's marginal trade-off between attention and cost determines its choice, and competing platforms, which take attention from one another, choose more addictiveness than they would jointly. The result implies Corollary 1: for $\kappa \ge \kappa^*$ the platforms gain from a collective cap on addictiveness, which bears on the debate about industry self-regulation.

The result is proved in the paper; to our knowledge none of it has been formalized. A machine-checked proof would cover a game with a continuum of strategies for every player, a consumer best response defined at every profile, a fixed-point characterization of equilibrium, and a threshold argument in the cost parameter. Appendix D's proof is short and leaves steps to the reader, among them that $U^J(\kappa)$ is increasing in $\kappa$ and that each $d_k$, not only consumer surplus, is lower under joint-profit maximization. A formal proof has to supply these steps.

Difficulty

The obvious argument is to compute both outcomes from first-order conditions and compare. Three steps of that argument do not go through as written. First, the consumer's allocation (A.6) is derived from an unconstrained first-order condition and fails when a platform is so addictive that its formula gives negative attention, so a platform's payoff away from symmetric profiles is not given by the closed form (A.10). Ruling out profitable deviations into that region needs a separate argument. Second, uniqueness of the equilibrium is claimed among all profiles, not only symmetric ones. Third, the "if and only if" requires the set of costs where the joint-profit outcome is better to be an interval closed at its left end, which in turn needs monotonicity and continuity of both consumer payoffs in $\kappa$ across the switch between the participation regime and the marginal regime.

Formalization scope

Platforms are Fin K (the paper's platform 1 is index 0) and the cap is an extended nonnegative real ℝ≥0∞. Derivatives of $u$, $C$ and $\gamma$ on $\mathbb{R}_+$ are one-sided. The consumer strategy is a choice at every profile, and the equilibrium requires optimality at every nonnegative profile. Without that requirement any profile could be supported by a consumer who punishes deviations. The joint-profit outcome uses its own restricted consumer problem ("join all or none") and the consumer-favourable tie-break among profit-maximizing profiles. Without the tie-break, profiles below the participation level would also count as outcomes. No value function is written as a supremum: equilibrium objects are characterized through maximizers. "Lower", "higher" and "decreasing" are read weakly. The proof yields only weak inequalities on both sides of $\kappa^*$, and at $\kappa = \kappa^*$ the two outcomes can coincide.

The statement adds the following disclosed hypotheses to the paper's assumptions:

• $u(\cdot,d)$ is strictly concave (Assumption 1 says concave; the proofs use strictness);
• $C(0) = 0$;
• the consumer's uncapped problem has an optimum for every profile and every set of platforms (stated on p. 6 for $\overline{A} = \infty$);
• $g = (v')^{-1}$ is read as $g(v'(x)) = x$ and $v'(g(C'(x))) = C'(x)$ for $x \ge 0$, with $g$ differentiable at each $C'(x)$;
• a platform pays $\kappa\gamma(d_k)$ whether or not the consumer joins it;
• $K \ge 2$ and $\overline{A} > 0$; at $\overline{A} = 0$ no platform receives attention and the equilibrium addictiveness is $0$.

Lemma D.1 also carries an interiority hypothesis, that every coordinate of (A.6) is nonnegative, without which it is false. The goal also asserts that a joint-profit maximizing outcome exists, so that its comparison cannot hold vacuously. $\kappa$ ranges over $(0,\infty)$; the proof's use of $\kappa = 0$ as a cost-free benchmark is not part of any statement.

The hypotheses are satisfiable. A sanity check, not part of the mission, verifies all of them in Lean for every $K$ on the instance

$$v(x) = 1 - e^{-x},\quad C(a) = \frac{e^a - 1}{2},\quad \gamma(d) = d^2,\quad g(c) = -\log c.$$

A complete development needs Karush–Kuhn–Tucker conditions for a concave program over a simplex-like set, implicit differentiation for $A(\cdot)$, a monotone fixed-point argument for the best response, and continuity of maximizers in a parameter. These parts are reusable beyond this mission. Proofs of the milestones, partial results under the closed-form allocation, and checks of the statements on concrete instances are all welcome. The goal is Proposition 5. Propositions 1–4, 6 and 7, Corollary 1 and the side claims of Appendices E–F are not posed here.

Selected references

• S. Ichihashi and B.-C. Kim, Addictive Platforms, Bank of Canada Staff Working Paper 2022-16, April 2022. https://doi.org/10.34989/swp-2022-16
• S. Ichihashi and B.-C. Kim, Addictive Platforms, Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4392

Motivation

Digital services are paid for with attention: an ad-financed platform earns more the longer its users stay. Policy reports on digital markets (Crémer, de Montjoye and Schweitzer, 2019; the U.K. Digital Competition Expert Panel, 2019; Scott Morton et al., 2019) worry that such firms degrade their services with features that capture attention at the user's expense, and they usually recommend more competition. Ichihashi and Kim, Addictive Platforms (Bank of Canada Staff Working Paper 2022-16; Management Science, 2023), ask whether competition actually helps. Their answer depends on how scarce attention is. When attention is scarce, platforms compete by making their services more addictive rather than better, and a monopoly serves the consumer better than a duopoly. This mission formalizes that comparison, the paper's headline result, together with the two equilibrium characterizations it rests on.

Setting

There are $K$ platforms and a single consumer. Each platform $k$ chooses an addictiveness $d_k \ge 0$. The consumer observes $d = (d_1, \dots, d_K)$, joins a set $J$ of platforms and allocates attention $a_k \ge 0$ to each $k \in J$. She receives $0$ if $J = \emptyset$, and otherwise

$$\sum_{k\in J} u(a_k, d_k) - C\Big(\sum_{k\in J} a_k\Big),$$

subject to the attention cap $\sum_{k\in J} a_k \le \overline{A}$, where $\overline{A} \in \mathbb{R}_+ \cup \{\infty\}$. Platform $k$ earns the attention $a_k$ if the consumer joins it and $0$ otherwise.

The service utility $u(a, d)$ is twice differentiable, strictly increasing and concave in attention $a$, and strictly decreasing in $d$. The marginal utility $u_1(a, d) = \partial u/\partial a$ is strictly increasing in $d$, so a more addictive service is worse to join but harder to stop using. There is some $d$ at which no amount of attention makes the service worth joining, and $u(0,0) \ge 0$. The attention cost $C : \mathbb{R}_+ \to \mathbb{R}_+$ is strictly increasing, convex and twice differentiable, with $\lim_{a\to0}[u_1(a,0) - C'(a)] > 0$. These are Assumptions 1 and 2 of the paper.

Platforms choose addictiveness simultaneously, and then the consumer chooses $J$ and $a$. The solution concept is pure-strategy subgame perfect equilibrium: the consumer chooses optimally at every profile $d$, and no platform gains by changing its own $d_k$. A monopolist ($K = 1$) breaks ties in the consumer's favour. Consumer surplus is the consumer's payoff in the equilibrium outcome.

The monopoly benchmark uses three quantities. The first is $A(d) = \arg\max_{A\ge0} u(A,d) - C(A)$, the consumer's attention on one platform when there is no cap. The second is $d^A(\overline{A}) = \min\{d \in [0,\infty] : A(d) \ge \overline{A}\}$, the lowest addictiveness at which she exhausts her attention. The third is $d^P(\overline{A})$, the addictiveness at which her best capped payoff from one platform falls to zero. Under competition, $A_K(d) = \arg\max_{A\in[0,\overline{A}]} K\,u(A/K, d) - C(A)$ is the total attention she spends on $K$ platforms of common addictiveness $d$.

Formalization targets

Goal: Proposition 3 (monopoly versus duopoly)

Let $\overline{A}^M$ be the least cap from which on monopoly consumer surplus is zero. For every monopoly equilibrium with addictiveness $d^M$ and every duopoly equilibrium with $(d_1, d_2)$:

$$0 < \overline{A} \le A(0) \;\Longrightarrow\; d^M < d_1,\ d^M < d_2,\ CS^{\mathrm{duo}} < CS^{\mathrm{mono}},$$ $$\overline{A} \ge \overline{A}^M \;\Longrightarrow\; d_1 \le d^M,\ d_2 \le d^M,\ CS^{\mathrm{mono}} \le CS^{\mathrm{duo}}.$$

The proposition is silent about intermediate caps, and so is the goal.

Milestones

1. Proposition 1 (monopoly). The monopolist sets $\min\{d^A(\overline{A}), d^P(\overline{A})\}$, which is increasing in $\overline{A}$. The consumer's payoff rises on $[0, A(0)]$, falls on $[A(0), \overline{A}^M]$ and is zero from some $\overline{A}^M > A(0)$ on.
2. Lemmas B.1–B.4. These are comparative statics of the consumer's problem: the tangent intercept $u(x) - xu'(x)$ is increasing, the value of spreading attention over $y$ platforms is concave in $y$, and the incremental gain from one more platform falls with the addictiveness and the number of the platforms already joined.
3. Step 1 of the proof of Proposition 2. For $K \ge 2$ there is a unique $d^* > 0$ solving the indifference condition (3) between joining $K$ and $K - 1$ platforms.
4. Proposition 2 (competition). For $K \ge 2$, every platform chooses $d^*$ in the unique equilibrium.

Significance

Proposition 3 separates two effects of competition. Business stealing pushes duopolists to raise addictiveness, because a more addictive service captures a larger share of a fixed attention budget. Competition for participation restrains them, because a consumer can drop a platform and spend her time on its rival. When attention is scarce the first effect dominates and the consumer is strictly worse off under duopoly. When it is abundant the monopolist extracts the whole surplus and duopoly cannot be worse. The result is the basis of the paper's policy discussion: digital curfews and the comparison between the equilibrium and the joint-profit outcome (Propositions 4 and 6). Propositions 1 and 2 are used throughout the paper.

The paper proves these results on paper. No machine-checked proof exists. A formal proof would check several delicate points. One is the role of the monopolist's tie-break, without which every $d \in [0, d^P]$ is a monopoly equilibrium when attention is scarce. Another is that the uniqueness argument for the duopoly needs a consumer who best-responds off the equilibrium path. The appendix also asserts a few claims without argument or slightly too strongly, recorded below. Verifying them is part of the work.

Difficulty

The obvious argument for Proposition 3 compares equilibrium payoffs through the closed forms of Figure 3, and closed forms do not exist in general. Every object is defined by an optimization problem whose maximizer has no formula. The value functions are concave but need not be differentiable, so the envelope-theorem steps of Appendix B cannot be applied as written; they have to be replaced by monotone comparative statics or one-sided derivatives. Proposition 2's uniqueness is the hardest part. It rules out asymmetric equilibria by a deviation argument that controls which platforms the consumer joins after a small change in one platform's addictiveness (Lemma B.4). It also needs the consumer's whole strategy, not only her choice on the path.

Formalization scope

Platforms are Fin K; the paper's platform 1 is the index 0. Addictiveness and attention are real numbers restricted to $[0,\infty)$, and only the values of $u$ and $C$ there matter. The cap $\overline{A}$ is an extended nonnegative real (ℝ≥0∞), so $\overline{A} = \infty$ is a genuine case and "$\overline{A} \ge \overline{A}^M$" includes it. Derivatives on $[0,\infty)$ are one-sided at $0$.

The definition file states the paper's Assumptions 1–2 as printed and adds disclosed pins:

• $u(\cdot, d)$ is strictly concave. The page says "concave", but Lemma B.1 needs strict concavity and Lemma B.2 applies Lemma B.1 to $u(\cdot,d)$.
• $C(0) = 0$. Without it $d^P$ need not exist.
• The uncapped consumer problem has an optimal attention profile for every profile and every nonempty $J$. The page (p. 6) assumes this for $\overline{A} = \infty$, and $A(d)$ presupposes it.
• $\overline{A} > 0$ where the result needs it: Proposition 1's characterization, Step 1, Proposition 2 and the first half of Proposition 3. At $\overline{A} = 0$ every profile is an equilibrium.

"Increasing" and "decreasing" are weak unless the page says "strictly". The one exception is "higher addictiveness" in the first half of Proposition 3, which is stated strictly because the proof gives $d^M = 0 < d^*$.

Three statements differ from the printed text. Lemma B.2's "$V^*$ is strictly concave" is false on the paper's own Figure 3 instance and is stated as concavity. The strict clause of Lemma B.4 fails when $C$ is linear and is not posed. The derivative claims of Lemmas B.2–B.4 are stated as decreasing differences of value functions.

Several trivializing formalizations are excluded:

• An equilibrium requires the consumer to best-respond at every profile, not only at the equilibrium one.
• The tie-break is part of the monopoly equilibrium.
• Equilibria exist (Propositions 1 and 2 assert existence), and a sanity file checks the standing hypotheses on $u(a,d) = 1 - e^{-(a-d)}$, $C(a) = a/2$.
• No value function is a real supremum; maxima enter through maximizers.

Not posed: Proposition 4 and later results, and the side models of Remarks 2–3. A complete development needs maximizers of concave problems on intervals and simplices, monotone comparative statics (Topkis, Milgrom–Shannon), and envelope arguments for concave value functions. These pieces are reusable well beyond this paper, and contributions of them as separate lemmas are welcome.

Selected references

• S. Ichihashi and B.-C. Kim, Addictive Platforms, Bank of Canada Staff Working Paper 2022-16, 2022. https://doi.org/10.34989/swp-2022-16. Published in Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4392
• P. Milgrom and I. Segal, Envelope Theorems for Arbitrary Choice Sets, Econometrica 70(2), 583–601, 2002. https://doi.org/10.1111/1468-0262.00296
• P. Milgrom and C. Shannon, Monotone Comparative Statics, Econometrica 62(1), 157–180, 1994. https://doi.org/10.2307/2951479
• J. Crémer, Y.-A. de Montjoye and H. Schweitzer, Competition Policy for the Digital Era, report for the European Commission, 2019. https://doi.org/10.2763/407537

Motivation

Many service platforms set a price paid by customers and a wage paid to the providers who serve them. A platform may instead announce how much of each transaction's price it will pass to providers, then choose prices after both platforms have announced their shares. These are different games: a price change in the second game changes both customer demand and provider pay. Hu and Liu's study of precommitments in two-sided competition asks which timing gives platforms a more favorable equilibrium. This mission isolates their comparison between a commission precommitment and no commitment, Proposition 3(b) of the submitted manuscript. The authors' Online Appendix, included in that manuscript, contains the proofs.

The comparison is useful where a platform must choose a contract with providers before it can adjust customer prices. It is not enough to know that either side of the market is competitive: the answer changes as demand-side and supply-side competition intensities move relative to each other. The mission makes the claimed parameter regions precise and ties them to equilibria of the two games.

Setting

There are two platforms, indexed by $i=1,2$, with rival $j\ne i$. Platform $i$ posts a consumer price $p_i$ and a provider wage $w_i$. Fix a potential market size $\Omega>0$. The demand substitution factor $\gamma\in[0,1)$ measures how a rival's price raises demand for platform $i$. The supply substitution factor $\beta\in[0,1)$ measures how a rival's wage draws providers away. The paper uses the positive part $[x]^+=\max\{x,0\}$:

$$d_i(p)=[\Omega-p_i+\gamma p_j]^+,\qquad s_i(w)=[w_i-\beta w_j]^+.$$

The number of completed matches is $z_i=\min\{d_i(p),s_i(w)\}$. Profit is $\pi_i=(p_i-w_i)z_i$. Unmatched consumers or providers generate no revenue. Keeping the positive parts matters when a platform chooses a price or wage that leaves one side of the market empty.

In mode P, both platforms choose their prices and wages simultaneously, and each can change its own price and wage together while its rival's choices stay fixed. In mode C, each platform first commits to a pay-out ratio $\alpha_i\in(0,1)$. The provider then receives $w_i=\alpha_i p_i$ per match and the platform keeps $1-\alpha_i$ of its price. After observing both ratios, the platforms choose prices. Their profit in this second stage is

$$\pi_i(\alpha,p)=(1-\alpha_i)p_i\min\{d_i(p),s_i(\alpha p)\}.$$

A subgame-perfect equilibrium in mode C specifies a price equilibrium after every admissible pair of ratios and an initial pair of ratios that resists unilateral deviation when prices are chosen again. The mission compares symmetric commission equilibria to the positive-profit equilibrium of mode P. In the paper's platform preference ranking, $X\succeq Y$ means that mode $X$ gives each platform a weakly higher price and profit, and a weakly lower wage and matching quantity, than mode $Y$.

Formalization targets

No commitment and commission outcomes

Lemma 1 gives the simultaneous price-and-wage outcome. Writing $D=4-3\beta-3\gamma+2\beta\gamma$, its price, wage, matching quantity, and profit are

$$p_P^*=\frac{3-2\beta}{D}\Omega,\quad w_P^*=\frac{\Omega}{D},\quad z_P^*=\frac{1-\beta}{D}\Omega,\quad \pi_P^*=\frac{2(1-\beta)^2}{D^2}\Omega^2.$$

Lemma F.2 says that second-stage commission prices equate demand and supply. Lemma 4 characterizes the symmetric commission equilibrium by the radical $\alpha^*$ in equation (7), its price $p_C^*=\Omega/[1-\gamma+(1-\beta)\alpha^*]$, and its profit in equation (9). These are the three milestones. The radical is transcribed exactly in the Lean definition associated with equation (7).

Proposition 3(b)

The goal compares the two equilibrium outcomes using all four components of the platform preference ranking:

$$\gamma\geq\beta\ \Longrightarrow\ C\succeq P;\qquad \gamma\ll\beta\ \Longrightarrow\ C\succeq P;\qquad \gamma\leq\beta\text{ and sufficiently close to }\beta\ \Longrightarrow\ P\succeq C.$$

The two informal proximity phrases are expressed by the existence of positive thresholds, with the threshold allowed to depend on $\beta$. At $\gamma=\beta$, both rankings can hold because the outcomes coincide. The goal also asserts that the equilibria being compared exist for every admissible parameter pair.

Significance

The result identifies when committing to a provider share yields a platform outcome that is preferable to choosing price and wage together. Its four-way comparison is stronger than a profit-only ranking: the associated prices, wages, and match counts all move in specified directions. It makes clear that the relative competition intensities on the two sides determine whether the timing of the provider contract helps or hurts platforms. Without the comparison, the closed-form equilibrium results for modes P and C would not say which contract timing platforms prefer.

The result is proved in the cited manuscript, with derivations in Online Appendix §F; it is not an open mathematical conjecture. The remaining work in this mission is a machine-checked Lean proof of the equilibrium statements and the parameter-region comparison. The development will also provide a reusable formal model of simultaneous and two-stage decisions in a two-sided market. No existing machine-checked proof of this particular comparison is identified in the local Prove2Me index.

Difficulty

A change in a commission ratio changes the wage at any given price, while the subsequent price decision changes both demand and the wage again. That coupling makes the comparison more delicate than ordering two prices by inspection. The commission equilibrium ratio contains a square root, and the ranking must establish the directions of four outcome quantities in several parameter regions. The apparent shortcut of comparing profits alone would leave three of Definition 1's required inequalities unresolved. The positive-part demand and supply functions also admit zero-match equilibria that complicate an unqualified uniqueness statement.

Formalization scope

The Lean development uses real-valued prices and wages, two platforms indexed by Fin 2, and all unilateral deviations in the stated strategy sets. Market size is positive, both substitution factors lie in $[0,1)$, and pay-out ratios lie in $(0,1)$. The paper does not spell out the strategy sets; these choices preserve the derivations in §3 and Appendix §F. The no-commitment uniqueness statement is restricted to equilibria where both platforms profit, because the literal unrestricted claim has zero-profit counterexamples. A second-stage strategy in mode C selects an equilibrium with positive profits for both platforms whenever one exists. This condition prevents off-path zero-profit punishments from making the printed symmetric SPE claim false.

The goal quantifies over equilibria derived from the demand, supply, match, and profit functions. It does not define an outcome to equal the paper's closed form, and it asserts equilibrium existence so that its universal comparisons have content. The radical for $\alpha^*$ is a named expression; Lemma 4, rather than its definition, establishes its equilibrium role. A full proof needs reasoning about unilateral deviations, positive-part functions, equilibrium existence and uniqueness, the radical expression, and real inequalities. The general Nash condition and the paper's market primitives are intended for reuse in other two-player platform games. Contributions addressing these foundations and any of the three cited milestones are within scope. Wage- and price-precommitment modes are outside this mission.

Selected references

• Ming Hu and Yan Liu, Precommitments in Two-Sided Market Competition, submitted manuscript with Online Appendix associated with the 2023 publication, SSRN 3734828. Manuscript.
• Ming Hu and Yan Liu, Precommitments in Two-Sided Market Competition, Manufacturing & Service Operations Management 25(2), 704–718, 2023. DOI.

Why compare subsidy formats?

Governments sometimes pay crop producers to increase supply. A payment for each unit planted and a payment for each unit harvested create different incentives when farmers have different yields. An agency choosing among those formats needs to know how much it must spend to attain the same total output. Fan, Feng, Li, Shanthikumar, and Wu study that question in an agricultural Cournot market and compare four programs: planting-only, harvesting-only, combined, and selective subsidies. Their Proposition 10 orders the minimum budgets required by those programs, with the order of the two single subsidies changing at a specified output threshold. The source for this mission is the 2023-03-18 SSRN version of their paper; the proof is in Online Appendix A.

The comparison matters because the payment format changes both who receives money and how much each farmer produces. The government seeks a target output, while each farmer chooses output in response to the market price and the payment offered. A budget comparison therefore has to account for the farmers' equilibrium response, rather than compare payment rates alone. The paper's Section 5 and Proposition 10 give the target and the resulting ordering.

Market and government programs

There are $N>0$ farmers. Farmer $j$ plants $x_j=z_jq_j$ units of input to harvest $q_j$ units of output, so $z_j$ is an input-to-output ratio. The farmers are indexed in nondecreasing order of $z_j$. Planting costs $c_P$ per input unit and harvesting costs $c_H$ per output unit. If total output is $Q=\sum_jq_j$, the market-clearing price is $p(Q)=\alpha-\beta Q$, with $\alpha,\beta>0$. An output profile is a Cournot equilibrium when every $q_j$ is nonnegative and no farmer can earn more by changing its own output while the other outputs stay fixed. These are the objects in the paper's Section 3 and equation (1).

A subsidy profile gives farmer $j$ a payment $t_j$ for each unit of output. Under a combined subsidy $(s_P,s_H)$, $t_j=z_js_P+s_H$: the planting part pays for $z_jq_j$ units of input and the harvesting part pays for $q_j$ units of output. Under a selective subsidy, the farmer chooses one payment, so $t_j=\max(z_js_P,s_H)$. Planting-only sets $s_H=0$; harvesting-only sets $s_P=0$. The model allows negative subsidy rates, which are taxes. When the two selective payments tie, either choice pays the same amount. These formats come from Sections 3, 4.1, and 4.2.

The government budget at equilibrium is $\sum_jt_jq_j$. A profile is feasible when every farmer produces a positive quantity and $\sum_jq_j\ge\bar Q$, where $\bar Q$ is the target output. For each program, its optimum is the infimum of its feasible budgets. This matches the paper's requirement that output reach at least the target, and the all-active regime used for the comparisons. The average ratio and its variability are $\bar z=N^{-1}\sum_jz_j$ and $v_z=N^{-1}\sum_jz_j^2-\bar z^2$. The paper introduces these statistics in Section 3.

Formalization targets

Write $B_C,B_S,B_P,B_H$ for the least feasible budgets under the combined, selective, planting-only, and harvesting-only programs. The goal is Proposition 10:

$$\bar Q\le Q^C(c_P,0)\quad\Longrightarrow\quad B_C\le B_S\le B_P\le B_H,$$ $$\bar Q>Q^C(c_P,0)\quad\Longrightarrow\quad B_C\le B_S\le B_H\le B_P.$$

Here $Q^C(c_P,0)$ is the all-active expression for market output under a combined subsidy with planting rate $c_P$ and harvesting rate zero, as given by equation (5). In addition, $v_z=0$ implies $B_C=B_S=B_P=B_H$. The target exceeds the no-subsidy output, as required at the start of Section 5. All farmers are assumed to produce at the three closed-form designs of Proposition 8.

The milestones record the market quantities in Proposition 3, equations (2)–(6), the three minimizing designs of Proposition 8, and the single-subsidy budget difference in the proof of Proposition 10, Online Appendix A, page 13. A separate theorem item states the selective optimum's lower bound from the same proof.

What the result establishes

The ordering identifies a minimum-spending format for any target in the stated all-active regime. The combined program never requires a higher optimal budget than the other three, and the selective program never requires a higher optimal budget than either single subsidy. The threshold tells the government which single subsidy is cheaper. When farmer input-to-output ratios have zero variability, the choice among all four formats has no budget effect. These conclusions are the specific content of Proposition 10, rather than a claim about all policy objectives or about equilibria with inactive farmers.

The mathematical result is proved in the paper. This mission asks for a machine-checked proof of its stated all-active comparison. It also creates reusable Lean definitions for a finite Cournot equilibrium with affine inverse demand, per-farmer subsidy payments, and budget optimization over equilibrium-feasible profiles. The formalization has not yet proved the goal or milestones; each theorem is offered as a statement for solvers. The paper's proofs are in Online Appendix A of the SSRN version.

Where the formalization is difficult

The government controls subsidy rates, but feasibility and spending are determined after farmers respond. The four programs therefore have different sets of possible payment vectors, and the output constraint may be met by several profiles. Comparing one chosen profile from each program does not by itself establish a comparison of their minima. The selective program adds another difficulty: farmers can receive different types of payments within the same equilibrium. The proof of Proposition 10 records a separate budget inequality for that program.

Formalization scope

Farmers are represented by Fin N, with Lean index $0$ corresponding to the paper's farmer $1$. A generic Cournot game is a separate definition; the agricultural market supplies its unit costs. Equilibrium is a best-response predicate over nonnegative real outputs. Subsidies are per-output payment vectors, and the government budget is the finite sum of payment times output. The combined program contains all pairs $(s_P,s_H)$; its definition does not fix the optimal planting rate $c_P/2$. The output constraint is $Q\ge\bar Q$, exactly as printed in Section 5. Subsidy rates and costs have no added sign restrictions.

The formalization explicitly assumes $N>0$, $\alpha>0$, $\beta>0$, nondecreasing $z_j$, and $z_j>0$. The last condition states the physical meaning of an input-to-output ratio and is a disclosed addition. For Proposition 10, $\bar Q$ is strictly above the no-subsidy output in the all-active regime, and the planting-only, harvesting-only, and combined designs of Proposition 8 each have an all-positive equilibrium. Every feasible budget set is restricted to all-active equilibria. This is the fixed-active-set reading of the paper's phrase “all farmers produce”; a variable-active-set version is outside this mission. The three design assumptions make the single-subsidy and combined feasible sets nonempty, and a single-subsidy profile also belongs to the selective program. The separate selective lower-bound theorem assumes that the paper's chosen optimal selective budget is attained. These conditions and the budget lower bounds ensure that real sInf represents a finite budget value.

The equilibrium formulas, optimality statements, and budget inequalities are proof obligations; none is built into the definitions. Contributions establishing those claims or reusable finite-game and finite-sum facts are in scope. Results on inactive farmers, random yields, or convex production costs are outside this mission.

Selected references

• Fan, T., Q. Feng, Y. Li, J. G. Shanthikumar, and Y. Wu, Output-Oriented Agricultural Subsidy Design, forthcoming in Management Science, SSRN version dated March 18, 2023, SSRN 4378693, DOI 10.1287/mnsc.2023.4749.

Motivation

A service platform makes decisions on two sides of a market. It charges consumers a price and pays independent providers a wage, then earns a margin only when it can match a consumer with a provider. Capacity is another decision available to the platform: it can limit how many matches it will carry, for example by limiting the active provider pool. Hu and Liu ask whether committing to this limit before setting price and wage changes the competitive outcome. Their submitted manuscript models this question for two competing platforms and states a two-sided counterpart of the quantity-precommitment result associated with Kreps and Scheinkman. The point matters for platform operations because a capacity decision can determine the price, wage, volume, and profit that emerge after both platforms react. Hu and Liu, submitted manuscript, §3.5.

Setting

There are two platforms, indexed by $i\in\{1,2\}$; $j$ denotes the other platform. The potential market size is $\Omega>0$. Each platform posts a consumer price $p_i\in\mathbb R$ and a provider wage $w_i\in\mathbb R$. Demand and supply are the positive parts

$$d_i(p)=[\Omega-p_i+\gamma p_j]^+, \qquad s_i(w)=[w_i-\beta w_j]^+,$$

where $[x]^+=\max\{x,0\}$. The demand substitution factor $\gamma$ and the supply substitution factor $\beta$ both lie in $[0,1)$. Higher rival prices raise a platform's demand; higher rival wages reduce its supply. A platform can serve only the smaller of its demand and supply. Its profit without a capacity limit is the margin $p_i-w_i$ times that number of matches. These are the manuscript's displays (1)–(3). Hu and Liu, submitted manuscript, pp. 8–9.

The first game is quantity competition. Each platform chooses a nonnegative matching quantity $z_i$. The prices and wages that clear demand and supply at those quantities are

$$p_i(z)=\frac{(1+\gamma)\Omega-z_i-\gamma z_j}{1-\gamma^2}, \qquad w_i(z)=\frac{z_i+\beta z_j}{1-\beta^2}.$$

A platform earns $(p_i(z)-w_i(z))z_i$. A quantity Nash equilibrium is a nonnegative vector $z$ at which neither platform can gain by choosing any other nonnegative quantity while the rival quantity stays fixed. The inverse price and wage appear in the proof of Lemma 6, where the profit function is written as (F.3). Hu and Liu, submitted manuscript, p. 14 and Online Appendix p. 32.

The second game is capacity precommitment. In stage one, each platform chooses a nonnegative capacity $q_i$, the most matches it can make. In stage two, both platforms simultaneously choose prices and wages. Platform $i$ then serves $m_i=\min\{d_i(p),s_i(w),q_i\}$ matches and earns $(p_i-w_i)m_i$. A second-stage Nash equilibrium lets a platform change its price and wage together. A subgame-perfect equilibrium specifies stage-two play after every admissible capacity vector and requires that no platform benefit from changing its stage-one capacity and then following the continuation for the changed vector. Hu and Liu, submitted manuscript, pp. 14–15 and Online Appendix §A.

Formalization targets

The goal is Proposition 1: capacity precommitment and quantity competition have the same equilibrium price, wage, matching quantity, and profit for each platform. Writing $q,\sigma$ for a capacity profile and its continuation plan, and $z$ for a quantity equilibrium, the target is

$$\forall i\in\{1,2\},\qquad \bigl(p_i(\sigma(q)),w_i(\sigma(q)),m_i(q,\sigma(q)),\pi_i(q,\sigma(q))\bigr) = \bigl(p_i(z),w_i(z),z_i,(p_i(z)-w_i(z))z_i\bigr).$$

The goal also asserts that an equilibrium of each game exists, so this comparison has actual outcomes to compare. Lemma 6 gives the unique quantity equilibrium and its closed forms. The subgame analysis in Online Appendix §A.1 gives a platform's best response to fixed rival price and wage. Lemma 7 states that demand and supply both equal committed capacity in the two-stage equilibrium. These three statements are the mission's milestones. Hu and Liu, submitted manuscript, pp. 14–15 and Online Appendix p. 1.

Significance

Proposition 1 supplies an operational interpretation of quantity competition in a market where each platform controls both consumer price and provider wage. A quantity outcome can arise through an earlier capacity choice followed by ordinary spot-market price and wage decisions. The conclusion covers four separate outcomes for each firm, so it supports comparisons of capacity policies in terms of what consumers pay, what providers receive, how many matches occur, and platform profit. The result is proved in the manuscript; its proofs are in Online Appendix §F of the same cited artifact. Hu and Liu, submitted manuscript, p. 15 and Online Appendix p. 33.

The formalization asks for machine-checked proofs of these known statements under explicit equilibrium conventions. It also creates reusable definitions for a two-sided market with positive-part demand and supply, a quantity game, and a two-stage capacity game. The paper's displayed formulas become auditable statements about every equilibrium of those games rather than numbers inserted into the definition of an outcome. No machine-checked proof of this specific proposition is asserted here.

Difficulty

The central issue is the full two-stage game. A stage-two platform changes price and wage jointly, and a stage-one capacity deviation leads to a new stage-two equilibrium. Checking a price deviation while holding wages fixed, or checking only capacities near a proposed equilibrium, does not establish the proposition. The positive parts in demand and supply also create zero-profit price-and-wage equilibria. Such equilibria can be used as off-path continuations and can change the set of stage-one equilibria. The formal target therefore selects positive profit for each platform whenever a subgame equilibrium permits it. The manuscript's Appendix §A distinguishes several regions of capacity profiles; this regime structure is part of the difficulty of proving a statement about all deviations. Hu and Liu, submitted manuscript, Online Appendix §§A.1–A.2.

Formalization scope

Lean uses Fin 2 for platforms and a named rival map. Prices and wages are real-valued. Capacities and chosen quantities are nonnegative reals. The standing parameters are $\Omega>0$ and $0\le\beta,\gamma<1$; these ranges keep the market-clearing denominators $1-\beta^2$ and $1-\gamma^2$ nonzero. Demand and supply retain the manuscript's positive-part operation even when it is inactive at a positive equilibrium.

A continuation plan maps every capacity profile to a pair of price and wage profiles. At every nonnegative capacity profile it must choose a second-stage Nash equilibrium. For each platform, if that subgame has an equilibrium in which it earns positive profit, the chosen equilibrium must give it positive profit. This includes a subgame in which its rival committed zero capacity. This selection is an explicit addition to the printed equilibrium language, needed because the unqualified statement admits zero-profit off-path punishments. The stage-one Nash condition evaluates a capacity deviation using the continuation plan at the deviated capacity. The manuscript does not specify strategy sets; the stated real and nonnegative domains make them explicit. The goal ranges over equilibria rather than defining outcomes from Lemma 6's closed forms, and it asserts existence to prevent a vacuous comparison.

Contributions can establish the market-clearing identities, the quantity equilibrium and its uniqueness, joint price-and-wage best responses, the capacity-binding result, and the existence and outcome claims of Proposition 1. The generic two-player Nash predicate and the positive-part market model are reusable beyond this mission.

Selected references

• Ming Hu and Yan Liu, Precommitments in Two-Sided Market Competition, submitted manuscript (SSRN 3734828; TSpace), published in Manufacturing & Service Operations Management 25(2), 2023, DOI 10.1287/msom.2022.1173. Mission statements follow the submitted manuscript and its Online Appendix, not the journal pagination.

Motivation

In reward-based crowdfunding, a seller asks customers to pay before the product's quality is known to them. A high-quality seller can try to communicate private quality through the prices he posts. That signal is costly because a price that deters imitation may also reduce the seller's own expected revenue. Bolandifar, Chen, Kouvelis and Zhou study this tradeoff when a campaign must meet a financing target and a successful campaign leads to a later retail period (SSRN manuscript, §§3–5). Their model asks whether a high-quality seller can separate himself from a low-quality seller by committing in advance to both the crowdfunding price and the later retail price.

The manuscript treats price commitment separately from the case in which the seller chooses the retail price after the campaign. This mission concerns the commitment case, specifically Proposition 2 and the lemmas that support it. The theorem describes a separating equilibrium after applying the intuitive criterion: the high-quality seller chooses a lower crowdfunding price and a higher retail price than he would under full information. The cited artifact is the authors' SSRN manuscript dated 2022-05-30; its proofs are in Appendix A (manuscript, pp. 38–43).

Setting

There are two privately known product qualities, $0<q_L<q_H$. A seller commits to a price pair $x=(P_1,P_2)$, where $P_1$ is paid by crowdfunding backers and $P_2$ is charged in the regular selling period. The project needs a financing target $T>0$, so a feasible pair satisfies $P_1\ge T$ and $P_2>0$. Both period market sizes are normalized to one; production and salvage costs are zero, and future revenue is not discounted (manuscript, pp. 9–13).

All funding customers have the same taste $\theta_c$, uniformly distributed on $[0,1]$ and unknown to the seller. They believe quality is $q_j$ and back the campaign when $\theta_c q_j\ge P_1$. Thus success has probability $\max\{0,1-P_1/q_j\}$. After a successful campaign, true quality $q_i$ becomes known. A fraction $\alpha\in(0,1)$ of regular customers have the same taste as the funding customers; success updates their conditional taste distribution. The remaining fraction has independent uniform tastes. A customer in the regular period buys if taste times $q_i$ is at least $P_2$ (manuscript, pp. 10–11).

Write $\Pi^{ij}(P_1,P_2)$ for the seller's expected total profit when true quality is $q_i$ and customers believe $q_j$. The expressions $V^{ij}$ and $W^{ij}$ distinguish the regions in which returning customers buy for sure or with a conditional probability. Write $\Pi^{ij*}$ for the maximum of $\Pi^{ij}$ over feasible pairs. In particular, $\Pi^{L*}=\Pi^{LL*}$ is the low type's full-information payoff. These are outcomes of optimization, not inserted formulas (manuscript, pp. 22–24, (7)–(11)).

In a separating equilibrium, the two seller types choose different feasible pairs $x_H$ and $x_L$. Funding customers believe the product is high quality exactly at $x_H$ and low quality at every other pair, including off-path pairs. Neither seller type can gain by deviating under those beliefs. The intuitive criterion then checks whether an off-path pair would be profitable to the high type if believed high while being unattractive to the low type (manuscript, pp. 13, 19).

Formalization targets

Lemma 4 identifies an attained full-information optimum for any choice of true and believed quality in $\{q_L,q_H\}$. Its crowdfunding price is

$$P_1^{ij*}=\max\left\{\frac{4q_j-(1-\alpha)q_i}{8},T\right\},$$

and its retail price follows the three cases of equation (11), depending on whether $T$ lies below $q_j/2$, between that threshold and $q_j/[2(1-\alpha)]$, or above the second threshold (manuscript, p. 23, Lemma 4).

The goal is Proposition 2 in the small-quality-gap regime $q_L<q_H\le(\alpha^2+6\alpha+25)q_L/16$. Define $(\dot P_1,\dot P_2)$ by its equations, requiring $\dot P_2>q_H/2$:

$$4\dot P_1+(1-\alpha)\dot P_2=2q_H,\qquad W^{LH}(\dot P_1,\dot P_2)=\Pi^{L*}.$$

When $T\le\dot P_1$, the goal states that the unique separating equilibrium surviving the intuitive criterion has $x_H=(\dot P_1,\dot P_2)$ and the low type at his full-information optimum. Relative to every full-information optimum $(P^H_{1f},P^H_{2f})$ of the high type, it also states

$$\dot P_1<P^H_{1f},\qquad \dot P_2>P^H_{2f}.$$

The mission separately targets uniqueness of the dotted pair, the first claim of Lemma 6 concerning profitable imitation of the high type's full-information pair, and the constrained optimum in equations (A.13)–(A.14) (manuscript, pp. 26–27, 41).

Significance

The result identifies how a commitment to the later price changes the signal available during crowdfunding. The high type's retail price is raised while his crowdfunding price is lowered, so the signal is encoded in the pair, rather than in a single crowdfunding price. The theorem also determines which separating outcome survives a refinement intended to remove equilibria supported only by arbitrary off-path beliefs (manuscript, pp. 26–27).

The mathematical result is already proved in the manuscript. The remaining formalization work is to give the economic model an exact Lean meaning, prove the optimization and equilibrium assertions, and make the boundary conventions explicit. The five open Lean theorems in this proposal are statements to be proved; their sorry bodies are not machine-checked proofs.

Difficulty

The seller's payoff changes expression when the regular price crosses a threshold determined by the funding price and the two qualities. The low type can mimic a pair whose regular price exceeds $q_L$, in which case regular sales vanish but the crowdfunding payoff can still rise. This makes a direct comparison of the printed $W^{LH}$ expression with the actual mimicking payoff invalid outside its demand region. The intuitive criterion adds a second layer: it tests deviations under a different belief from the default off-path belief. These regime changes and belief-dependent deviations are the central obstacles to a concise, faithful Lean statement (manuscript, pp. 23, 26–27, 41–43).

Formalization scope

Lean represents qualities, prices, probabilities and payoffs as real numbers. Its parameter structure contains $q_L,q_H,\alpha,T$, with $0<q_L<q_H$, $0<\alpha<1$ and $T>0$. The prior high-quality belief is omitted because the separating statements use beliefs fixed by the observed pair. Market sizes, zero costs, salvage value and discount rate are incorporated into the payoff. The funding success probability and purchase probabilities are clipped at zero outside their printed domains. The printed $V^{ij}$ and $W^{ij}$ remain available for the page 41 equations; $W^{ij}$ is only used away from its zero denominator. Suprema range over all feasible pairs $P_1\ge T$, $P_2>0$, and “optimal” means the displayed pair attains that supremum.

The manuscript's Proposition 2 needs the additional bound $T\le(3+\alpha)q_L/8$. Without it, the low type's constrained full-information payoff can be too small and he can profitably mimic a dotted pair with $\dot P_2>q_L$; a numerical counterexample and the discrepancy are recorded in the local moderation notes. This proposal states that bound openly rather than treating the printed proposition as valid for all $T\le\dot P_1$. Lemma 4 also records its displayed domain $T\le q_j$. The goal does not define the optimum by a formula, the equilibrium by the paper's necessary conditions (13)–(14), or the dotted pair by an arbitrary choice.

The foundational setting is a reusable two-type, two-price payoff and equilibrium model. A complete development must establish the payoff's agreement with the manuscript's regions, attainment and comparison of the full-information optima, uniqueness of the dotted pair, optimization on the relevant iso-profit curve, and the no-deviation and intuitive-criterion conclusions. Contributions proving these targets or reusable real optimization lemmas are within scope.

Selected references

• E. Bolandifar, Z. Chen, P. Kouvelis and W. Zhou, Quality Signaling through Crowdfunding Pricing, SSRN manuscript 3689946, 2022-05-30, SSRN. Published as Manufacturing & Service Operations Management, doi:10.1287/msom.2022.1177.