All missions

Motivation

Decision theory under uncertainty distinguishes risk, where probabilities are known, from ambiguity, where they are not. Ellsberg's (1961) urn experiments showed that people's choices between bets on the same kind of event depend on where the uncertainty comes from: a bet on a known urn is preferred to the matching bet on an unknown urn. Tversky and Fox (1995) found that basketball fans prefer bets on basketball games to bets with matched objective chances. Models of ambiguity therefore have to let attitudes depend on the source of uncertainty.

Baillon, Bleichrodt, Li and Wakker (Source Theory: A Tractable and Positive Ambiguity Theory, Management Science 71(10), 2025) take sources to be algebras of events and propose source theory: within each source the agent behaves as if events carry probabilities, transformed by a source-dependent weighting function, while different sources may be weighted differently. The behavior within one source is probabilistic sophistication in the sense of Machina and Schmeidler (1992), restricted to that source. This mission formalizes the paper's first main result, Theorem 1: a characterization of when a single source admits such a probability, entirely in terms of two ambiguity attitudes that are measured in experiments.

Setting

A state space $S$ carries an algebra $\mathcal E$ of events, and $\Gamma$ is a set of outcomes. An act is a finite-valued map $x : S \to \Gamma$ whose level sets are events; it is from an algebra $\mathcal A$ if its level sets lie in $\mathcal A$. The binary act $\gamma E \beta$ pays $\gamma$ on $E$ and $\beta$ on $E^c$. The agent has a preference $\succcurlyeq$ on acts.

Structural Assumption 1 (p. 8771) requires that $\succcurlyeq$ is a weak order represented on binary acts by biseparable utility: there are a utility $U : \Gamma \to \mathbb R$ and a weighting function $W$ on events ($W(\emptyset)=0$, $W(S)=1$, monotone) such that for $\gamma \succcurlyeq \beta$ the act $\gamma E\beta$ is valued $W(E)U(\gamma)+(1-W(E))U(\beta)$. It further requires three nonindifferent outcomes, convex rangedness of $W$ (between two nested events every intermediate weight is attained by a nested event), strong monotonicity, cumulative dominance and the Archimedean axiom. Events are ranked by $W$: $A \succcurlyeq B$ means $W(A) \ge W(B)$.

A source $\mathcal S$ is a subalgebra of $\mathcal E$ on which $W$ is convex ranged. It is uniform (source theory holds for it, Definition 1) if there is a finitely additive probability measure $P$ on $\mathcal S$ such that for all acts $x, y$ from $\mathcal S$

$$\bigl[\forall \alpha\in\Gamma:\ P(x\succcurlyeq\alpha)\ge P(y\succcurlyeq\alpha)\bigr]\ \Longrightarrow\ x\succcurlyeq y. \tag{2}$$

Two attitudes compare sources $\mathcal A$ and $\mathcal C$. $\mathcal C$ is preferred to $\mathcal A$ (Definition 2) if for all $A_1\in\mathcal A$, $C_1\in\mathcal C$,

$$W(A_1)=W(C_1)\ \Longrightarrow\ W(A_1^c)\le W(C_1^c). \tag{6}$$

$\mathcal A$ is more insensitive than $\mathcal C$ with insensitivity region $[B,D]$ (Definition 4) if for all ordered threefold partitions $(C_1,C_2,C_3)$ of $S$ from $\mathcal C$ and $(A_1,A_2,A_3)$ from $\mathcal A$,

$$W(A_1)=W(C_1)\ \&\ W(A_3^c)=W(C_3^c)\le W(D)\ \Rightarrow\ W(A_2)\ge W(C_2), \tag{8}$$ $$W(B)\le W(A_1)=W(C_1)\ \&\ W(A_3^c)=W(C_3^c)\ \Rightarrow\ W(A_2^c)\le W(C_2^c). \tag{9}$$

The region is regular for $\mathcal S$ if every fourfold partition $(E_1,\dots,E_4)$ of $S$ from $\mathcal S$ has a cell with $E_j \succcurlyeq B$ and $E_j^c \preccurlyeq D$.

Formalization targets

Goal: Theorem 1 (p. 8774)

For a source $\mathcal S$ under Assumption 1,

$$\mathcal S \text{ is uniform}\iff \mathcal S \text{ is preferred to itself, and } \exists\, B,D\in\mathcal E:\ [B,D] \text{ regular for } \mathcal S,\ \mathcal S \text{ more insensitive than itself w.r.t. } [B,D].$$

Milestones (in proof order)

