All missions

Motivation

Private equity funds ask investors to commit capital before the timing of their own cash needs is known. If an investor needs liquidity before the fund pays out, selling a partnership claim can be more useful than holding it to maturity. The price at which such claims trade therefore affects both the return investors demand when a fund is raised and the way fund managers schedule capital calls. Maurin, Robinson, and Strömberg study these two markets together in A Theory of Liquidity in Private Equity. The mission follows the authors’ December 2020 working-paper draft, whose Proposition 3 characterizes equilibrium when L-fund claims can trade in a secondary market.

Setting

A unit mass of general partners (GPs) each has wealth $A$ and raises one fund of size $I>A$. The fund makes two independent investments. A share $x$ is invested at the first date and $1-x$ at the second. Each unit succeeds with probability $p$ if the GP works, pays $R$ when successful, and otherwise pays zero. Shirking lowers the success probability to $q<p$ but gives the GP a private benefit $B$ per unit. A contract assigns the GP a fee to each pair of success outcomes. The fee is subject to limited liability and must give the GP enough incentive to work on both investments. The GP chooses the fee, $x$, and $I$ to maximize expected fee income, while meeting the investors’ promised return and the constraint that they will honor the second capital call.

The limited partners (LPs) have total capital $K$. A fraction $\mu_H$ belongs to type H and the rest to type L. With probability $\lambda$, a common liquidity shock makes period-two proceeds less useful at period one. Type $i$ values a unit of those later proceeds at $\delta_i$, with $0<\delta_L<\delta_H<1$. Type H is therefore more willing to hold an illiquid claim. Each LP chooses whether to supply capital to a primary fund or keep cash, and a cash holder may buy fund claims after the shock.

The secondary market has one actively traded asset: an L-fund claim. Its price is $P_L$ and its promised expected payoff is $\bar R_{PE,L}$. L-LPs supply claims when the price reaches their reservation value $\delta_L\bar R_{PE,L}$. H-LPs buy them when the price is at most $\delta_H\bar R_{PE,L}$, using capital left after any primary H-fund commitment. The discount to net asset value is

$$D_L=1-\frac{P_L}{\bar R_{PE,L}}.$$

An equilibrium specifies both funds’ contracts and promised returns, the fractions of GPs raising each fund type, primary capital supply, and secondary claims sold and bought. Contracts must be globally optimal among feasible contracts at their quoted returns, and both markets must clear.

Formalization targets

Return gap and market clearing

At a discount $D_L\in[1-\delta_H,1-\delta_L]$, the minimum returns acceptable to L- and H-LPs are described by (C.5) and (C.6). Lemma 3 asserts that the gap between the H and L minimum returns grows strictly with the discount. The gap is zero at $D_L=1-\delta_H$ and positive above it. For interior discounts, the secondary clearing equation is

$$(I_L-A)P_L=\mu_H K.$$

These statements are milestones because they give solvers the return comparison and the equation that determines price when all claims sell.

Proposition 3: secondary-market equilibrium

Under the paper’s Assumptions 1–3 and 5–7, together with the capacity condition described below, the goal is a set of ordered capital-share thresholds

$$0<\mu_{H,1}<\mu_{H,2}<\mu_{H,3}<\bar\mu_H.$$

An equilibrium exists for every $\mu_H\in(0,1)$. H-funds are raised only at or above $\mu_{H,3}$; if both fund types are raised, their promised returns agree. At or below $\mu_{H,3}$, only L-funds are raised and their promised return is $1/(1-\lambda D_L)$. Equation (22) gives $D_L=1-\delta_L$ below $\mu_{H,1}$, a capital-clearing ratio between $\mu_{H,1}$ and $\mu_{H,3}$, and $D_L=1-\delta_H$ at the third threshold. It also describes the early capital call: the lower boundary $\hat x(\lambda,\delta_L)$ at small H capital shares, the binding no-default call in the middle, and an interval of undistorted optimal calls near the third threshold.

Significance

The result explains why more liquid investors may prefer to provide liquidity in the resale market instead of financing funds directly. It ties the observed secondary-market discount to the amount of H capital available to buy claims and identifies the ranges where that discount changes the GP’s early capital call. Without the return and clearing conditions, the discount would be an exogenous price rather than an equilibrium object.

The cited paper proves this characterization in its economic model; this mission asks for machine-checked proofs of the formal statements. The resulting definitions cover incentive-compatible partnership contracts, primary capital supply, and the secondary claims market. They can also support later formal work on the welfare comparison in Corollary 2. None of the goal or milestone statements is claimed to have a machine-checked proof here.

Difficulty

There are two linked optimization problems. A GP chooses a fee and an early call under incentive, limited-liability, and no-default constraints. LPs then compare the value of primary investment with cash that can be used to buy claims after the shock. Solving only the contract problem does not determine the secondary price: that price changes the LPs’ outside option and the no-default constraint at the same time. The return comparison in Lemma 3 and the capacity available to each LP type are central to ruling out an apparently attractive H-fund equilibrium.

Formalization scope

Lean represents amounts, probabilities, prices, and returns by real numbers. Fee schedules are functions on the four ordered pairs of investment outcomes; the source indexes them by cash flow, so two equal-cash-flow outcomes at $x=1/2$ are formally distinct. Fund size satisfies the multiplied identity $(pR-\bar f)I=\bar R(I-A)$ and $I>A$, avoiding a meaningless value from division by zero. An optimal contract is compared with every feasible contract at the same promised return. The secondary value of cash uses the two positive prices, and the discount is defined only from a positive L return.

The standing parameters impose $q>0$, $p\leq1$, strict Assumption 5 at $\delta_L$, and $B\leq p(p-q)R$ so a fee with the required incentives can satisfy limited liability. The equilibrium also specifies nonnegative GP fractions summing to one. A raised fund must maximize GP profit; at a profit tie either fund may be selected. The printed supply and demand schedules are extended by zero outside their quoted reservation-price range. These choices fix cases left implicit by the paper.

The goal adds a sufficient L-capital condition: at $\mu_{H,3}$, L-LP capital covers the maximum primary external-financing need. The printed Proposition 3 lacks this condition. Its Step 1 assumes L-LP participation binds, yet Assumption 3 bounds only total $K$; for permitted smaller $K$, L-LPs can be scarce and the printed return formula fails. The added condition is explicit in the goal rather than hidden in the equilibrium definition. Assumption 7 is also a goal hypothesis, since it is specific to the no-segmentation result.

Assumption 4’s capital-call relief argument, Appendix A’s alternative contracts, the option for no GP fund, and the dynamic interpretation in Section 5.2 are outside this mission. The no-default constraint of (4) is imposed directly. A proof must establish equilibrium existence as well as properties of all equilibria, so a vacuous equilibrium predicate cannot meet the target. Contributions to the contract, return-gap, and clearing milestones are welcome.

Selected references

• Vincent Maurin, David T. Robinson, and Per Strömberg, A Theory of Liquidity in Private Equity, Management Science, 2023. DOI: 10.1287/mnsc.2022.4612. The formal statements use the authors’ December 2020 working-paper draft, especially §§3–4, §6, and Appendix C.5–C.6.

Why investment can reverse a cost advantage

Quantum algorithms can reduce the work needed for some computations, but a provider also has to build hardware capable of serving a market. Bova, Goldfarb, and Melko model these two costs separately in Quantum Economic Advantage. Their question is whether a quantum provider can choose more market-creating investment than a classical rival even when building that additional quantum capacity is more expensive. The answer matters to their economic comparison: a lower variable cost does not, by itself, order the firms' investment decisions.

The working paper was circulated as NBER Working Paper No. 29724 in February 2022 and appeared in Management Science in 2023. This mission cites the NBER version throughout. It addresses the paper's Proposition 2, its explicit numerical witness, and the model results used around that proposition. The paper proves these results analytically; the remaining task here is a machine-checked formalization of their statements and proofs.

The two-stage duopoly

There are two firms. Firm 1 supplies quantum computing and has constant unit cost $c$; firm 2 supplies classical computing and has unit cost $c^2$. A common demand intercept $a$ measures the initial market size. The paper assumes $a>c^2>c>1$. The firms sell differentiated computing services, with substitution parameter $\gamma\in[0,1]$: at $\gamma=0$ their products do not compete through demand, while at $\gamma=1$ they are identical in the model. This is an economic representation of quantum advantage, rather than a formal model of a quantum algorithm. See §2 of the working paper.