1. Necessity (App. B, p. 8779): a uniform source is preferred to itself and more insensitive than itself with the maximal region $[\emptyset, S]$.
2. Lemma A.1 (p. 8779): (6) is equivalent to its weak-premise form (7), $W(A_1)\ge W(C_1)\Rightarrow W(A_1^c)\le W(C_1^c)$.
3. Lemma A.2 (p. 8779): (8) and (9) are equivalent to their weak-premise forms (A.1) and (A.2).
4. (B.1) (p. 8780): in a source preferred to itself, $A\succcurlyeq C \iff A^c\preccurlyeq C^c$.
5. Lemma B.1 (p. 8780): under statement (ii), for $E\cap H=F\cap H=\emptyset$ in $\mathcal S$, $E\succcurlyeq F\iff E\cup H\succcurlyeq F\cup H$.
6. The representing probability (p. 8780): under statement (ii), a unique probability measure on $\mathcal S$ represents event preference on $\mathcal S$.
7. The aside (p. 8780): a representing probability $P$ gives $W = w\circ P$ on $\mathcal S$ for a continuous, strictly increasing $w$ with $w(0)=0$, $w(1)=1$.
8. Uniqueness (p. 8774): the probability measure of a uniform source is uniquely determined.

Significance

Theorem 1 gives source theory a behavioral foundation: whether a source admits an a-neutral probability measure can be read off from comparisons of bets on its own events, without assuming expected utility for risk. Uniformity is what makes the paper's quantitative tools available. Once a source is uniform, its weighting function factors as $W = w_{\mathcal S}\circ P_{\mathcal S}$, and Theorems 2–4 of the paper compare sources through the pmatcher between their source functions; Theorem 4 uses Theorem 1 as a step. The uniqueness of $P_{\mathcal S}$ (milestone 8) is what makes the source function well defined.

The result is proved in the paper; nothing in it is formalized anywhere to our knowledge. The proof relies on a classical representation theorem for qualitative probability (Krantz, Luce, Suppes and Tversky, 1971, Theorem 5.2.2), which is not in Mathlib either. A complete development would give Lean a first framework of Savage-style acts, biseparable utility and comparative probability, which other decision-theory missions could reuse.

Difficulty

The necessity half rests on the probability $P$ of a uniform source representing event preference strictly, which needs strong monotonicity and the range of $P$ on a convex-ranged source. The sufficiency half is the hard one. From the two attitude conditions alone one has to derive de Finetti's additivity (Lemma B.1). Its proof is a case analysis that uses regularity of the region to guarantee that one of the cells is a genuine middle event. One then needs a representation theorem for qualitative probabilities on an algebra, with uniqueness, in the finitely additive setting. Dropping regularity is not an option: without it the region $B=S$, $D=\emptyset$ makes insensitivity nearly empty, and source preference alone does not imply uniformity (the paper's Example 1). The obvious route through countably additive measure theory is not available either, because the probabilities are only finitely additive.

Formalization scope

All statements share one module, SourceTheory.Uniform.Model. It holds acts (IsActFrom), binary acts (bet), null events, convex rangedness, Assumption1 (a structure with one field per clause of Assumption 1), sources (IsSource), finitely additive probabilities (IsProbOn), uniformity (IsUniformWith, IsUniform), IsPreferredTo (Definition 2), IsMoreInsensitive (Definition 4) and IsRegularRegion. Its text is shared verbatim by the four missions on this paper. The conventions are:

• Events are the members of an algebra $\mathcal E$ (endnote 1 licenses any algebra; the power set is a special case). Every quantified event lies in $\mathcal E$ or in the source, so the values of $W$ off $\mathcal E$ never matter.
• Event preference is $W$-order, as Assumption 1 prescribes. The preference forms (15)–(17), (A.3)–(A.5) therefore coincide with the $W$-forms.
• Assumption 1's "W is convex ranged for every source" is split. Convex rangedness on all events is part of Assumption1, and each source carries its own via IsSource. Reading it over every subalgebra would make Assumption 1 unsatisfiable, because $\{\emptyset,S\}$ has no event of weight $1/2$.
• Twofold partitions are $(A_1,A_1^c)$. Threefold and fourfold partitions are ordered and may have empty cells.
• Probability measures on a source are finitely additive, real valued and nonnegative, with total mass 1.
• In the goal, the boundary events $B, D$ are arbitrary events, and "equally preferred/insensitive to itself" is one copy of each condition: for $\mathcal A=\mathcal C=\mathcal S$ both directions coincide.

Statement (ii) carries an existential region, and it must be regular. A version without regularity, or with uniformity replaced by "$W=w\circ P$ for some $P$", would be a different and weaker theorem.

Needed infrastructure: comparative-probability representation (Krantz et al. 1971, Theorem 5.2.2, or a direct construction via convex rangedness), finitely additive measures on set algebras, and the range of a finitely additive probability that represents a convex-ranged weighting. Proofs of the milestones, of the representation theorem as a reusable lemma, and sanity models of Assumption 1 (for instance an expected-utility agent on $[0,1)$ with Lebesgue measure) are all welcome.