In stage 1, firms simultaneously choose investments $x_1,x_2\ge0$. Firm $i$ pays $B_i x_i^2/2$, where $B_i>0$, and its investment raises its own demand intercept to $a+x_i$. In stage 2, after observing both investments, firms simultaneously choose quantities $q_1,q_2\ge0$. Their inverse-demand prices and profits are

$$p_1=a+x_1-q_1-\gamma q_2,\qquad p_2=a+x_2-q_2-\gamma q_1,$$ $$\pi_1=q_1p_1-cq_1-\frac{B_1x_1^2}{2},\qquad \pi_2=q_2p_2-c^2q_2-\frac{B_2x_2^2}{2}.$$

A subgame-perfect equilibrium consists of an investment pair and a quantity strategy assigning a Cournot Nash equilibrium to every feasible investment pair, including pairs reached after a unilateral deviation. At the chosen investments, neither firm can improve its profit by changing its own investment, anticipating the stage-2 strategy. The stage-2 payoff excludes investment cost because that cost is already sunk when quantities are chosen.

Formalization targets

Proposition 2: investment reversal

The goal is the paper's existence claim, over the game itself:

$$\exists\,(a,c,\gamma,B_1,B_2)\text{ satisfying the model and Lemma 1 conditions},\quad B_2<B_1,\quad \exists\,\text{an SPE},\quad \forall\,\text{SPEs},\;x_2<x_1.$$

The classical firm's cost coefficient is smaller, yet the quantum firm invests more. The proof gives $a=20$, $c=2$, $\gamma=1$, $B_1=10$, $B_2=8$; its investments are $x_1^*=102/109$ and $x_2^*=89/109$. The goal concerns the actual two-stage equilibrium, so the closed forms are supporting milestones rather than the definition of success. The paper's Proposition 2 and its proof appear on PDF pages 14 and 27–28.

Supporting results

Equations (3)–(4) give the interior Cournot quantities; (14)–(15) give the second derivatives of reduced profit; Lemma 1 gives sufficient parameter thresholds for positive investments and concavity; and (5)–(6) give equilibrium investments. Section 7 derives an exact threshold for the inequality $x_1^*>x_2^*$ and evaluates it at the numerical witness. Additional milestones record the displayed optimal profits, Proposition 1 on positive quantum profit, the no-investment comparative static of (11)–(12), and Corollary 1's monopoly case. These targets follow the working paper's equations and proofs.

What the result establishes

The result separates a firm's marginal cost of supplying computations from its cost of expanding the market. In this model, the quantum firm can justify a larger investment even with a larger coefficient on investment cost. The exact threshold identifies which combination of demand, variable cost, competition, and investment costs creates that ordering. Proposition 1 and the comparative static make related claims about profitability and the value of additional market size.

A complete formalization would connect the printed algebraic formulas to best responses over nonnegative actions, including possible corner outcomes after off-path investments. The reusable component is the published linear differentiated Cournot game; this mission adds the investment stage and source-specific parameters. The working paper supplies proofs on paper, while the Lean theorem files here are open statements awaiting machine-checked proofs.

Where the argument is delicate

Equations (3)–(4) solve interior first-order conditions, but stage-2 deviations can drive one firm's quantity to zero. A proof about a genuine subgame-perfect equilibrium must handle those corners throughout the strategy, not only at the final investment pair. Likewise, the second derivatives of the algebraic interior profit do not automatically settle every stage-1 deviation in the constrained game. The mission's equilibrium milestone must bridge those two readings. Lemma 1's thresholds also contain quotients whose denominators require checking under the stated parameter conditions.

Formalization scope and conventions

All parameters, investments, quantities, profits, and thresholds are real. The formalization requires $x_i,q_i\ge0$ in the equilibrium predicates. Standing records $0\le\gamma\le1$, $a>c^2>c>1$, and positive $B_i$. Lemma1Cond records the strict thresholds at the end of the proof of Lemma 1, with the paper's $\operatorname{Max}$ represented by real max. Firm 1 is quantum throughout; firm 2's unit cost is defined as $c^2$, not an independent parameter. The closed-form quantities and investments are used in milestones; the main goal quantifies over the subgame-perfect equilibrium predicate.

Several printed or implicit conventions affect the statements. Lemma 1 is phrased loosely on PDF page 11; its proof's exact sufficient conditions on page 26 are the milestone. The proof's strict claims about differences of thresholds become equalities when $\gamma=0$, without changing the final sufficient condition. Corollary 1 uses a different regime, $a<c^2$, and is stated without the main model's Standing condition; $c<a$ ensures the asserted quantum monopoly has positive output. The comparative static concerns the separate model with $x_1=x_2=0$. A printed reference to optimal profits in “(11)” in the proof of Proposition 1 points to the unnumbered optimal-profit display on PDF page 12. The repeated $x_1^*$ in the proof of Proposition 2 is read as $x_1^*,x_2^*$.

Useful contributions include proofs about nonnegative Cournot best responses and their uniqueness, the boundary behavior of stage-1 reduced profits, the exact sign conditions on the paper's denominators, and proofs of the source-indexed statements. The definition layer is meant to be shared by all results in this one paper.

Selected references

• Francesco Bova, Avi Goldfarb, and Roger G. Melko, Quantum Economic Advantage, NBER Working Paper No. 29724, 2022. Working paper.
• Francesco Bova, Avi Goldfarb, and Roger G. Melko, Quantum Economic Advantage, Management Science, 2023. DOI: 10.1287/mnsc.2022.4578. The mission's theorem numbering follows the NBER version above.

Fundraising competition after a disaster

In the days after a sudden-onset disaster, several humanitarian organizations (HOs) appeal to the same pool of donors. Donors increasingly want to earmark their gifts (restrict them to a programme, region or item), and HOs can offer more or less of that control. Earmarked money is less useful in the response: renegotiating restrictions costs time and overhead, so each dollar delivers less immediate relief. HOs therefore face a trade-off between attracting donors and using donations well, and they face it while competing with each other for the same donors.

A. Aflaki and A. J. Pedraza-Martinez model this trade-off as a game among HOs whose donors choose by a multinomial logit (MNL) rule, and compare three regimes: competition, full collaboration and partial collaboration (SSRN 3705595, December 2022; published in Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2023.1202). This mission formalizes the equilibrium result for the competition regime, Proposition 1 of the paper. The source is the SSRN version dated December 2022; its proofs are in the bound-in Online Supplement (§S3).

The competition game

There are $n \ge 1$ HOs $i \in I = \{1, \dots, n\}$. HO $i$ chooses two numbers:

• a base utility $s_i \in [a_i, b_i]$ that it offers donors (in the paper, a monotone reparametrization of its earmarking level, used from problem (6) on);
• a fundraising effort $x_i \in [0,1]$, the fraction of donors it contacts, at cost $C_i(x_i)$ with $C_i : [0,1] \to \mathbb R_+$ strictly increasing.

Each dollar HO $i$ receives produces $\delta_i(s_i)$ dollars of immediate relief, the unit performance. HO $i$ needs $B_i > 0$ dollars of effective funding. Donors have mean budget $z > 0$.

A donor contacted by the set $J$ of HOs gives HO $i \in J$ the MNL share

$$\theta^J_i(s) = \frac{e^{s_i}}{1 + \sum_{j\in J} e^{s_j}}, \tag{4}$$

the $1$ standing for not donating. Contacts are independent, so with $w^a_i = \prod_{j \ne i} x_j^{a_j}(1-x_j)^{1-a_j}$ for $a \in A_i = \{a \in \{0,1\}^n : a_i = 1\}$ and $J_a = \{j : a_j = 1\}$, HO $i$'s expected donations are

$$\mathbb E[D_i(s;x)] = z\, x_i \sum_{a\in A_i} w^a_i\, \theta^{J_a}_i(s). \tag{5}$$

The unit performance per donor contacted is $PPD_i(s;x) = \delta_i(s_i)\, z \sum_{a\in A_i} w^a_i\, \theta^{J_a}_i(s)$; it does not depend on $x_i$.

Each HO is lexicographic (problem (6)): given the others' strategies, it first minimizes its funding gap $(B_i - \delta_i(s_i)\mathbb E[D_i(s;x)])^+$ over $[a_i,b_i]\times[0,1]$, and among the minimizers it maximizes

$$U_i(s_i,x_i) = \min\big(\delta_i(s_i)\mathbb E[D_i(s;x)],\, B_i\big) - C_i(x_i).$$

A Nash equilibrium is a profile $(s;x) \in \prod_i [a_i,b_i]\times[0,1]^n$ in which every HO's strategy solves its problem (6).

Assumption 1 (p. 16) asks that $\log\delta_i$ be sufficiently concave: $\partial^2 \log\delta_i(s_i)/\partial s_i^2 \le -\tfrac14 + e^{s_i}/(1+e^{s_i})^2$ on $[a_i,b_i]$.

Formalization targets

Goal: Proposition 1 (p. 16)

Under the standing hypotheses and Assumption 1, a Nash equilibrium exists, and a profile in the strategy box is an equilibrium if and only if for every $i$

$$x_i = \min\Big(\frac{B_i}{PPD_i(s;x)},1\Big),\qquad \frac{\delta_i'(s_i)}{\delta_i(s_i)} + \frac{\sum_{a\in A_i} w^a_i\,\partial\theta^{J_a}_i(s)/\partial s_i}{\sum_{a\in A_i} w^a_i\,\theta^{J_a}_i(s)} + \lambda_{i1}-\lambda_{i2} = 0,$$

with $\lambda_{i1},\lambda_{i2}\ge 0$, $\lambda_{i1}(a_i-s_i) = 0$ and $\lambda_{i2}(s_i-b_i) = 0$ (system (7)).

Milestones

1. Lemma 2 (p. 15): $\mathbb E[D_i]$ is nondecreasing in $x_i$ and $s_i$ and nonincreasing in $x_j$, $s_j$ for $j\ne i$.
2. Claim (S5) (p. S10): HO $i$'s strategy solves (6) iff $s_i$ maximizes $PPD_i$ over $[a_i,b_i]$ and $x_i = \min(B_i/PPD_i,1)$.
3. (S8) (p. S12): $\partial^2 \log\big[\sum_{a} w^a_i\theta^{J_a}_i(s)\big]/\partial s_i^2 \le \tfrac14 - e^{s_i}/(1+e^{s_i})^2$ for efforts in $[0,1]$.
4. Log-concavity (p. S12): under Assumption 1, $s_i \mapsto PPD_i$ is log-concave on $[a_i,b_i]$.

Significance

Proposition 1 is the foundation of the paper's comparison of fundraising regimes: Propositions 2, 5, 6 and 7 compare equilibria characterized by (7) with the full- and partial-collaboration outcomes, and the numerical study of the Haiti response (§8) computes equilibria by solving (7). The proposition reduces a two-level game with a non-smooth objective to a per-HO KKT system plus a closed-form effort, and it shows that equilibrium earmarking balances the relative loss in unit performance against the relative gain in donor share.

The result is proved on paper, in the Online Supplement; no machine-checked version exists. Formalizing it would check the reduction from the lexicographic problem to (S5), which hinges on $B_i>0$ and strictly increasing costs, and supply a sound proof of the bound (S8), whose printed derivation is loose (see below). The log-mixture-of-logit bound (S8) and the lexicographic best-response reduction are reusable for other MNL competition models.

Difficulty

The central difficulty is (S8). Each single share $\theta^J_i$ is log-concave in $s_i$, but a mixture of log-concave functions is not log-concave in general, so concavity of $\log\sum_a w^a\theta^{J_a}$ fails and only the weaker, $s_i$-dependent bound (S8) holds. The printed argument passes through a quasi-concavity step and a termwise inequality that do not combine as written; a correct argument must control the variance-like term of the mixture uniformly in the weights. Numerical tests on random instances support (S8).

Existence is a fixed-point argument, but Assumption 1 with "$\le$" yields only concavity, so best responses in $s_i$ can be intervals rather than points, and a single-valued map need not exist. The correspondence is convex-valued, which is where the obvious Brouwer argument needs adjustment.

The reduction (S5) requires handling both regimes of the lexicographic problem: the gap can be closed (effort $B_i/PPD_i$, minimal cost) or cannot (full effort).

Formalization scope

HOs are Fin n. The paper's sum over $a\in A_i$ is a sum over finite sets $J$ with $i\in J$; $w^a_i$ is the product of $x_j$ over $J\setminus\{i\}$ and of $1-x_j$ over $j\notin J$. All statements live in base-utility coordinates: $\delta_i:\mathbb R\to\mathbb R$ is a primitive function of $s_i$ (earmarking $e_i$ and the map $s_i(e_i,\delta_i(e_i))$ are not modelled), and expected donations are the formula (5) (Lemma 1's Gumbel derivation is not formalized).

The standing hypotheses, collected in one predicate, are: $n\ge1$; $a_i\le b_i$; $B_i>0$; $z>0$; $C_i\ge0$ and strictly increasing on $[0,1]$; $\delta_i$ twice continuously differentiable on $\mathbb R$ with $0<\delta_i\le1$ on $[a_i,b_i]$. The additions relative to the page are $B_i>0$ (without it every $s_i$ is a best response and the "only if" fails), $z>0$, $\delta_i>0$ (needed for $\log\delta_i$ and $B_i/PPD_i$), and smoothness on all of $\mathbb R$ rather than on $[a_i,b_i]$. Assumption 1 is a separate predicate, assumed only by the goal and the log-concavity milestone. Derivatives are Mathlib's deriv; $\partial\theta^{J}_i/\partial s_i$ is the derivative of $t\mapsto\theta^J_i(s_{-i},t)$.

The equilibrium is defined as the lexicographic best response of problem (6) over the full strategy box, never by (7), (S5) or an argmax of $PPD_i$; with any of those as the definition the goal would be trivial. Multipliers are existential. Uniqueness of the equilibrium is not claimed.

Welcome contributions: proofs of the milestones, a reusable lemma that the KKT conditions characterize maximizers of a concave differentiable function on a closed interval, and Kakutani-type existence for convex-valued best responses.

Selected references

• A. Aflaki, A. J. Pedraza-Martinez, Competition and Collaboration on Fundraising for Short-Term Disaster Response: The Impact on Earmarking and Performance, SSRN 3705595, version of December 2022. https://ssrn.com/abstract=3705595
• A. Aflaki, A. J. Pedraza-Martinez, same title, Manufacturing & Service Operations Management, 2023. https://doi.org/10.1287/msom.2023.1202
• D. McFadden, Conditional logit analysis of qualitative choice behavior, in Frontiers in Econometrics, 1973.

Motivation

Since 2017, billions of dollars have been raised through the issuance of crypto-assets, many of them tokens: digital claims on a future product or service, issued before the product exists. Malinova and Park, Tokenomics: When Tokens Beat Equity (SSRN 3286825; Management Science, 2023, doi:10.1287/mnsc.2023.4882), ask when such a pre-sale is a better way to finance a venture than the two classical instruments, equity and debt. To answer, they first work out how equity and debt perform in a simple monopoly model in which demand is uncertain when the money is raised. This mission formalizes the debt half of that benchmark (Proposition 2), together with the equity half (Proposition 1). The other three missions of the series treat the optimal token contract (Proposition 3), its comparative statics (Proposition 4) and financing under moral hazard (Proposition 8); all of them compare against the benchmark proved here.

Setting

An entrepreneur must pay a set-up cost $C_0 > 0$ before she learns demand. Afterwards she is a monopolist with constant marginal cost $c$, facing the linear inverse demand

$$p(q) = x - q,$$

where the demand intercept $x$ is uniformly distributed on $(0,\theta)$, with $0 < c < \theta$. Investors require a zero expected return. For a payoff $g$ of the demand realization write

$$\mathsf E_\theta[g] = \frac1\theta \int_0^\theta g(x)\,dx .$$

At demand $x$ the monopolist produces $q^m(x) = \max\{(x-c)/2, 0\}$ and earns the monopoly profit

$$\pi^m(x) = \max\{x-c,\,0\}^2/4 ,$$

that is $(x-c)^2/4$ if $x \ge c$ and $0$ otherwise. The project's net present value is $\mathrm{NPV} = \mathsf E_\theta[\pi^m] - C_0$.