Selected references

• A. Baillon, H. Bleichrodt, C. Li, P. P. Wakker, Source Theory: A Tractable and Positive Ambiguity Theory, Management Science 71(10):8767–8782, 2025. https://doi.org/10.1287/mnsc.2023.03307
• D. Ellsberg, Risk, Ambiguity, and the Savage Axioms, Quarterly Journal of Economics 75(4):643–669, 1961. https://doi.org/10.2307/1884324
• I. Gilboa, Expected Utility with Purely Subjective Non-Additive Probabilities, Journal of Mathematical Economics 16(1):65–88, 1987. https://doi.org/10.1016/0304-4068(87)90022-X
• D. H. Krantz, R. D. Luce, P. Suppes, A. Tversky, Foundations of Measurement, Vol. I, Academic Press, New York, 1971 (cited in the paper for Theorem 5.2.2).
• M. J. Machina, D. Schmeidler, A More Robust Definition of Subjective Probability, Econometrica 60(4):745–780, 1992. https://doi.org/10.2307/2951565
• A. Tversky, C. R. Fox, Weighing Risk and Uncertainty, Psychological Review 102(2):269–283, 1995. https://doi.org/10.1037/0033-295X.102.2.269

Motivation

The European Union's General Data Protection Regulation (GDPR, in force since 2018) shifted control over personal data from firms to consumers: data may be collected and processed only with the consumer's consent, and consent may be given for some uses and withheld for others. Online retailers use consumer data in two opposite ways. Saved shopping carts, stored addresses and location sharing make shopping more convenient for the consumer; the same data can also be monetized against the consumer, through targeted advertising, data sales or other exploitation. Whether giving consumers control over these uses helps them, and what it costs firms and society, is a question for regulators and for operations managers of e-commerce platforms alike.

F. Xu, X. Wang and F. Zhang, Consumer Privacy in Online Retail Supply Chains (Management Science, forthcoming), build a stylized model in which both uses of data appear and the consumers' disclosure decisions are taken under rational expectations. This mission formalizes the paper's single-firm result: when one vertically integrated e-commerce firm sells directly to consumers, the GDPR always raises the firm's profit and social welfare, but it raises consumer surplus only when the product's valuation is below an explicit threshold. A companion mission treats the supplier–retailer chain of the same paper, where the GDPR can hurt all three parties.

Setting

A unit mass of consumers values one product at $v>0$. A consumer's inconvenience cost $\theta$ is uniform on $[0,1]$. The data quality is $\delta\in(0,1)$, and monetizing data at intensity $r\ge0$ costs the firm $cr^2$ with $c>0$. Write

$$\mathcal Z = 2c+\delta,\qquad \mathcal M = 4c^2(1-\delta)+c\delta(4-3\delta)+\delta^2,\qquad \mathcal F = 4c^2(1-\delta)+4c\delta(1-\delta)+\delta^2 .$$

The firm first decides whether to collect data ($\ell\in\{0,1\}$), then sets a price $p\in\mathbb R$. Production is free. A buyer who hides her data gets $v-p-\theta$. A buyer who discloses gets $v-p-(1-\delta)\theta-r\delta$: the data scale her inconvenience down by the factor $1-\delta$, and the firm extracts $r\delta$ from her. Without collection only hiding is available. A consumer buys iff her best buying utility is nonnegative.

Two data policies are compared.

• In the $\mathbb R$ mode (retailer-controlled, before the GDPR), the firm chooses $r$ after the data are collected, to maximize $r\delta s-cr^2$ given the mass $s$ of disclosing consumers. Consumers anticipate $s$; a rational expectations equilibrium (REE) is a pair $(s,r)$ in which $r$ is the firm's best response to $s$ and $s$ is the mass of consumers who disclose given $r$.
• In the $\mathbb C$ mode (consumer-controlled, the GDPR), consumers allow the convenience use and block exploitation, so $r=0$ and every buyer discloses.

The firm's profit is $p\cdot(\text{demand})+r\delta s-cr^2$. Consumer surplus is the integral over $\theta\in[0,1]$ of each consumer's realized utility (zero for non-buyers), and social welfare is profit plus consumer surplus. A subgame-perfect equilibrium (SPE) is a profile with an REE response after every $(\ell,p)$, an optimal price over $\mathbb R$ after each $\ell$, and an optimal $\ell$.

Formalization targets

Goal: Theorem 1 (p. 17)

Let $\tau = \dfrac{2\mathcal M\sqrt{1-\delta}}{\mathcal Z\sqrt{\mathcal F}}$. SPEs exist under both policies, and for every SPE of the $\mathbb R$ mode and every SPE of the $\mathbb C$ mode,