Under equity, investors receive a fraction $\alpha_s$ of profits; break-even is $\alpha_s\,\mathsf E_\theta[\pi^m] = C_0$ (5). Under debt with promised repayment $D \ge 0$, investors receive $\min\{\pi^m(x), D\}$: the full $D$ when the venture is solvent ($x > c + 2\sqrt D$), the whole monopoly profit under the debtor-in-possession arrangement when $c \le x \le c + 2\sqrt D$, and nothing when $x < c$. The entrepreneur keeps $\max\{\pi^m(x) - D, 0\}$. The repayment breaks even when

$$\mathsf E_\theta\big[\min\{\pi^m(x), D\}\big] = C_0. \qquad (7)$$

In Lean these are expect, pim, npv, equityShare, debtInv and debtEnt in the namespace TokenFinance.Debt.

Formalization targets

Goal: Proposition 2 (Debt Financing)

If $\mathrm{NPV} > 0$, then

$$\exists!\, D \ge 0:\ \mathsf E_\theta\big[\min\{\pi^m, D\}\big] = C_0,$$

and every such $D$ satisfies

$$C_0 < D < \frac{(\theta-c)^2}{4}, \qquad \mathsf E_\theta\big[\max\{\pi^m - D, 0\}\big] = \mathrm{NPV}.$$

Uniqueness is asserted among all nonnegative repayments, which implies the paper's uniqueness in $(C_0, (\theta-c)^2/4)$.

Milestones

1. (3): $\mathrm{NPV} = (\theta-c)^3/(12\theta) - C_0$.
2. (32)–(33): with $D = (\theta-c)^2\delta^2/4$ and $0 \le \delta \le 1$, the left side of (7) minus $C_0$ equals the split integral (32) and the cubic $\frac{(\theta-c)^3}{12\theta}(-2\delta^3 + 3\delta^2) - C_0$ of (33).
3. Monotonicity of (33): the cubic is $-C_0$ at $\delta = 0$, equals NPV at $\delta = 1$, has positive derivative and is strictly increasing on $[0,1]$; it has a unique root in $(0,1)$ when NPV $> 0$.
4. (34): at a root $\delta \in (0,1)$, $D = C_0 \cdot \frac{\theta}{\theta-c}\cdot\frac{3}{3-2\delta} > C_0$.
5. (8): at any break-even $D \ge 0$ the entrepreneur's expected payoff is the NPV.
6. Proposition 1 (Equity Financing): if NPV $> 0$, then $\alpha_s = 12\theta C_0/(\theta-c)^3 \in (0,1)$, investors break even and the entrepreneur earns $(1-\alpha_s)\mathsf E_\theta[\pi^m] = \mathrm{NPV}$.

Significance

Propositions 1 and 2 establish that, absent agency problems, equity and debt finance exactly the positive-NPV projects and leave the entrepreneur the entire surplus. This is the benchmark of the paper: Proposition 3 shows that a carefully designed token pre-sale matches it, while naive token contracts (revenue sharing, plain output pre-sales) distort output and fail to finance some profitable projects. Corollary 1 of the paper is the conjunction of Propositions 1–3. The debt repayment characterized here also reappears in the moral-hazard analysis (§IV), where the ranking of debt, tokens and equity depends on the size of $D$ relative to the low-demand state.

On the formal side, the results are proved in the paper with short calculus arguments, and nothing about them is machine-checked. The mission produces a checked model of uniform-demand monopoly financing in which expectations are genuine integrals of realized payoffs, the cubic reduction of the break-even condition, and the uniqueness argument for the repayment. These are the pieces the token missions of the series build on.

Difficulty

The central step is the passage from (7) to the cubic (33). The investors' payoff $\min\{\pi^m(x), D\}$ changes form at $x = c$ and at the solvency threshold $c + 2\sqrt D$, so the expectation must be split at points that depend on $D$ and may fall outside $(0,\theta)$ for large $D$; only for $D \le (\theta-c)^2/4$ does the threshold stay inside the demand range. Uniqueness over all $D \ge 0$ also needs the regime $D \ge (\theta-c)^2/4$, where the investors receive the whole profit and the break-even condition reduces to $\mathrm{NPV} = 0$. A naive argument that solves the cubic in $\delta$ and stops gives uniqueness only inside $[0,1]$.

Formalization scope

All objects are plain functions of real parameters; there is no probability space. Demand enters only through $\mathsf E_\theta[g] = \frac1\theta\int_0^\theta g$, the expectation under $U(0,\theta)$ (open or closed endpoints make no difference). Case distinctions of the paper are encoded with $\max$ and $\min$, so the break-even condition (7) is a single integral of the realized repayment rather than the paper's split integral with $\sqrt D$ limits; the split form is a theorem (milestones 2 and 5). The standing assumptions are $0 < c < \theta$ and $C_0 > 0$; $0 < c$ is the paper's "positive marginal cost" (p. 22) and is kept throughout the series although Proposition 2 itself needs only $c \ge 0$. "All positive NPV projects" is the hypothesis $0 < \mathrm{NPV}$ on the integral-defined NPV.

A trivializing formalization is ruled out: the NPV, the investors' break-even condition and the entrepreneur's payoff are expectations of realized payoffs, never their closed forms, so neither (3) nor the reduction to (33) is true by definition.

The definitions file also declares the token objects of Proposition 3 (the revenue share $t/(t+c)$, the realized token payoffs and condition (16)), identical across the four missions of this series so that they can be merged later; they are not used here. Out of scope: the secondary token market, bankruptcy costs, consumer welfare and the institutional discussion of the paper. Useful infrastructure includes lemmas for integrals of piecewise polynomials on intervals and a reusable "strictly increasing continuous function with a sign change has a unique root" argument.

Selected references

• K. Malinova and A. Park, Tokenomics: When Tokens Beat Equity, SSRN 3286825, version of June 1, 2023. https://ssrn.com/abstract=3286825
• K. Malinova and A. Park, Tokenomics: When Tokens Beat Equity, Management Science, 2023. https://doi.org/10.1287/mnsc.2023.4882

Motivation

A manufacturer can sell directly to consumers and also supply an independent retailer. The retailer reaches consumers for whom its distribution service is more valuable, but its presence can also force the manufacturer to lower direct-channel prices. Jullien, Reisinger and Rey study when the additional sales justify dual distribution under different abilities to personalize retail prices (Jullien, Reisinger and Rey, 2023). This mission isolates their Proposition 4: the manufacturer can personalize its own prices, and the retailer may either personalize or charge one uniform price. The source used here is the authors' March 2022 manuscript; the formal claims follow its Proposition 4 and Online Appendix A.

The question matters for vertical channel design because a retailer's reach and the competition it creates pull industry profit in different directions. The manufacturer and retailer negotiate a wholesale contract before retail pricing. A fixed fee can divide their combined profit, so the distribution decision depends on whether both channels together earn more than the manufacturer's direct channel alone. The model makes that comparison exact for a continuum of consumers rather than treating the retailer's contribution as a general benefit (Jullien, Reisinger and Rey, 2023).

Setting

Consumers have types $x\in[0,X]$, with one unit of consumer mass per unit of $x$. A monopoly manufacturer A offers a direct channel, and retailer B offers a differentiated service. Their consumer values are $u_A(x)=\max\{1-x,0\}$ and $u_B(x)=\max\{v-sx,0\}$. The market parameters satisfy $0<s<v<1$ and $X\ge v/s$. Thus both valuations fall as the consumer index rises, B's valuation falls more slowly, and the market extends beyond the last consumer with positive value for B. The two values cross at $\hat x=(1-v)/(1-s)$, with common value $\hat u=(v-s)/(1-s)$.

The channel contributions measure valuation advantages. A's contribution is $\alpha=\int_0^{\hat x}(u_A(x)-u_B(x))\,dx$; B's is $\beta=\int_{\hat x}^{X}(u_B(x)-u_A(x))\,dx$. They are defined by the integrals. The closed forms in the Online Appendix, $\alpha=(1-v)^2/[2(1-s)]$ and $\beta=(v-s)^2/[2s(1-s)]$, are milestone results, not substitutions into the definitions.

The manufacturer can instead use mono distribution, selling only through A and charging each consumer the full direct-channel value. Its profit is $\Pi_P^m=\int_0^X u_A(x)\,dx=1/2$. Under dual distribution, a two-part tariff has wholesale price $w\ge0$ and a fixed fee. The fee allocates the proceeds between firms; industry profit is the total price paid by consumers. Dual distribution is selected only when its industry profit strictly exceeds $\Pi_P^m$, as specified in the manuscript's footnote 17.