$$v<\tau\ \Rightarrow\ CS_{\mathbb R}<CS_{\mathbb C},\qquad v>\tau\ \Rightarrow\ CS_{\mathbb C}<CS_{\mathbb R},\qquad \pi_{\mathbb R}<\pi_{\mathbb C},\qquad W_{\mathbb R}<W_{\mathbb C}.$$

Milestones

1. The optimal monetization intensity $r(s)=\delta s/(2c)$ (§4.1, p. 11).
2. The REE at each price, display (2) (p. 13), with the saturated branch: $s=2c(v-p)/(2c(1-\delta)+\delta)$, $r=\delta(v-p)/(2c(1-\delta)+\delta)$ when $(v-p)\mathcal Z\le 2c(1-\delta)+\delta$, and $s=2c/\mathcal Z$, $r=\delta/\mathcal Z$ otherwise.
3. Lemma 1 (p. 13): the hide-and-buy, disclose-and-buy and no-purchase intervals.
4. Proposition 1 (p. 14): the $\mathbb R$-mode equilibrium; the firm collects, and $(r^*,p^*,\mathcal T_1(p^*))$ switches form at $v=2\mathcal M/\mathcal Z^2$.
5. Proposition 2 (p. 16): the $\mathbb C$-mode equilibrium; the firm collects, and $(\tilde p^*,\mathcal T_2(\tilde p^*))$ switches form at $v=2(1-\delta)$.
6. The equilibrium consumer surplus in both modes (proof of Theorem 1, p. ec23).
7. The equilibrium profit in both modes (proof of Theorem 1, p. ec23).

Significance

The theorem separates two effects of the GDPR on consumers. The direct privacy effect removes the exploitation loss $r\delta$ of every discloser. The indirect pricing effect works the other way: without the exploitation revenue the firm no longer discounts the price to attract disclosers, and once the market under the GDPR is fully covered the firm raises the price sharply. The threshold $\tau$ says exactly where the second effect overtakes the first. The result that profit and welfare rise regardless of $v$ shows that in a single-firm market the GDPR is never welfare-reducing; the supply-chain mission shows that this conclusion fails once a supplier sets a wholesale price, which is the paper's main policy message.

The paper's proofs (e-companion, Appendix C, pp. ec21–ec24) work with closed forms and leave several steps to "it can be verified". A formal proof checks the reduction from the game to those closed forms: existence and uniqueness of the REE at every price including the saturated range, global optimality of the prices over all of $\mathbb R$, and the collection decision against the full no-collection subgame. To our knowledge no part of this paper has been machine-checked.

Difficulty

The obvious argument plugs the printed formula $r(p)=\delta(v-p)/(2c(1-\delta)+\delta)$ into the profit (3) and maximizes. That formula solves the REE condition only while the market is not saturated; on the saturated range the REE intensity is the constant $\delta/\mathcal Z$, and the profit is a different function of $p$. The firm's problem is therefore a maximization of a piecewise function with a kink at full coverage, and the price comparison has to cover prices above $v$ (no sales) and the subgame without collection.

The consumer-surplus comparison involves two piecewise quadratics with different breakpoints, $2(1-\delta)<2\mathcal M/\mathcal Z^2$, and their single crossing at $\tau$ lies in the middle region where one mode is saturated and the other is not. Strictness of the profit and welfare comparisons needs the identity $\mathcal M-(1-\delta)\mathcal Z^2=c\delta^2+\delta^3>0$ and its relatives.

Formalization scope

All objects are real numbers; $c>0$, $0<\delta<1$ and $v>0$ are hypotheses of every statement. The paper does not state $v>0$; at $v\le0$ nothing is sold, every outcome is $0$, and every strict claim fails, so $v>0$ is a disclosed standing assumption.

Sets of consumers are measured by Lebesgue measure on $[0,1]$ ((volume S).toReal); consumer surplus is the interval integral $\int_0^1\max\{0,u(\theta)\}\,d\theta$. Indifferent consumers buy and disclose (a null set). The REE uses an IsMaxOn condition over $r\ge0$ and the disclosing quantity defined from utilities; neither $r(s)$ nor $\mathcal T_1$ is hard-coded. The firm's profit is defined from the REE response, not from the paper's (3). A strategy profile specifies a price for both collection decisions and an REE response at every $(\ell,p)$ with $p\in\mathbb R$; the comparisons in the goal are between on-path outcomes of such profiles.

The goal is not a comparison of printed closed forms: those are milestones 6–7. It asserts existence of an SPE in each mode, so "every equilibrium" is not vacuous; no price range is restricted and no off-path action is omitted.

Display (2) is stated in its corrected two-branch form for $p\le v$; Lemma 1 is stated for $p\le v$, with $r(p)$ the REE intensity at $p$. The paper's Table 1 (p. 12) misprints the purchase condition of disclosers and is not used.

A complete development needs volumes of intervals, the REE fixed point, maximization of concave piecewise quadratics over $\mathbb R$, and square-root threshold algebra. No probability or limits are involved. The consumer-stage definitions are shared verbatim with the supply-chain mission and may later be merged. Proofs of any milestone, and of auxiliary lemmas such as $2(1-\delta)\le 2\mathcal M/\mathcal Z^2$, are welcome.

Selected references

• F. Xu, X. Wang, F. Zhang, Consumer Privacy in Online Retail Supply Chains, Management Science, forthcoming; author manuscript, version of November 2024. https://doi.org/10.1287/mnsc.2022.01819
• European Union, Regulation (EU) 2016/679 (General Data Protection Regulation), 2016. https://eur-lex.europa.eu/eli/reg/2016/679/oj

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

Consumers judge a price against a reference price, an internal benchmark formed from the prices they have seen before. A price above the reference is perceived as a loss and depresses demand; a price below it is perceived as a gain and stimulates it. Because today's prices shape tomorrow's reference prices, a seller facing reference effects solves a dynamic problem even when demand is otherwise stationary. The single-product theory is classical: Popescu and Wu (2007) showed, for a broad class of demand models, that loss-averse consumers make optimal and myopic price paths converge monotonically, and Hu, Chen and Hu (2016) studied the cyclic behaviour that gain-seeking consumers can induce under linear demand.

Retailers sell many substitutable products, and the standard model of substitution is the multinomial logit (MNL). Guo, Jiang and Shen (2025) combine the two: each product has its own reference price and its own asymmetric sensitivities to gains and losses, and consumers choose among the products by MNL. This mission formalizes the paper's first set of results, on the myopic pricing policy, which maximises the current period's revenue at the current reference prices and ignores the effect on the future. Myopic pricing is both a widely used heuristic and the benchmark against which the optimal policy is measured later in the paper.

Setting

There are $n$ products $N=\{1,\dots,n\}$. Product $i$ has an intrinsic utility $a_i\in\mathbb R$, a price sensitivity $b_i>0$, and reference sensitivities $c_i^+\ge0$ (to gains) and $c_i^-\ge0$ (to losses). At price vector $p$ and reference price vector $r$ the deterministic utility of product $i$ is

$$u_i(p,r)=a_i-b_ip_i+c_i^+(r_i-p_i)_+-c_i^-(p_i-r_i)_+ ,$$

the market share of product $i$ is $q_i(p,r)=e^{u_i}/(1+\sum_k e^{u_k})$, and the single-period revenue is $\Pi(p,r)=\sum_i p_i\,q_i(p,r)$. Product $i$ is loss-averse if $c_i^+<c_i^-$, loss-neutral if $c_i^+=c_i^-$, and gain-seeking if $c_i^+>c_i^-$; the three sets are $N_l,N_n,N_g$.

Prices and reference prices lie in the box $\mathcal P^n=[0,p_H]^n$ with ceiling $p_H>0$. A myopic policy $p^m$ assigns to each $r\in\mathcal P^n$ a maximiser of $\Pi(\cdot,r)$ over $\mathcal P^n$; the maximum value is the optimal single-period revenue $\Pi^m(r)$. Reference prices follow exponential smoothing with memory $\alpha\in[0,1]$:

$$r^{t+1}=\alpha r^t+(1-\alpha)\,p^m(r^t),$$

and $\{p^m(r^t)\}_{t\ge0}$ is the myopic price path. A policy has a steady state if $p^m(r)=r$ for some $r\in\mathcal P^n$.

The paper assumes throughout that $p_H\ge\hat p_H$, where $\hat p_H$ is the unique root of the scalar equation (9), $p=\chi+\sum_i \frac{1}{b_i+c_i^+}e^{a_i-b_ip+(b_i+c_i^+)\chi-1}$ with $\chi=\max_i 1/(b_i+\min\{c_i^+,c_i^-\})$. This ceiling assumption makes the ceiling non-binding for the myopic problem.

Formalization targets

Goal: Theorem 3, long-run behaviour of the myopic policy

For every myopic policy $p^m$ and every $r^0\in\mathcal P^n$:

$$N_g=\emptyset\ \Longrightarrow\ p^m(r^t)\to L\in\mathcal P^n,\ \text{and } p^m(L)=L \text{ when } \alpha<1;$$ $$N_g\neq\emptyset\ \Longrightarrow\ p^m(r)\neq r\ \ \forall r\in\mathcal P^n,\ \text{and the path does not converge when } \alpha<1 .$$

Milestones