Two retail continuations are relevant. In PP, both firms personalize prices, and the manuscript selects the Bertrand equilibrium where the lower-valued offering prices at its opportunity cost. In PU, B first announces one price $p_B$, and A then tailors its prices to consumer types. B chooses a globally profit-maximizing price after allowing for A's response. These rules determine each consumer's payment and hence industry profit; they are represented directly in the Lean definitions.

Formalization targets

The central target is Proposition 4. It asserts the existence of functions $\beta_{PP}$ and $\beta_{PU}$ of $\alpha$ alone, valid uniformly across all admissible $(v,s,X)$, with

$$\text{dual distribution in PP}\iff\beta>\beta_{PP}(\alpha),\qquad \text{dual distribution in PU}\iff\beta>\beta_{PU}(\alpha),\qquad \beta_{PP}(\alpha)<\beta_{PU}(\alpha).$$

The valuation-space milestones identify the underlying cutoffs $\tilde v(s)=s(2+\sqrt{1-s})/(1+s)$ in PP and $\check v(s)=s[2+\sqrt{(1-s)(2+5s+s^2)/(1+2s)}]/(1+s)$ in PU. They say dual distribution is strictly better exactly when $v$ exceeds the respective cutoff. Other milestones give the mono benchmark, the formulas for $\alpha$ and $\beta$, the existence of the two contribution thresholds, and the strict ordering $\tilde v(s)<\check v(s)$ (Jullien, Reisinger and Rey, 2023, Proposition 4 and Online Appendix A).

Significance

Proposition 4 turns a distribution choice involving wholesale and retail prices into a comparison of two channel contributions. It identifies precisely how large B's contribution must be to make a second channel profitable, and it says that B's ability to personalize prices lowers that required contribution. A price policy restriction on B therefore changes the region of market parameters in which the retailer is brought into the channel. The strict threshold statement also distinguishes an actual gain from a tie with mono distribution.

The result is proved in the authors' manuscript, with detailed arguments in Online Appendix A. This mission asks for a machine-checked version of the market definitions, its integral and cutoff identities, and the passage from $(v,s)$ to $(\alpha,\beta)$. The proposed Lean theorem files contain open proof obligations; compilation of their statements does not supply those proofs. A completed development would give reusable formal definitions of the consumer outcomes and a checked statement of the channel comparison.

Difficulty

The industry profit changes formula as the wholesale price changes which consumers can be served by B. In PP, the profit derivative has different expressions on either side of $w=v-s$, and the curvature of one region changes with $s$. In PU, B's uniform price can leave some consumers buying directly from A both before and after B's customer interval. A single interior first-order calculation therefore does not settle the global distribution choice. The contribution thresholds add another step: each cutoff in $(v,s)$ must correspond to a threshold depending only on $\alpha$, and the two resulting thresholds must retain a strict order along every admissible iso-$\alpha$ curve (Jullien, Reisinger and Rey, 2023, Online Appendix A).

Formalization scope

Lean uses real numbers for $v,s,X,w,p_B$, interval integrals against Lebesgue measure for profits and contributions, and the Lebesgue volume of B's buyer set for its PU demand. The standing assumptions are exactly $0<s<v<1$ and $v/s\le X$. Retail prices in B's maximization range over all real numbers; wholesale prices satisfy $w\ge0$. The continuation fixes an assignment of indifferent consumers. Positive-valuation tie boundaries have measure zero; at $w=0$, an interval of zero-valuation consumers pays zero in PP. Consumers with $u_B(x)=0$ are assigned to A in PU and are excluded from B's demand. If several uniform prices maximize B's profit, a strict industry gain at one maximizing price suffices in the dual-distribution predicate.

The setting defines industry profits from consumer payments and defines dual distribution by a strict profit comparison. It never defines them from $\tilde v$, $\check v$, or the desired threshold functions. The real-valued integrals are well behaved here because the consumer interval is bounded and the integrands are piecewise affine. The cutoff expressions use positive denominators under the standing assumptions. The PU price maximum is global; neither a stationary point nor the first market configuration is built into the definition.

A complete proof needs interval integration of piecewise affine functions, global optimization across the PP and PU price regions, and a comparison of the induced contribution-space thresholds. The integration and market-outcome lemmas can be reused for related channel games. Contributions establishing the stated milestones, or reusable lemmas about these bounded price regions, fit the mission's scope.

Selected references

• Bruno Jullien, Markus Reisinger and Patrick Rey, Personalized Pricing and Distribution Strategies, Management Science, 2023. DOI 10.1287/mnsc.2022.4437. Formalization source: authors' manuscript of March 2022, PDF SHA-256 25a6c84ac0c48c6720f6a9e1f9b1f1ec516412c31dac044ac84c1d4c72dfc253, Proposition 4 and Online Appendix A.

Motivation

Social platforms show news articles to their users without sending them to the publisher's site. Publishers argue that this diverts readers and advertising revenue, and so weakens their incentive to invest in journalism. Several regulators have responded by requiring dominant platforms to negotiate payments with news publishers: France transposed the EU neighbouring right for press publishers in 2019, and Australia adopted the News Media Bargaining Code in 2021. Whether such negotiated payments raise or lower the quality of news is not obvious, because the payment and the publisher's traffic both depend on the quality the publisher chooses.

de Cornière and Sarvary (TSE Working Paper n° 1152, August 2021; published in Management Science, 2023, doi:10.1287/mnsc.2022.4341) study a model in which a platform bundles a publisher's content with user-generated content. In their baseline (§3–§4) the platform bundles unilaterally; this is the subject of the companion mission Social Media and News: Content Bundling and News Quality I. Section 6 replaces unilateral bundling by a negotiated agreement, and Proposition 5 compares the resulting news quality with both the no-bundling benchmark and unilateral bundling. This mission formalizes Proposition 5.

Setting

Consumers. A consumer has one unit of time. She spends $T_1$ on the publisher's site and $T_0=1-T_1$ on the platform. On the platform a share $\lambda$ of what she sees is news and $1-\lambda$ is user-generated content, so she consumes $x_N=T_1+\lambda T_0$ units of news and $x_U=(1-\lambda)T_0$ units of other content, with utility

$$U(x_U,x_N)=x_U+(1+q)x_N-\frac{x_N^2}{2},$$

where $q$ is the quality of the publisher's news.

Baseline game (unilateral bundling). The publisher chooses $q\in[0,1]$ at cost $cq^2/2$; the platform chooses $\lambda\in[0,\Lambda]$; the consumer chooses $T_1\in[0,1]$. The platform earns $R_0=(1-\lambda+\lambda\varphi_0)T_0$ and the publisher earns $R_1=\beta T_1+\varphi_1\lambda T_0$. The standing assumptions (Table 1) are $\varphi_0,\varphi_1\in(0,1)$, $\beta>\varphi_1$, $c>2\beta$, $\Lambda\in(0,1/2)$. The benchmark is the same game with $\Lambda=0$. The unilateral threshold is

$$c^\dagger=\frac{\beta+\varphi_1(1-2\Lambda)}{2\Lambda(1-\Lambda)}.$$

Negotiated game (§6). The publisher chooses $q$. Publisher and platform then agree, by Nash bargaining with equal bargaining power, on a lump-sum payment $F$ to the publisher. The platform chooses $\lambda\le\Lambda$ and keeps all advertising revenue ($\varphi_0=1$, $\varphi_1=0$). Finally the consumer allocates her time. With an agreement the publisher receives $\beta T_1+F$ and the platform $T_0-F$; if bargaining fails the outcome is the benchmark, with payoffs $\beta q$ and $1-q$. The fee maximizes the Nash product

$$\bigl(\beta T_1+F-\beta q\bigr)\bigl(T_0-F-(1-q)\bigr).$$

Section 6 assumes $1/3<\beta\le1$ and keeps $c>2\beta$ and $\Lambda\in(0,1/2)$.

In each game a subgame-perfect equilibrium requires best responses after every history: the consumer at every $(q,\lambda)$, the platform at every $q$, the fee at every $q$, and the publisher's quality optimal over $[0,1]$. In the negotiated game, a platform that is indifferent between several values of $\lambda$ chooses the smallest one (p. 19). The equilibrium qualities are written $\hat q$ (benchmark), $q^*$ (unilateral) and $\tilde q$ (negotiated).