1. Proposition 1.2 (p. 10): (9) has a unique root $\hat p_H$, and for $p_H\ge\hat p_H$ the maximisers of $\Pi(\cdot,r)$ over $\mathcal P^n$ are its maximisers over $\mathbb R^n$.
2. Theorem 2 (p. 13): every myopic price is $\Pi^m(r)$ plus an explicit constant that depends on the product's type and on where $r_i$ lies relative to thresholds such as $\Pi^m(r)+Z_i$, $Z_i=\frac{\log(b_i+c_i^+)-\log(b_i+c_i^-)}{c_i^+-c_i^-}$.
3. Theorem 1 (p. 12): $\Pi^m(r)$ is the unique root of the scalar equation (13).
4. Corollary 1 (p. 12): the right-hand side of (13) is non-increasing in $\Pi$.
5. §3.1, p. 13: $\Pi^m(r)$ is non-decreasing in $r$.
6. Corollary 2 (p. 16): if every product is loss-neutral, the myopic policy has a unique steady state $p_i^{m\star}=\Pi^{m\star}+1/(b_i+c_i)$, with $\Pi^{m\star}$ the unique root of (18), and the price paths of all products move synchronously.

Significance

Theorem 3 separates two regimes by consumer type alone. With loss-averse and loss-neutral consumers a seller who reprices myopically settles at a stable price vector; with even one gain-seeking product no price vector is self-reproducing, and myopic prices keep oscillating. Theorems 1 and 2 are the structural results behind this: they reduce a non-concave, non-smooth $n$-dimensional optimisation to one scalar equation with a monotone right-hand side, which is also how the myopic policy is computed in practice. The same structure is used later in the paper to bound the gap between myopic and optimal revenue.

All results are proved in the paper; the proofs are in its online supplement (Appendices B.1–B.5), which is not part of the source file used here. None of the results is formalized. The work in this mission is the first machine-checked treatment of MNL pricing with reference effects: global optimality of a candidate maximiser for a non-concave revenue, the analysis of a scalar root equation with piecewise definitions, and the dynamics of a map that is continuous without gain-seeking products and discontinuous with them.

Difficulty

The obvious route to Theorem 2, setting the gradient of $\Pi(\cdot,r)$ to zero, fails twice. The revenue has kinks at $p_i=r_i$, so a maximiser may sit at a kink where no gradient exists; this is the middle branch $p_i^m=r_i$ for loss-averse products. And the revenue is not concave in prices: for a gain-seeking product the first-order conditions have several solutions, and a global maximiser must be singled out among them. The usual reformulation of MNL pricing in market-share variables, which restores concavity without reference effects, does not survive the kinks.

For Theorem 3 the difficulty is dynamic. Without gain-seeking products the myopic map is continuous, but the flat middle branch of (14) makes it non-contracting, so the standard contraction arguments do not apply, and the limit depends on the starting point. With a gain-seeking product the map jumps at the threshold $\Pi^m+Z_i$, so continuity-based arguments about the limit of the path are unavailable.

Formalization scope

Products are indexed by Fin n (0-based); vectors are Fin n → ℝ with the product topology and the coordinatewise order. The standing hypotheses $b_i>0$, $c_i^\pm\ge0$, $\alpha\in[0,1]$, $p_H>0$ and the ceiling assumption (as "some root of (9) is at most $p_H$") appear as hypotheses of every theorem that needs them; Corollary 1 needs only $b>0$, $c^\pm\ge0$. The market shares (3) are defined directly, without the Gumbel derivation. $\chi$ is an indexed supremum over Fin n (zero when $n=0$). The three sums of (13) are written as one sum whose term is chosen by product type.

Maximisers need not be unique, so a myopic policy is any selection of maximisers, and every statement holds for all selections; $\Pi^m(r)$ is the revenue of an arbitrary maximiser. "The unique solution" is split into "is a solution" and "every solution equals it". The following deviations are disclosed in the items: at the threshold $r_i=\Pi^m+Z_i$ of (16) both prices are maximisers, so only "one of the two" is claimed there; the fixed-point property of the limit in Theorem 3, and every limit claim of Corollary 2, require $\alpha<1$, since at $\alpha=1$ the price path is the constant $p^m(r^0)$; the non-convergence clause in Theorem 3.2 is an addition to the literal "no steady state". "Monotone decreasing" (Corollary 1) and "monotone increasing" (Corollary 2, §3.1) are read non-strictly.

A trivializing formalization is ruled out: Theorem 3.2 quantifies over every reference price in the box and every myopic selection, Theorem 3.1 asserts convergence from every initial reference price rather than the existence of some fixed point, and Theorems 1–3 keep the ceiling assumption, without which the maximiser can sit on the boundary and (14)–(16) fail.

A complete development needs: continuity and compactness facts for the MNL revenue on a box; optimality conditions for the kinked, non-concave revenue; one-variable analysis of the piecewise-exponential right-hand side of (13); and convergence results for monotone or continuous recursions in $\mathbb R^n$. The MNL and reference-price infrastructure is reusable by the five other missions of this series. Contributions to any milestone, and alternative proofs, are welcome.

Selected references

• M. A. Guo, H. Jiang, Z.-J. M. Shen, Multi-Product Dynamic Pricing with Reference Effects Under Logit Demand, Manufacturing & Service Operations Management, 2025; source used: SSRN 4189049, version of 2024-05-25. https://ssrn.com/abstract=4189049, https://doi.org/10.1287/msom.2024.0801
• I. Popescu, Y. Wu, Dynamic Pricing Strategies with Reference Effects, Operations Research 55(3), 2007. https://doi.org/10.1287/opre.1070.0393
• Z. Hu, X. Chen, P. Hu, Dynamic Pricing with Gain-Seeking Reference Price Effects, Operations Research 64(1), 2016. https://doi.org/10.1287/opre.2015.1446
• D. McFadden, Conditional Logit Analysis of Qualitative Choice Behavior, in Frontiers in Econometrics, Academic Press, 1974.

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

Large technology firms often buy small startups mainly to hire their staff, a practice known as acquihiring. Antitrust authorities review acquisitions that may reduce competition in product markets, but an acquihire can instead reduce competition in the labour market: a firm that buys the employer of a scarce worker no longer has to outbid that employer for her. Bar-Isaac, Johnson and Nocke study this effect in a three-player model: a startup, its essential employee, and a potential acquirer (CRC TR 224 Discussion Paper No. 500, 2024; published in Management Science, 2025, doi:10.1287/mnsc.2024.04604).

In the paper's baseline model (Proposition 1) the acquirer, whenever it hires the employee, does so by buying the startup, and the employee always prefers direct wage competition. This mission formalizes §6, where the employee's private benefit from staying at the startup is her private information. That uncertainty softens wage competition, so acquihiring is no longer always chosen, and the paper derives the exact threshold at which the acquirer switches.

Setting

An employee produces value $v_a$ if she works for the acquirer and $v_s$ if she works for the startup. At the startup she also enjoys a private benefit $b$, which only she observes and which is uniformly distributed on $[0,B]$. She has an outside option worth $0$, and wages are unrestricted real numbers. The standing assumptions of §6 are

$$0 < B < \min\{v_a, v_s\}, \qquad v_s - B < v_a < v_s + 2B .$$

The acquirer chooses between two modes.

• Direct hiring. The acquirer and the startup make simultaneous wage offers $w_a$ and $w_s$. A type-$b$ employee joins the acquirer when $w_a > w_s + b$ and $w_a \ge 0$, and stays at the startup when $w_s + b \ge w_a$ and $w_s + b \ge 0$. Expected profits are averages over $b \sim U[0,B]$, for example

$$\pi_a(w_a, w_s) = \frac1B \int_0^B (v_a - w_a)\,\mathbf 1\{\text{type } b \text{ joins the acquirer}\}\,db .$$

A pair $(w_a, w_s)$ is an equilibrium of this wage game when each offer is a best response to the other over all real wages.

• Acquihiring. The acquirer bids for the startup. A startup that is a monopsonist pays wage $0$ and earns $v_s$, so the acquisition succeeds at price $v_s$ exactly when $v_a > v_s$, and the acquirer then pays the employee $0$. The acquirer's acquihiring profit is $\max\{0, v_a - v_s\}$ (Lemma 2 of the paper with wage floor $0$).

The quantities named in the statements are Lemma 5's wages

$$w_a^* = \frac{2v_a + v_s - B}{3}, \qquad w_s^* = \frac{2v_s + v_a - 2B}{3},$$

the indifferent type $b^* = (v_a - v_s + B)/3 = w_a^* - w_s^*$, and the threshold

$$\hat v_a = v_s + \frac{7 - 3\sqrt5}{2}\,B .$$

Formalization targets

Goal: Proposition 5

Under the standing assumptions, $\hat v_a > v_s$, $(w_a^*, w_s^*)$ is a direct-hiring equilibrium, and

$$v_a > \hat v_a \;\Longrightarrow\; \pi_a(w_a^*, w_s^*) < \max\{0, v_a - v_s\},$$ $$v_a < \hat v_a \;\Longrightarrow\; \max\{0, v_a - v_s\} < \pi_a(w_a^*, w_s^*) \ \text{ and the poaching probability is } \frac{v_a - v_s + B}{3B}.$$

In addition, every type $b \in [0,B]$ of employee is strictly better off under direct hiring than under acquihiring.

Milestones