Formalization targets

Goal: Proposition 5

Under $1/3<\beta\le1$, $\varphi_0,\varphi_1\in(0,1)$, $\varphi_1<\beta$, $c>2\beta$, $\Lambda\in(0,1/2)$, all three games have subgame-perfect equilibria, and for any equilibria of the three games

$$\beta<1\ \Longrightarrow\ \bigl(\hat q<\tilde q\iff c>\beta/\Lambda\bigr),\qquad c\neq c^\dagger\ \Longrightarrow\ \bigl(q^*<\tilde q\iff c>c^\dagger\bigr).$$

Milestones

The negotiated equilibrium is solved by backward induction, as in §6:

• the platform's choice $\lambda=\min\{q,\Lambda\}$ (p. 19);
• the fees $F_1(q)=q(1+\beta)/2$ for $q\le\Lambda$, display (4), and $F_2(q)=(1-q)(1+\beta)\Lambda/(2(1-\Lambda))$ for $q>\Lambda$, display (6);
• the publisher's stage-1 profit, display (7);
• $q_1(c)<1$ and $q_2(c)<q_1(c)$, where $q_1(c)=(1+\beta)/(2c)$ and $q_2(c)=(\beta(2-\Lambda)-\Lambda)/(2(1-\Lambda)c)$ (proof of Lemma 5);
• Lemma 5: $\tilde q=q_2(c)$, $\Lambda$ or $q_1(c)$ according as $c$ is below, inside or above $\bigl[\tfrac{\beta(2-\Lambda)-\Lambda}{2(1-\Lambda)\Lambda},\tfrac{1+\beta}{2\Lambda}\bigr]$.

The comparison uses Lemma 1 ($\hat q=\beta/c$), Lemma 4 ($q^*=q_L(c)=\varphi_1/c$ above $c^\dagger$, $q_H(c)=(\beta-\Lambda\varphi_1)/(c(1-\Lambda))$ below), and the inequality $q_2(c)<\beta/c<q_1(c)$ of the proof of Proposition 5.

Significance

Proposition 5 reverses the conclusion of the unilateral analysis. Under unilateral bundling (Proposition 1, companion mission) quality rises only when quality is cheap ($c<c^\dagger$). Under a negotiated agreement quality rises over unilateral bundling exactly when quality is costly ($c>c^\dagger$), and over the benchmark exactly when $c>\beta/\Lambda$. A bargaining mandate therefore helps news quality for publishers whose content is mostly consumed through the platform, which is the case that motivates the Australian and French policies.

The result is proved in the paper; the proof of part 2 is a one-sentence case sketch over the position of $c^\dagger$ relative to the two thresholds of Lemma 5. No machine-checked version exists. A formal proof checks the case analysis, including the knife-edge cases $c=c^\dagger$ and $\beta=1$, which the printed statement does not treat, and produces a reusable formal model of Nash bargaining inside a multi-stage game.

Difficulty

The closed forms are elementary; the content lies in the equilibrium objects. Each equilibrium concept quantifies over strategies at every history, so every closed form must be derived, not assumed: the consumer's split from utility maximization, the platform's share from the revenue comparison and the tie-break, the fee from maximizing the Nash product, and the quality from a piecewise objective whose two pieces meet at $q=\Lambda$. The comparison in part 2 then crosses two different games, whose thresholds $c^\dagger$ and $\bigl[\tfrac{\beta(2-\Lambda)-\Lambda}{2(1-\Lambda)\Lambda},\tfrac{1+\beta}{2\Lambda}\bigr]$ can be ordered in several ways, and the equivalence must hold in every ordering. Reading the closed forms off the paper and comparing them does not prove anything about the games.

Formalization scope

All objects are real-valued. Quality ranges over $[0,1]$, since demand for news equals $q$ and the paper notes the profit expression is valid only for $q\le1$. A strategy profile is a record of functions: the consumer's time $T_1(q,\lambda)$, the platform's share $\lambda(q)$, in the negotiated game the fee $F(q)$, and a quality. The fee maximizes the Nash product over all $F\in\mathbb R$; the agreement and disagreement payoffs are those printed on p. 19. The negotiated platform minimizes $\lambda$ among its maximizers, as printed. The benchmark is the baseline game at $\Lambda=0$, and the unilateral game keeps Table 1's $\varphi_0,\varphi_1$; footnote 16's $\varphi_0=1$, $\varphi_1=0$ apply to the negotiated game only.

Two hypotheses are added to the printed statement, both disclosed in the goal's statement:

1. part 1 is posed for $\beta<1$, because at $\beta=1$ the negotiated quality equals the benchmark quality $\beta/c$ whenever $c>(1+\beta)/(2\Lambda)$;
2. part 2 is posed for $c\ne c^\dagger$, because at $c=c^\dagger$ the unilateral game has two equilibrium qualities and the negotiated quality lies strictly between them.

Trivializing formalizations are ruled out. Equilibrium strategies are never given by their closed forms. Best responses are required after every history, not only on the path. The fee is never defined as $F_1$ or $F_2$. The benchmark is an equilibrium of the game at $\Lambda=0$, not the number $\beta/c$. The goal and Lemma 5 assert existence of equilibria, so the "for every equilibrium" clauses are not vacuous.

The definitions (NewsBundling.Negotiated.Setting) import the baseline game from the shared module NewsBundling.Unilateral.Setting and define the negotiated game. A proof needs elementary real analysis: maxima of concave quadratics, piecewise functions on $[0,1]$, and the existence of maximizers. Proofs of any milestone are welcome, as are proofs of Lemmas 1 and 4 shared with the companion mission.

Selected references

• A. de Cornière and M. Sarvary, Social Media and News: Content Bundling and News Quality, Toulouse School of Economics Working Paper n° 1152, August 2021 (the version this mission cites); journal version below.
• A. de Cornière and M. Sarvary, Social Media and News: Content Bundling and News Quality, Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4341
• J. F. Nash, The Bargaining Problem, Econometrica 18(2), 1950. https://doi.org/10.2307/1907266

Motivation

Firms that customize products, especially in business-to-business and service markets, need to learn what each customer wants before designing for that customer. Liang Guo's paper The Voice of Customers in Customization (SSRN 3994319; published in Management Science, DOI 10.1287/mnsc.2021.04025) compares two ways a seller can learn a customer's preference. Under A-Learning the customer describes its preference and the seller designs the product. Under O-Learning the customer proposes the design itself and the seller decides whether to accept it. The customer's preference is private, and the price is bargained after the product has been made, so a customer has a reason to misrepresent itself in either case: a customer believed to value quality less is charged less.

This mission formalizes the paper's characterization of when O-Learning reveals preferences without distortion: each customer type requests exactly the design it would request if its preference were public. The paper calls this the cheap-signaling equilibrium. A companion mission in this series formalizes the analogous result for A-Learning (Proposition 1), and another shows that O-Learning has no separating equilibrium at all below the threshold found here.

Setting

A seller faces buyers whose quality preference is $\theta\in\{\theta_H,\theta_L\}$ with $\theta_H>\theta_L>0$. Each buyer knows its own $\theta$. The seller holds the prior that a fraction $\alpha\in(0,1)$ of buyers has $\theta_H$. A product has a quality $q\ge 0$. Producing it costs $kq^2$ and selling it costs $sq^2$, with $k,s>0$. The selling cost is incurred before the price is set. In the price stage either party makes a take-it-or-leave-it offer: the seller with probability $\gamma\in(0,1)$, charging $\hat\theta q$ where $\hat\theta$ is its belief about the buyer, and the buyer with probability $1-\gamma$, offering $kq^2$.

The O-Learning game has three stages.

1. Each buyer submits a quality request $q(\theta)\ge 0$.
2. The seller, holding a posterior belief $\hat\theta(q)$, accepts or rejects the request. It accepts if and only if its expected profit is nonnegative:

$$\gamma(\hat\theta q-kq^2)-sq^2\ge 0.$$

3. The price is set as above. A rejected request ends the game with payoff $0$ to both parties.

A buyer of true preference $\theta$ whose request $q$ is accepted under belief $\hat\theta$ expects