1. A monopsonistic startup sets wage $0$ and earns $v_s$; a monopsonistic acquirer sets wage $0$ (§6, p. 15).
2. Lemma 5: the direct-hiring wages, the poaching probability $(v_a - v_s + B)/(3B) \in (0,1)$, and the acquirer's profit $(v_a - v_s + B)^2/(9B)$.
3. The two values of $v_a$ at which the profits are equal, $\hat v_a$ and $v_s + (7 + 3\sqrt5)B/2$, and the fact that the second lies above $v_s + 2B$.
4. The welfare display in the proof of Corollary 4, and Corollary 4 itself: acquihiring is more efficient than direct hiring exactly when $v_a > v_s + \tfrac45 B$, so on $\tfrac{7-3\sqrt5}{2} < (v_a - v_s)/B < \tfrac45$ the acquirer acquihires although direct hiring yields more surplus.

Significance

The proposition separates two effects that coincide in the baseline model. Without private information, wage competition is Bertrand-like: the winning firm must match the losing firm's full willingness to pay, so buying the competitor is always cheaper. With a privately known benefit, competition between the two employers resembles product differentiation, and each offers less than the employee's productive value. Direct hiring then becomes profitable when $v_a$ is close to $v_s$, and acquihiring is chosen only when $v_a - v_s$ exceeds $\frac{7-3\sqrt5}{2}B \approx 0.146\,B$. Corollary 4 compares this threshold with the efficiency threshold $\frac45 B$ and finds a band of parameters in which acquihiring occurs although it lowers total surplus. That band is the paper's case for labour-market scrutiny of acquisitions.

The results are proved on paper, by first-order conditions and a quadratic comparison. None of them has a machine-checked proof, and the platform has no prior formalization of wage competition, monopsony or acquisitions. The mission adds an explicit Bayesian wage game with expected profits written as integrals over the type distribution, with global best responses rather than first-order conditions. The objects are small enough to be reused for other two-firm wage-posting models with a uniformly distributed taste shock.

Difficulty

The algebra of Proposition 5 is a quadratic inequality in $(v_a - v_s)/B$. The work is in Lemma 5. The page solves first-order conditions inside the region $w_a \ge 0$, $0 < w_a - w_s < B$, where both expected profits are concave quadratics. An equilibrium, however, requires that no deviation pays anywhere on the real line, including offers so low that no type accepts and offers so high that every type accepts. Outside the interior region the profit functions are piecewise (zero below, linear above), and each piece has to be compared with the interior optimum. The expected profits are interval integrals of indicator functions, so evaluating them requires the measure of the set of accepting types. Ties between the two offers occur with probability zero, and the statements are insensitive to how they are broken.

Formalization scope

All quantities are real numbers. The parameters $v_a$, $v_s$, $B$ form a structure, and the five standing inequalities form a predicate that every theorem except the pure-algebra milestone takes as a hypothesis (that milestone needs only $B > 0$). Expected profits, the poaching probability and direct-hiring welfare are $\frac1B \int_0^B$ of bounded, piecewise-constant integrands, hence interval integrable. A verification file evaluates the acquirer's profit at Lemma 5's wages to its closed form on one instance, and exhibits instances of both branches of the proposition and of the window in Corollary 4. Ties $b = w_a - w_s$ go to the startup.

Conventions committed to:

• best responses range over all real wages, which is stronger than the page's first-order conditions;
• the direct-hiring branch is evaluated at Lemma 5's wages, and Lemma 5's uniqueness clause is claimed only within the interior region where the page derives it; uniqueness among all equilibria is not on the page and is not claimed;
• the acquihiring profit $\max\{0, v_a - v_s\}$ and the employee's acquihiring payoff ($0$ if $v_a > v_s$, otherwise her benefit $b$) are Lemma 2's outcomes with wage floor $0$, as §6 states; the milestone on the monopsonistic wage justifies this, and at $v_a = v_s$ the acquisition is taken to fail;
• surplus under acquihiring is $v_a$, the allocation with the employee at the acquirer, as in Corollary 4.

The direct-hiring profit is an integral over the type distribution evaluated at wages that are proved to be an equilibrium. It is not a closed-form payoff taken as a definition. Dropping any standing inequality would change Lemma 5 (the poaching probability leaves $(0,1)$) or Proposition 5 (the second root comes back into range). The employee-preference clause is part of the goal, and no equilibrium is claimed unique beyond what the page derives.

Contributions welcome: the interval-integral evaluations of step functions, the global best-response argument for Lemma 5, and the quadratic comparison with $\sqrt5$.

Selected references

• H. Bar-Isaac, J. P. Johnson, V. Nocke, Acquihiring for Monopsony Power, CRC TR 224 Discussion Paper No. 500, January 2024 (the version formalized here; journal version below).
• H. Bar-Isaac, J. P. Johnson, V. Nocke, Acquihiring for Monopsony Power, Management Science, 2025. https://doi.org/10.1287/mnsc.2024.04604