$$\mu(q,\theta,\hat\theta)=\gamma\max\{\theta q-\hat\theta q,0\}+(1-\gamma)\max\{\theta q-kq^2,0\}.\tag{9}$$

A separating equilibrium consists of distinct requests $q_H\ne q_L$ and a belief function $\hat\theta(\cdot)$ satisfying three conditions. Beliefs are consistent on the equilibrium path: $\hat\theta(q_H)=\theta_H$ and $\hat\theta(q_L)=\theta_L$. Beliefs off the path are arbitrary. No type gains by deviating to any other request $q\ge 0$.

If the preference were public, the buyer would choose $q$ to maximize $\mu(q,\theta,\theta)$ subject to acceptance. The solution is the first-best request

$$q^*(\theta)=\min\Big\{\frac{\gamma\theta}{s+\gamma k},\ \frac{\theta}{2k}\Big\}.$$

The thresholds are

$$\Lambda_{H1}=\frac{\gamma(s+k)}{(1-\gamma)s},\qquad \Lambda_{H2}=\frac{1+\gamma}{1-\gamma},\qquad \Lambda_L=\frac{s}{\gamma k},\qquad \Lambda=\max\{\min\{\Lambda_{H1},\Lambda_{H2}\},\Lambda_L\}.$$

Formalization targets

Goal: Proposition 3 (p. 17)

The requests $q^O_H=q^*(\theta_H)$, $q^O_L=q^*(\theta_L)$ form a separating equilibrium for some belief function if and only if

$$\frac{\theta_H}{\theta_L}\ge\Lambda.$$

When this holds, the equilibrium is supported by the out-of-equilibrium belief $\hat\theta(q)=\theta_L$ if $\gamma\le s/k$, and by $\hat\theta(q)=\theta_H$ if $\gamma\ge s/k$.

Milestones

In attack order:

1. Seller acceptance (§3.3, p. 16). For $q\ge 0$, the seller accepts a request iff $q\le\gamma\hat\theta/(s+\gamma k)$.
2. The first-best request solves (10) (§3.3, p. 16). $q^*(\theta)$ is the unique maximizer of $\mu(q,\theta,\theta)$ over the acceptable requests.
3. The case form of $q^*$ (Appendix, Proof of Proposition 3, p. 28). $q^*(\theta)=\gamma\theta/(s+\gamma k)$ if $\gamma\le s/k$, and $q^*(\theta)=\theta/(2k)$ if $\gamma\ge s/k$.
4. Necessity of (11)–(12) (p. 17). If $(q^O_H,q^O_L)$ is a separating equilibrium under any beliefs, then

$$\mu(q^*(\theta_H),\theta_H,\theta_H)\ge\mu(q^*(\theta_L),\theta_H,\theta_L)\quad\text{and}\quad\mu(q^*(\theta_L),\theta_L,\theta_L)\ge\mu(q^*(\theta_H),\theta_L,\theta_H).$$

5. $\gamma\le s/k$ (p. 28). $\mathrm{IC}'_H\iff\theta_H/\theta_L\ge\Lambda_{H1}$, and $\mathrm{IC}'_L\iff\theta_H/\theta_L\ge\Lambda_L$.
6. $\gamma\ge s/k$ (p. 28). $\mathrm{IC}'_H\iff\theta_H/\theta_L\ge\Lambda_{H2}$, and $\mathrm{IC}'_L$ holds strictly.
7. $\Lambda_{H1}\le\Lambda_{H2}\iff\gamma\le s/k$ (p. 28).

Significance

Proposition 3 locates the boundary of truthful self-design. Above $\Lambda$, a buyer who designs its own product can both reveal its type and obtain its full-information design. The seller then learns preferences without distorting quality. Below $\Lambda$, the companion mission shows that no separating equilibrium exists at all. The paper builds on this threshold. Proposition 7 compares $\Lambda$ with the A-Learning threshold $\Delta$ to decide which learning mode supports customization over a wider range of preferences. Proposition 8 compares the seller's and buyers' payoffs in the two separating equilibria and shows that the seller prefers to design while the buyers prefer to self-design.

The result is proved in the paper's Appendix. As far as the series' searches show, it has not been machine-checked. This mission poses a formal version of the O-Learning game, its equilibrium notion, and the deviation arguments the paper sketches in a sentence each.

Difficulty

The incentive constraints are polynomial inequalities in the ratio $\theta_H/\theta_L$ once $q^*$ is substituted. The work is elsewhere.

First, the equilibrium quantifies over every request $q\ge 0$, not only over mimicking the other type. A deviation interacts with the belief the seller holds at that request and with the acceptance rule, and the payoff (9) has two kinks. The proof shows that the two stated off-path beliefs deter every deviation. Each regime needs a different belief: the low-type belief works when the acceptance constraint binds at the first-best, and the high-type belief works when it does not.

Second, the "only if" direction has to hold for every belief function. The argument must show that mimicking the other type's first-best request is always accepted, whatever the seller believes elsewhere.

Third, the paper's proof writes the payoffs without the $\max\{\cdot,0\}$ terms. Those identities hold only on part of the domain, and the formal argument has to track where.

Formalization scope

The O-Learning objects live in the namespace CustomerVoice.OLearn, in a single definition file. The model is a structure with real fields $\theta_H,\theta_L,\alpha,\gamma,k,s$. Buyer types use the shared CustomerVoice.ALearn.BType, an inductive type with constructors H and L. The standing assumptions $\theta_H>\theta_L>0$, $\alpha,\gamma\in(0,1)$ and $k,s>0$ are a hypothesis of every theorem. $\alpha$ does not enter this mission but is kept as printed. No other hypothesis is added.

Commitments of the formalization:

• Qualities, requests and deviations are real numbers $q\ge 0$.
• The payoff $\mu$ keeps both $\max\{\cdot,0\}$ terms.
• The seller accepts at indifference, as the paper prints its acceptance rule.
• A rejected request pays $0$.
• A belief function is any total map from requests to the two types. It is pinned only on the equilibrium path.
• The price stage is in reduced form, entering only through (9) and the acceptance inequality.
• Optimality in (10) is stated as attainment of the maximum (IsMaxOn on the acceptable interval) together with uniqueness.

Ruled-out trivializations. Acceptance is the printed inequality, not the threshold $q\le\gamma\hat\theta/(s+\gamma k)$, which is milestone 1. The requests are $q^*(\theta)$, and milestone 2 proves that $q^*(\theta)$ solves (10). The equilibrium is a perfect Bayesian equilibrium against all deviations, not the conjunction of (11) and (12). The "only if" direction quantifies over all belief functions. $\Lambda$ is the printed expression, not an infimum of ratios at which an equilibrium exists.

The development needs only elementary real algebra and one-variable concave quadratics from Mathlib. The equilibrium definition is a template for the other O-Learning mission of the series. Proofs of any milestone, and alternative arguments for the deviation step, are welcome.

The source is the SSRN author version (SSRN 3994319, version of 2023-11-29). All page and display numbers refer to it, and the proofs behind the milestones are in its Appendix.

Selected references

• Liang Guo, The Voice of Customers in Customization, SSRN working paper 3994319, version of 2023-11-29. https://ssrn.com/abstract=3994319
• Liang Guo, The Voice of Customers in Customization, Management Science. https://doi.org/10.1287/mnsc.2021.04025
• Vincent P. Crawford and Joel Sobel, Strategic Information Transmission, Econometrica 50(6), 1982. https://doi.org/10.2307/1913390

Why a firm would hand customer data to a rival

Large platforms that also sell their own products (Amazon, JD.com, app stores) hold detailed data on consumers and sometimes share part of it with the independent sellers they compete with. The usual view in the personalized-pricing literature is that information is a competitive weapon: a firm that knows more about consumers can price discriminate and capture more surplus, so giving that knowledge to a rival should only hurt. Thisse and Vives (American Economic Review, 1988) showed that when both firms on a Hotelling line can price every consumer individually, competition intensifies and the profits of the informed firm fall.

Choe, Cong and Wang (Monash Discussion Paper 2021-10, revised October 20, 2022; published in Management Science, 2024, doi:10.1287/mnsc.2023.4689) show that this is not the whole picture: an informed firm can strictly gain by sharing data on a well-chosen segment of consumers with an uninformed rival, and the rival gains too. This mission formalizes that result, Proposition 1 of the paper, together with the steps its proof is built from.

Setting

Consumers are located on the interval $[0,1]$. A consumer's location has cumulative distribution function $F$ with density $f>0$, continuous on $[0,1]$, and the hazard rate

$$h(x)=\frac{f(x)}{1-F(x)}$$

is strictly increasing on $[0,1)$ (the monotone hazard rate condition). Firm 1 sits at $0$ and knows every consumer's location; firm 2 sits at $1$ and knows none. A consumer at $x$ who buys from firm $i$ at price $p_i$ pays $p_i$ plus a transport cost equal to her distance to firm $i$; production is costless and the market is fully covered.

Benchmark. Without data sharing, firm 2 sets one uniform price $p_2$ and firm 1 undercuts it consumer by consumer, so firm 2 serves $[z,1]$ with $p_2=2z-1$ and earns $(2z-1)(1-F(z))$. The first-order condition gives the benchmark marginal consumer $z^N$ and price $p^N_2$:

$$z^N=\frac12+\frac1{h(z^N)},\qquad p^N_2=\frac2{h(z^N)}=2z^N-1.$$

The benchmark profits are $\pi^N_1=\int_0^{z^N}(p^N_2+1-2x)\,dF(x)$ and $\pi^N_2=p^N_2(1-F(z^N))$.

Data sharing on $[a,b]$. Firm 1 gives firm 2 the locations of the consumers in $[a,b]$. Firm 2 then chooses a uniform price for the consumers it does not know and personalized prices on $[a,b]$. Its uniform price either serves only $[b,1]$, at price $2b-1$ and profit $\pi_{21}(b)=(2b-1)(1-F(b))$, or serves $[z',a]\cup[b,1]$ for some $z'\le a$, with best profit

$$\pi_{22}(a,b)=\max_{z'\in[0,a]}(2z'-1)\bigl(1-F(b)+F(a)-F(z')\bigr).$$

When firm 2 chooses the first option, the profits are

$$\pi_1(a,b)=\int_0^a\bigl((2b-1)+(1-2x)\bigr)\,dF(x),\qquad \pi_2(a,b)=\int_a^b(2x-1)\,dF(x)+\pi_{21}(b).$$

Firm 2's incentive constraint (IC) is $\pi_{21}(b)\ge\pi_{22}(a,b)$.

Formalization targets

Goal: Proposition 1

For every distribution $(F,f)$ satisfying the conditions above:

$$\pi_1(z^N,b)>\pi^N_1\quad\text{and}\quad\pi_2(z^N,b)>\pi^N_2\qquad\text{for all } b\in(z^N,1],$$

and there exists $b'\in(z^N,1)$ with

$$\pi_{21}(b')>\pi_{22}(z^N,b'),$$

so sharing data on $[z^N,b']$ satisfies firm 2's incentive constraint and makes both firms strictly better off than without sharing.

Milestones

1. Eq. (1): $z^N$ exists and is unique in $(1/2,1)$.
2. $z^N$ is the unique maximizer of $\pi_{21}$ on $[0,1]$.
3. Lemma 2: if firm 2's uniform price serves $[z',a]\cup[b,1]$ with $z'$ solving the first-order condition (5), then $z'<z^N$, firm 2's price falls below $p^N_2$, and firm 1 earns less than $\pi^N_1$.
4. $\pi_1(z^N,b)-\pi^N_1=2(b-z^N)F(z^N)$.
5. $\pi_2(z^N,b)-\pi^N_2>\int_b^1(2b-2z^N)\,dF(x)>0$ for $z^N<b<1$.
6. With $\hat\pi_{22}(b)=\pi_{22}(z^N,b)$: $\pi_{21}(z^N)=\hat\pi_{22}(z^N)$ and $\pi_{21}(1)<\hat\pi_{22}(1)$.
7. $\hat\pi_{22}(b)<\hat\pi_{22}(z^N)$ for every $b\in(z^N,1]$.

Significance

The result reverses the standard intuition that a firm's informational advantage should be guarded. Firm 1 shares data only on firm 2's own customer base $[z^N,b']$, which it could not win anyway, and keeps the data on the most loyal consumers $[b',1]$ private. Firm 2 then prefers to extract surplus from those loyal consumers with a high uniform price $2b'-1>p^N_2$, and firm 1 raises its personalized prices accordingly. Competition is softened without firm 1 conceding market share. The statement holds for every monotone-hazard-rate distribution, not for a parametric family, which is what makes it a structural claim rather than a numerical example. It underlies the paper's analysis of optimal data sharing (Section 3.3) and its welfare conclusion that consumer surplus falls (Proposition 3), and it is the benchmark against which the paper's extensions (sales fees, data sale, entry) are compared.

The paper's proof is complete for the first part. For the existence of $b'$, the written argument infers a negative derivative of $\hat\pi_{22}$ at $z^N$ from a strict inequality, which does not follow as written and presupposes differentiability of a maximum value function; the statement itself is true. A machine-checked proof closes that step. To the best of current knowledge none of these results has been formalized.

Difficulty

The two profit comparisons in the first part are integral identities and estimates that only need the fundamental theorem of calculus and $f>0$. The existence of $b'$ is the hard part. Both $\pi_{21}(b)$ and $\hat\pi_{22}(b)$ start from the same value at $b=z^N$, and $\pi_{21}$ has zero derivative there, so the comparison is decided at first order by how fast $\hat\pi_{22}$ decreases. But $\hat\pi_{22}$ is a maximum over $z'\in[0,z^N]$ whose maximizer moves with $b$ and need not be unique, so $\hat\pi_{22}$ is not known to be differentiable, and the strict decrease of milestone 7 alone does not give a linear rate. A proof has to bound $\hat\pi_{22}(b)$ from above by $\pi_{21}(z^N)$ minus a term proportional to $b-z^N$, uniformly over the possible maximizers, and compare it with the second-order behaviour of $\pi_{21}$ near its maximum. Existence of $z^N$ similarly needs the hazard rate to blow up at $1$, which uses $F(1)=1$ and $f(1)>0$.

Formalization scope

All objects are real-valued functions on $\mathbb R$ with hypotheses only on $[0,1]$. The distribution is the structure MHRDist F f: $F(0)=0$, $F(1)=1$, $F$ has derivative $f$ within $[0,1]$ at every point of $[0,1]$, $f$ is continuous and strictly positive on $[0,1]$, and $h=f/(1-F)$ is strictly increasing on $[0,1)$. The paper's "smooth" is read as continuously differentiable, a weaker assumption, so the formal theorems are at least as strong as the paper's. Every $dF$ integral is an interval integral of the integrand times $f$, always with increasing bounds. $z^N$ enters as a number zN with the hypothesis IsZN F f zN ($z^N\in(1/2,1)$ and $z^N=1/2+1/h(z^N)$); milestone 1 shows exactly one such number exists, so no statement is vacuous. $\pi_{22}$ is defined as the supremum of the profit over $z'\in[0,a]$ (a maximum, since the set is compact and the function continuous), never through the first-order condition (5); the incentive inequality in the goal is strict, as in the paper's proof.

A trivializing formalization is ruled out: $\pi_{22}$ is the actual maximum, not a free parameter or the value at a stationary point, and $z^N$ is pinned by Eq. (1), whose solution is shown to exist.

A complete development needs the fundamental theorem of calculus for interval integrals, compactness and the intermediate value theorem on $[0,1]$, and a uniform first-order estimate on a parametric maximum. The lemmas on hazard rates and on the maximizer of $(2z-1)(1-F(z))$ are reusable for other Hotelling and pricing models with monotone-hazard-rate demand. Contributions are welcome on any milestone, and alternative proofs of the existence of $b'$ are of particular interest.

Selected references

• Chongwoo Choe, Jiajia Cong, Chengsi Wang, Softening Competition through Unilateral Sharing of Customer Data, Monash University Department of Economics Discussion Paper 2021-10, revised October 20, 2022 (the version formalized here; all page and equation numbers refer to it); published in Management Science, 2024. https://doi.org/10.1287/mnsc.2023.4689
• Jacques-François Thisse, Xavier Vives, On the Strategic Choice of Spatial Price Policy, American Economic Review 78(1), 1988, 127–137.
• Greg Shaffer, Z. John Zhang, Competitive One-to-One Promotions, Management Science 48(9), 2002, 1143–1160.