All missions

Why engagement is not utility

Online platforms rank content by what they can measure: clicks, watch time, session length. The implicit justification is revealed preference: if users stay longer, they must like what they see. Kleinberg, Mullainathan and Raghavan (arXiv:2202.11776v3, Management Science 2023, doi:10.1287/mnsc.2022.03683) question this justification with a model of a user whose preferences are internally inconsistent, in the tradition of dual-process models of choice. Within the model, an engagement-maximizing platform can serve content that lowers the user's welfare, and the paper asks exactly when this happens. This mission formalizes its first characterization result, Theorem 4.1 (p. 16).

The model

A user consumes a stream of items $t=0,1,2,\dots$ and is a composite of two agents (§2.1, pp. 5–8).

• System 2 is forward-looking. Each consumed item gives it a random value with mean $\bar v$, while leaving the platform gives an outside option $W$ per step. After each item, system 2 still wants to continue with probability $q$, and otherwise it is "done" for the rest of the session.
• System 1 is impulsive. With probability $p$ it is hooked by the current item and consumes the next one without consulting system 2.

A content distribution is the triple $\omega=(p,q,\bar v)$, read as moreishness $p$, span $q$ and value $\bar v$. The parameter space is (p. 15)

$$\Omega=[0,1)\times[0,1)\times\mathbb R_+ .$$

The content a platform can offer forms a content manifold $\mathcal M\subseteq\Omega$.

Summing system 2's utility over the two phases of a session (before and after system 2 is done) gives, when the user participates,

$$g_S(\omega)=\frac{\bar v-W}{1-q}-\frac{pW}{1-p},\qquad g_T(\omega)=\frac{1}{1-q}+\frac{p}{1-p}$$

(p. 16). Here $g_S$ is system 2's expected utility $\mathbb E[S]=\max(g_S,0)$ (equation (1), p. 7) and $g_T$ is the expected session length $\mathbb E[T]$ (equation (2), p. 8). The user stays away when $g_S(\omega)<0$, and then $T=0$.

Write $\omega_S=(p_S,q_S,\bar v_S)$ and $\omega_T=(p_T,q_T,\bar v_T)$ for the utility and engagement maximizers (p. 16):

$$\omega_S\in\arg\max_{\omega\in\mathcal M} g_S(\omega)\quad(3),\qquad \omega_T\in\arg\max_{\omega\in\mathcal M,\ g_S(\omega)\ge0} g_T(\omega)\quad(4).$$

The platform observes only engagement, so it serves $\omega_T$, and only among content the user is willing to consume. The paper assumes that $\mathcal M$ contains at least one point with $g_S>0$.

Formalization targets

Goal: Theorem 4.1 (p. 16)

Suppose $\omega_S\neq\omega_T$ and the disagreement is strict, $g_S(\omega_S)>g_S(\omega_T)$ and $g_T(\omega_T)>g_T(\omega_S)$. Then

$$p_T>p_S\qquad\text{or}\qquad\bigl(q_T>q_S\ \text{ and }\ \bar v_T<\bar v_S\bigr).$$

Milestones (the two steps of the printed proof)

1. Proof of Theorem 4.1, p. 16: for $\omega_S,\omega_T\in\Omega$, if $p_T\le p_S$ and $g_T(\omega_T)>g_T(\omega_S)$, then $q_T>q_S$.
2. Proof of Theorem 4.1, p. 17: for $\omega_S,\omega_T\in\Omega$ and $W>0$, if $p_T\le p_S$, $q_T>q_S$, $g_S(\omega_S)>g_S(\omega_T)$ and $g_S(\omega_T)\ge0$, then $\bar v_T<\bar v_S$.

A supporting item, not a milestone: for $\omega\in\Omega$ and $W>0$, $g_S(\omega)\ge0$ implies $\bar v\ge W$.

Significance

The theorem names the only two ways an engagement maximizer can do worse for the user than a utility maximizer. Either the content is more habit-forming (it raises system 1's grip), or it keeps system 2 interested for longer while delivering less per item, as when a long series of instructional videos replaces a short one. A platform that wants to diagnose misalignment therefore needs to look at moreishness and at the span–value trade-off, and at nothing else. The companion result of the paper (Theorem 4.2, a separate mission) turns this around: when moreishness is small and value nearly constant across $\mathcal M$, engagement maximization is near-optimal.

The result is proved in the paper by a few lines of algebra. No machine-checked version of it was found on Prove2Me or in Mathlib. Formalizing it pins down what the printed proof leaves implicit: the step from $\frac{\bar v_T-W}{1-q_T}$ to $\frac{\bar v_T-W}{1-q_S}$ on p. 17 is valid only because $\bar v_T\ge W$, which follows from the participation constraint of (4). The mission also provides a reusable encoding of the paper's model (Ω, $g_S$, $g_T$, (3), (4)).

Difficulty

The mathematics is elementary. What makes the statement delicate is its hypotheses. If the participation constraint $g_S(\omega_T)\ge0$ is dropped from (4) together with the standing assumption that $\mathcal M$ contains a point with $g_S>0$, the theorem is false. With $W=1$ and $\mathcal M=\{(0,0,\tfrac12),(0,\tfrac12,\tfrac12)\}$, the first point maximizes $g_S$ and the second maximizes $g_T$, the disagreement is strict, yet $p_T=p_S$ and $\bar v_T=\bar v_S$. The obvious reading of the second step, "a larger $q$ shrinks the denominator", fails when $\bar v_T<W$, because the numerator is then negative.

Formalization scope

• A content distribution is a structure Params with three real fields p, q, v (for $\bar v$). Membership in $\Omega$ is the predicate InOmega: $0\le p<1$, $0\le q<1$, $0\le\bar v$. Every theorem requires it of the points it uses, because Lean's division gives $x/0=0$ and $g_S$, $g_T$ would take junk values at $p=1$ or $q=1$.
• The outside option $W$ is a real parameter with the added hypothesis $W>0$. The paper sets $W=1$ "without loss of generality" (p. 5) but keeps $W$ in its formulas, and the proof uses $W>0$.
• (3) and (4) are the predicates IsUtilityMaximizer and IsEngagementMaximizer, built from Mathlib's IsMaxOn. $\omega_S$ maximizes over all of $\mathcal M$; $\omega_T$ lies in $\mathcal M$, satisfies $g_S(\omega_T)\ge0$, and maximizes $g_T$ over $\{\omega\in\mathcal M:g_S(\omega)\ge0\}$. The theorem holds for every pair of maximizers, which is stronger than the paper's "ties broken consistently" and needs no tie-breaking rule.
• The paper's closedness of $\mathcal M$ only guarantees that the maximizers exist. Since the theorem assumes them, closedness is not required.
• The standing assumption "$\mathcal M$ contains at least one point with strictly positive $\mathbb E[S]$" is kept as a hypothesis, as printed, although the proof does not need it once $g_S(\omega_T)\ge0$ is part of (4).
• "One of the following conditions must hold" is an inclusive or.
• A trivializing formalization would drop the participation constraint from (4) (the statement is then false), or replace (4) by maximization over a set that may be empty; both are ruled out by IsEngagementMaximizer, which requires $\omega_T$ itself to be feasible.
• No library beyond Mathlib's real arithmetic is needed. Proofs of the milestones and the goal are welcome; the definitions are shared in spirit with mission II of this series, which keeps its own copy.

Selected references

• J. Kleinberg, S. Mullainathan, M. Raghavan, The Challenge of Understanding What Users Want: Inconsistent Preferences and Engagement Optimization, arXiv:2202.11776v3, 2023. https://arxiv.org/abs/2202.11776
• Same paper, Management Science, 2023. https://doi.org/10.1287/mnsc.2022.03683

Motivation

A Fisher market divides a supply of goods among buyers with different values and budgets. In many fair division models, the goods form a continuum: pieces of time, land, or a divisible resource can be allocated in arbitrarily small amounts. A direct description of all possible buyer utilities then appears to require one allocation function for every buyer. Gao and Kroer show that when values vary linearly along an interval, the same utility set has a finite description using linear constraints and a parabolic cone. This makes the utility possibilities visible to convex optimization methods even though the underlying allocation space is infinite dimensional. Gao and Kroer, §§2 and 4.

The result is a characterization of a set, rather than a claim about one selected market equilibrium. It includes every feasible utility vector, including vectors below the Pareto frontier and cases in which adjacent buyers have identical valuations. The article proves the characterization as Theorem 4 and extends it to arbitrary subintervals and piecewise linear valuations in Theorems 5 and 6. Gao and Kroer, Theorems 4–6.

Setting

There are $n$ buyers and one unit interval of items, $\Theta=[0,1]$, with Lebesgue measure. Buyer $i$ values item $\theta$ at $v_i(\theta)=c_i\theta+d_i$. An allocation assigns a nonnegative, essentially bounded share $x_i(\theta)$ to each buyer, with $\sum_i x_i(\theta)\le 1$ almost everywhere. Its utility vector has coordinates $u_i=\int_0^1v_i(\theta)x_i(\theta)\,d\theta$. The feasible utility set $U(v,[0,1])$ contains all vectors obtained this way, including utilities from allocations that leave some supply unused. Gao and Kroer, (1), p. 8.

The goal assumes normalized valuations, $c_i/2+d_i=1$, and intercepts $2\ge d_1\ge\cdots\ge d_n\ge0$. These bounds ensure that each valuation is nonnegative on the item interval. The ordering can contain ties. For each adjacent pair of buyers, the result introduces four real auxiliary variables $(z_i,w_i,s_i,t_i)$. The pair $(s_i,t_i)$ lies in the parabolic cone $\mathcal C=\{(s,t):s^2\le t\}$, and a $2\times2$ matrix $G_i$ maps it to $(z_i,w_i)$. Gao and Kroer, Theorem 4, pp. 15–16.

For the supporting welfare statement, the item space is instead a compact subset of Euclidean space. A buyer's valuation is integrable and nonnegative, prices are integrable and nonnegative, and a market equilibrium gives each buyer a utility maximizing bundle within budget while clearing all positively priced supply. A Pareto optimal allocation admits no feasible allocation that weakly improves every buyer and strictly improves one. These notions are used in Lemma 6 and the path to the interval result. Gao and Kroer, §§2 and 4.1.

Formalization targets

The main target is the full equivalence of Theorem 4:

$$u\in U(v,[0,1])\quad\Longleftrightarrow\quad u\ge0\text{ and there exist }z,w,s,t\text{ satisfying Theorem 4's linear and parabolic constraints.}$$

The constraints include $u_1\le z_1$, $u_i\le z_i+w_{i-1}$ for interior buyers, $u_n\le1+w_{n-1}$, $G_i(s_i,t_i)=(z_i,w_i)$, $s_i^2\le t_i$, $0\le z_i\le1$, $-1\le w_i\le0$, and $z_i+w_i\ge0$ for each adjacent pair. The representation quantifies over real auxiliary variables; it does not assume a market equilibrium or a partition into intervals. Gao and Kroer, Theorem 4, pp. 15–16.

The milestones are the paper's continuum second welfare theorem (Lemma 6), the ordered interval structure of equilibrium under Assumption 1 (Lemma 5), the ordered interval domination of feasible utilities (Lemma 7), the breakpoint description in the proof of Theorem 4, and the two buyer region identity in that proof. Theorem 5 is a companion target: it identifies utilities on $[l,h]$ with scaled, permuted utilities for normalized valuations on $[0,1]$. Gao and Kroer, pp. 14–19 and a10–a13.

Significance

Theorem 4 turns an infinite dimensional feasibility question into membership in a projection of a finite convex set. This lets the interval utility set enter a conic optimization model without choosing a discretization of the item space. Theorem 5 transfers that description to other intervals, and the paper uses these results for piecewise linear fair division. Gao and Kroer, §§4.2–4.3.

The mathematical results are proved in the article. The formalization work here records the precise objects and open Lean theorem statements; machine checked proofs of these new statements remain to be supplied. The generic allocation, demand, equilibrium, and feasible utility definitions can also support later results about continuum Fisher markets and Eisenberg–Gale optimality.

Difficulty

A feasible utility vector may come from a fractional allocation that varies arbitrarily along the interval. The geometric statement, however, describes it with only one adjacent pair of auxiliary variables per buyer boundary. The link must preserve the entire feasible set, including vectors below the Pareto frontier and valuations with equal intercepts. A characterization proved only for equilibrium utilities, or only for distinct valuations, would miss those vectors. Lemma 6 also works over general compact Euclidean item spaces, so its assertion cannot be reduced to the interval case. Gao and Kroer, Lemmas 5–7 and Theorem 4.

Formalization scope

Lean represents allocations and valuations as real functions modulo almost everywhere equality in the statements, rather than as quotient $L^p$ elements. Bundles must belong to $L^\infty$ and prices and valuations to $L^1$; their integral pairings are then meaningful. The feasible utility set is defined from allocations and Lebesgue measure restricted to the relevant interval. Buyers are indexed from zero in Lean and from one in the paper. Natural number indices for the auxiliary sequences follow the same shift. The goal requires $n\ge2$ because its first and last adjacent pair constraints do not exist for smaller $n$; Lemmas 5 and 7 require $n\ge1$ for their endpoint lists.

The goal includes ties among intercepts. The printed further claim that all feasible auxiliary $s_i,t_i$ lie in $[0,1]$ fails with a tie, so its companion statement assumes the relevant adjacent intercepts are strictly ordered. Theorem 5 reads the valuation as $c_i\theta+d_i$: that agrees with its normalization and interval integral, while the displayed $c_i\theta/2+d_i$ on p. 18 is inconsistent with those formulas. These readings are recorded with concrete checks in the moderation notes. Gao and Kroer, Theorems 4–5, pp. 16 and 18.

A complete proof will need reusable measure theoretic facts about allocations, interval integrals of linear functions, Pareto optimal utilities, and the image of the parabolic cone under a linear map. Contributions to those foundations and to the listed theorem statements are within scope. The target cannot be met by assuming a breakpoint partition or an equilibrium for the utility vector: it must characterize $U(v,[0,1])$ directly.

Selected references

• Yuan Gao and Christian Kroer, Infinite-Dimensional Fisher Markets and Tractable Fair Division, Operations Research, 2023. arXiv:2010.03025v5.

Why compare subsidy formats?

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

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

Market and government programs

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

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

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

Formalization targets

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

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

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

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

What the result establishes

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

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

Where the formalization is difficult

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

Formalization scope

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

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

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

Selected references

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

Motivation

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

Setting

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

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

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

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

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

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

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

Formalization targets

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

A delivery company can assign each driver a permanent district instead of allowing every driver to serve the whole city. This makes dispatching simpler, but it raises a service question: if the districts receive almost equal shares of demand and travel workload, how different can their expected delivery times be? Carlsson, Liu, Salari and Yu study this question for a region partitioning policy in which one vehicle serves each district. Their Proposition 3 gives an explicit error bound for a partition whose shares are accurate within a tolerance ε. The proposition complements their exact equitability result, Theorem 6, by quantifying the effect of a partition that can only be computed approximately.

Setting

The service region R is a compact convex subset of the Euclidean plane, with depot x₀ ∈ R. Orders arrive at a rate λ and have locations distributed with density f on R. The density is nonnegative, Lipschitz on R, and normalized by ∫_R f(x) dx = 1. There are m ≥ 1 identical vehicles, each with speed v > 0 and capacity q ≥ 1. An order requires a mean on site service time s̄ ≥ 0. The positive constant β is the geometric constant in the paper's heavy traffic delivery time expression. A partition R₁, …, R_m covers R, with districts disjoint up to area zero; vehicle i serves R_i.

For a measurable district S, let p(S) = ∫_S f(x) dx be its share of demand. Its arrival rate is λ_S = λp(S), and its conditional density is f_S(x) = f(x)/p(S) when p(S) > 0. The paper uses two partition measures:

$$\mu_1(S)=\int_S\sqrt{f(x)}\,dx,\qquad \mu_2(S)=\int_S(\bar s vq+2\lVert x-x_0\rVert)f(x)\,dx.$$

The first controls the leading travel term. The second combines service time and radial travel from the depot. A partition is ε equitable when, for every district i and each j ∈ {1,2}, the difference between μ_j(R_i) and μ_j(R)/m has absolute value at most ε.

For vehicle count k, arrival rate a, region S, and density g, write the workload factor as

$$W(k,a,S,g)=\frac{a\bar s}{k} +\frac{2a}{kvq}\int_S\lVert x-x_0\rVert g(x)\,dx.$$

The heavy traffic expression from the paper's Theorem 3 is

$$L(k,a,S,g)=\frac{\beta^2a(1-1/q)^2 \left[\int_S\sqrt{g(x)}\,dx\right]^2} {2k^2v^2(1-W(k,a,S,g))^2}.$$

The comparison value is L* = L(m,λ,R,f). For district i, the value L_i = L(1,λ_{R_i},R_i,f_{R_i}) uses that district's own arrival rate, density, and workload factor.

Formalization targets

Proposition 3: approximate districts

For λ > 0 with W(m,λ,R,f) < 1, ε ≥ 0, and an ε equitable partition, define the corrected tolerance factor

$$\eta=\frac{\varepsilon}{ \min\left\{\mu_1(R)/m,\; \frac{vq}{\lambda}\left(1-\frac{\lambda\mu_2(R)}{mvq}\right) \right\}}.$$

When η < 1, the target is the two sided estimate

$$\lvert L_i-L^*\rvert\le \frac{4\eta}{(1-\eta)^2}L^* \qquad\text{for every }i.$$

The first milestone rewrites each district's Theorem 3 expression using μ₁(R_i) and μ₂(R_i). The next two milestones give upper and lower comparisons with L*. The final algebraic milestone evaluates the larger of the two relative deviations. These are the displayed steps on the paper's e companion pages ec6 and ec12–ec13.

The printed Proposition 3 uses max in the denominator defining η. Its proof requires min: when the two entries are 1 and 100 and ε = 0.1, a district can have L_i/L* = (1.1/0.999)² ≈ 1.212, while the printed η = 0.001 permits a deviation of only about 0.004. The correction is recorded in the theorem statements and audit notes.

Significance

The bound makes partition accuracy interpretable as a service guarantee. Once both shares are close enough that η < 1, every district's leading delivery time lies in a controlled interval around the flexible policy's benchmark. It states a guarantee for each district, rather than just for a demand weighted average, so it addresses unequal service across the region.

The authors prove the displayed comparison in their accepted manuscript. This mission formalizes the comparison between explicit heavy traffic expressions; it does not claim a new queueing theorem or a machine checked proof of the stochastic model. The reusable output is a precise Lean interface for spatial demand integrals, workload, conditional district densities, and perturbation bounds involving both numerator and denominator errors. The theorem items are proof targets.

Difficulty

The denominator responds to the μ₂ error in the opposite direction from the numerator's response to the μ₁ error. Bounding their ratio requires both the district workload and the lower numerator estimate to stay in their proper sign ranges. Simply squaring the ε share inequalities is invalid until those signs are known. The condition η < 1 supplies the required room; it also rules out a zero probability district under the other hypotheses. The printed choice of max for η fails to control the error in whichever of the two scales is smaller.

Formalization scope

Lean uses EuclideanSpace ℝ (Fin 2), Lebesgue set integrals, and real valued leading terms. The density, region, depot, fleet parameters, and positive β are fixed while λ and ε vary. The source's compactness, convexity, Lipschitz density, normalization, positive vehicle count, speed, and capacity, and nonnegative mean service time are included in a single standing predicate. A partition has null measurable pieces, pairwise disjoint almost everywhere, and exact union R; shared district boundaries have area zero. The goal also states λ > 0, global workload < 1, ε ≥ 0, and η < 1, matching the stable regime and the proof's small ε condition. Capacity q = 1 remains admitted: both leading terms then vanish and the inequality still holds.

The stochastic renewal arrivals, routing policy, and queueing process are outside this development. Theorem 3 supplies the paper's leading expression, applied separately to the full region and each district. Thus L_i and L* here are leading expressions at one fixed λ, not the underlying expected delivery time functions. A fixed positive ε makes η grow near the heavy traffic boundary, so the page's parenthetical “in heavy traffic” is read through the leading expressions used by its proof. The district value is formed from λ_{R_i} and f_{R_i}; it is not defined from the global benchmark or from the right hand side of the first milestone.

A complete proof will need standard facts about set integrals and square roots, the normalization of a conditional density, and inequalities for positive real denominators. The setting definitions can support other region partition comparisons. Contributions establishing these identities and the upper and lower estimates are welcome.

Selected references

• J. G. Carlsson, S. Liu, N. Salari, and H. Yu, Provably Good Region Partitioning for On-Time Last-Mile Delivery, accepted manuscript, SSRN 3915544; published in Operations Research 72(1), 91–109 (2024), DOI: 10.1287/opre.2021.0588. Proposition 3, printed p. 21; proofs on pp. ec6 and ec12–ec13.
• D. J. Bertsimas and G. J. van Ryzin, Stochastic and Dynamic Vehicle Routing with General Demand and Interarrival Time Distributions, Advances in Applied Probability 25(4), 947–978 (1993), DOI: 10.2307/1427801. Source of the heavy traffic expression cited as Theorem 3 in the Carlsson et al. manuscript.

Motivation

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

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

Setting

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

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

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

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

Formalization targets

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

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

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

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

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

Markets with network externalities can support several levels of adoption at the same price. A consumer's willingness to buy may rise when many other consumers buy, while the ordinary price effect still works in the opposite direction. A price and an aggregate demand curve can therefore identify several self-consistent quantities without identifying which one consumers reach. In Network Externalities and Market Dominance, Akerlof, Holden and Rayo study this selection problem before analyzing firms' pricing decisions (accepted manuscript, §2.1).

The paper uses an introspective equilibrium: consumers begin with an impulse about firm 1's sales and repeatedly revise consumption in response to the previous level. The resulting limit gives a selection rule tied to an observable starting condition rather than to an arbitrary choice among fixed points. The mission formalizes Proposition 1 of the accepted manuscript, dated September 16, 2022. Its source is the repository manuscript; the numbering and printed pages here refer to that artifact, not the journal typesetting (Akerlof, Holden and Rayo, Proposition 1, p. 10).

Setting

There is a unit mass of consumers, each with unit demand. Write $p=p_1-p_2$ for firm 1's relative price, and let $Q\in[0,1]$ be its current total sales. The aggregate demand $D(p,Q)\in[0,1]$ is the quantity that would be demanded at price $p$ if consumers believed sales were $Q$. With one firm, the paper sets the second firm's price and quantity to zero, so the same two-argument demand map applies. With two firms, $p$ is the difference of their prices. An equilibrium quantity is a feasible fixed point,

$$Q=D(p,Q).$$

The inverse demand curve $P$ gives a price at which a given quantity is self-consistent: $D(P(Q),Q)=Q$ for $Q\in[0,1]$. The market assumptions say demand is continuous in price and feasible quantity, decreases with price, and increases with believed quantity. The formal market records weak monotonicity together with strict price comparisons at an inverse-demand point on the nonsaturated part of the range. These comparisons give the signs used in the paper's footnote 12 (§2, p. 5; footnote 12, p. 10).

An In/Out curve has two quantity thresholds $0<Q_L<Q_H<1$. The curve $P$ is strictly decreasing and convex on $[0,Q_L]$, strictly increasing on $[Q_L,Q_H]$, and strictly decreasing and concave on $[Q_H,1]$; convexity and concavity here are weak. Define $p_{\min}=P(Q_L)$ and $p_{\max}=P(Q_H)$. The endpoint conditions are $p_{\max}<P(0)$ and $P(1)<p_{\min}$. At a price between the thresholds, the intersections of $P(Q)=p$ with the three branches are $Q^{\mathrm{out}}(p)$, $Q^{\mathrm{mid}}(p)$, and $Q^{\mathrm{in}}(p)$. At either threshold price, two adjacent branch labels can name the same quantity (footnote 7, p. 6; §2.1, p. 8).

The consumers' impulse $I_0$ lies in $[0,1]$. Level-$k$ consumption is the actual iteration $I_k=D(p,I_{k-1})$, or $I_k=D(p,\cdot)^{\circ k}(I_0)$ with $I_0$ at level zero. An introspective equilibrium $Q_1^*$ is the limit of this sequence as $k\to\infty$ (Definition 1, p. 9).

Formalization targets

Equilibrium structure

For $p_{\min}<p<p_{\max}$, the three branch quantities are distinct and exhaust the feasible equilibrium quantities. At $p=p_{\min}$ or $p=p_{\max}$, two distinct quantities remain. The milestone from §2.1 also records uniqueness within each branch. Footnote 12 records where $D(p,Q)$ lies above or below $Q$ between these intersections (§2.1, p. 8; footnote 12, p. 10).

Selection rule

The goal is the full two-part Proposition 1. When $p_{\min}\le p\le p_{\max}$, the branch equilibria exist and

$$Q_1^*(p)= \begin{cases} Q^{\mathrm{in}}(p),&I_0>Q^{\mathrm{mid}}(p),\\ Q^{\mathrm{mid}}(p),&I_0=Q^{\mathrm{mid}}(p),\\ Q^{\mathrm{out}}(p),&I_0<Q^{\mathrm{mid}}(p). \end{cases}$$

When $p>p_{\max}$ or $p<p_{\min}$, exactly one feasible quantity solves $Q=D(p,Q)$, and $I_k$ converges to it for every $I_0\in[0,1]$. The proof's convergence and uniqueness passages are separate milestones, so the goal retains both claims without taking either as an extra assumption (Proposition 1 and proof, p. 10).

Significance

Proposition 1 ties a market's adoption outcome to the initial impulse. In the multiple-equilibrium price range, the middle equilibrium separates impulses that select the low and high quantities; outside that range, the selected quantity is independent of the impulse. This makes the refinement usable when the subsequent economic analysis asks how a price or a change in expectations can move the market between dominant firms (§2.1–§3).

The paper proves the result in ordinary mathematics. The remaining work here is a machine-checked proof of its precise selection statement and of the source passages that support it. The definition layer also supplies a reusable interface for continuous aggregate demand and inverse demand on a bounded quantity interval. There is no claim that this paper's later pricing-game propositions have already been formalized.

Difficulty

The inverse-demand picture shows three crossings, but a picture alone does not establish that every branch crossing exists or that no additional feasible fixed point is present. At a threshold, two branch labels meet, so a claim that always demands three distinct quantities would be false. Outside the threshold interval, the paper's reference to a unique intersection of $P(Q)=p$ fails at prices beyond $P(0)$ or $P(1)$: the equilibrium can instead be a saturated fixed point at $0$ or $1$. The formal statements must cover those prices with $D(p,Q)=Q$ (Proposition 1 and proof, p. 10).

The convergence claim concerns a specific recursive sequence from every allowed impulse. Fixed-point existence by itself does not identify that limit or its dependence on the impulse. The market assumptions also require care at the saturation endpoints: strict decrease in price on the whole real line would conflict with nonnegative demand at $Q=0$, while merely weak decrease permits extra fixed points that would defeat the selection claim.

Formalization scope

Lean represents prices and quantities by real numbers and restricts feasible quantities and impulses to $[0,1]$. A Market stores $D$, $P$, continuity of $D$ on real prices and feasible quantities, range bounds, weak monotonicity in quantity and price, the inverse-demand identity, and the strict nonsaturation signs from footnote 12. The paper says demand is strictly increasing in quantity below $1$; the formal interface uses weak increase because its own saturated consumer model can have a constant zero-demand segment. The strict price signs make explicit the stronger reading of “decreasing” needed at inverse-demand points. Both choices are disclosed in the setting item. The polynomial and clamped-demand example in the local verification file witnesses that the assumptions are consistent.

IsInOut retains every monotonicity, convexity, concavity, threshold-order, and endpoint condition of footnote 7, even when a clause is unused in a proof. The branch quantities are predicates that include their intervals and the equation $P(Q)=p$; the goal asserts their existence before quantifying over them. IsIntrospectiveEq uses Function.iterate and Tendsto for the prescribed $I_k$, so it cannot be satisfied by selecting an unrelated fixed point or sequence. Outside the threshold interval, uniqueness is over feasible fixed points of $D$, including $0$ and $1$. The assumptions apply to the aggregate map for either one or two firms; consumer types, their distribution, the micro-foundations, the firms' pricing game, profits, the WIN constraint, Corollary 1, and later sections are outside this mission.

A complete development needs continuity and intermediate-value results, monotonicity and convexity of real functions on intervals, and convergence of bounded sequences of real numbers. The market and level-$k$ definitions can be reused by later work on equilibrium selection. Contributions may prove the listed milestones, supply independent proofs of Proposition 1, or build the interval-dynamics lemmas they require, while retaining the statement's full price and impulse domains.

Selected references

• R. Akerlof, R. Holden and L. Rayo, Network Externalities and Market Dominance, author's accepted manuscript, WRAP 178238, dated September 16, 2022; published in Management Science (2024). Accepted manuscript; DOI.

Motivation

Entrepreneurs sometimes sell claims on a product before it exists. A token can represent a claim on a future unit, and its eventual market price can depend on how much the entrepreneur produces. That link creates a production incentive absent from a simple sale of equity. Malinova and Park study whether the token allocation can fund a venture while preserving the output choice that maximizes operating profit Malinova and Park, 2023. Their Proposition 3 gives a contract that does so under exogenous demand. This mission formalizes that proposition, including its investor break-even calculation and the uniqueness of the pre-sale size.

The paper first examines two simpler arrangements. Giving investors a fixed fraction of revenue leaves the entrepreneur paying the full marginal cost while receiving only part of the marginal revenue, which induces underproduction. Selling a fixed number of output units without a later revenue share induces overproduction: an extra unit reduces the price of units already promised to investors, a cost the entrepreneur does not bear. These comparisons are Lemmas 1 and 2 of the paper Malinova and Park, pp. 18–20. Proposition 3 combines an output pre-sale with a share of tokens issued after production.

Setting

At time zero, an entrepreneur must pay a set-up cost $C_0>0$ and obtains financing from investors. At time one, the demand intercept $x$ is observed. It is uniform on $(0,\theta)$, and producing $q\ge0$ units gives the inverse price $p(q)=x-q$. Each unit costs $c$, where $0<c<\theta$. With no financing distortion, monopoly output and operating profit are

$$q^m(x)=\max\left\{\frac{x-c}{2},0\right\},\qquad \pi^m(x)=\frac{\max\{x-c,0\}^2}{4}.$$

For a realized payoff $g(x)$, $E_\theta[g]=\theta^{-1}\int_0^\theta g(x)\,dx$. The project's net present value is $V=E_\theta[\pi^m]-C_0$. This mission assumes $V>0$, the positive-NPV case of Proposition 3. Equation (3) evaluates it as $V=(\theta-c)^3/(12\theta)-C_0$ Malinova and Park, p. 14.

Under the proposed token contract, investors buy $t>0$ initial tokens at time zero, providing $C_0+ct$. If production exceeds $t$, the entrepreneur issues $q-t$ more tokens and grants the initial holders the fraction $\alpha_t=t/(c+t)$ of those new tokens. If production is at most $t$, token-holders receive the full output and a refund of the unused production funds, $c(t-q)$. Let $\pi_t^e(x,q)$ and $I_t(x,q)$ be the resulting realized payments to the entrepreneur and investors. Their definitions follow the two output branches of the contract Malinova and Park, pp. 21–24, 39–40.

Formalization targets

Contract and output

For every demand realization and every feasible output, monopoly output maximizes the entrepreneur's realized payment under this contract:

$$\forall t>0,\ \forall x,\ \forall q\ge0,\qquad \pi_t^e(x,q)\le\pi_t^e(x,q^m(x)).$$

The claim includes the low-demand branch $q^m(x)\le t$, where several outputs can yield zero to the entrepreneur. No uniqueness of the production choice is claimed.

Break-even and expected profit

Investors must receive $C_0+ct$ in expectation. For $0<t<(\theta-c)/2$, this requirement is equivalent to the paper's equation (16):

$$E_\theta[I_t(x,q^m(x))]=C_0+ct \quad\Longleftrightarrow\quad \frac{c}{c+t}\frac{2}{3\theta}\left(\frac{\theta-c}{2}-t\right)^3 =\frac{(\theta-c)^3}{12\theta}-C_0.$$

Proposition 3 and its Appendix A proof assert that the equation has exactly one positive solution $t$, that the solution lies below $(\theta-c)/2$, and that the entrepreneur then receives $E_\theta[\pi_t^e(x,q^m(x))]=V$ Malinova and Park, pp. 24, 39–41. Milestones cover the revenue share, the high- and low-demand cases, the investor integrals, the entrepreneur's expected payoff, and the existence and uniqueness of the break-even size.

Significance

The result shows that token financing can preserve monopoly output in this model even though the two simpler token arrangements distort it. It identifies both the later-token share and the unique number of units to pre-sell, with investor break-even and the entrepreneur's full positive NPV in one contract. That contract provides the baseline for the paper's comparative statics and its later moral-hazard comparison of equity, tokens, and debt Malinova and Park, Propositions 4 and 8.

The result is proved in the cited paper. The remaining work here is a machine-checked development of its piecewise payoffs, interval integrals, and real-analysis claims. This proposal contains open Lean statements and definitions; it does not claim that their proofs have been completed. The expectation, monopoly payoff, and contract representations can also support subsequent formalizations of the paper's cost and demand comparisons.

Difficulty

The simple first-order calculation behind the revenue share covers the branch $q>t$, but it does not establish the entrepreneur's incentives when output is at most the pre-sale. In that branch her contractual payment is zero, and the refund rule changes the investor payment. The output claim must compare every $q\ge0$ across both branches, including the threshold $q=t$.

The financing claim has a separate difficulty. Investors receive three different payments over the demand ranges $x<c$, $c<x<c+2t$, and $x>c+2t$. Their expectation must equal the explicit cubic equation, while the entrepreneur's expectation must equal its left-hand side. A root argument stated only for the cubic would omit the economic break-even assertion. The paper also uses the interior bound $t<(\theta-c)/2$ when evaluating the entrepreneur's expectation Malinova and Park, Appendix A, pp. 39–41.

Formalization scope

Lean uses real parameters and a real interval integral for uniform demand. The expect definition integrates the realized payoff over $[0,\theta]$ and divides by $\theta$; endpoints have zero mass. The definitions qm and pim use a nonnegative maximum to represent no production below cost. The entrepreneur and investor payments use the contract's two branches. NPV is defined from the integral, while the formula in equation (3) is a theorem. Equation (16) is a predicate on $c,C_0,\theta,t$, while the corresponding expected-profit identity is another theorem. No closed form replaces an expected realized payment by definition.

The hypotheses $c>0$, $c<\theta$, $C_0>0$, and $V>0$ express the paper's positive-cost, productive, positive-NPV setting. A milestone about an integral over the upper demand region assumes $c+2t\le\theta$; a milestone about the cubic expected profit uses the same range. Proposition 3 states the break-even equivalence on the interior and establishes that its unique positive solution lies there. Output optimality is among $q\ge0$ under the specified contract. The paper does not define a space of all possible financing contracts, so the Lean statement does not claim an optimization theorem over such a space.

The secondary token market, the physical redemption mechanism, bankruptcy costs, consumer welfare, and the institutional discussions of Sections I and V are outside this mission. Needed reusable work includes real interval integration of piecewise polynomial payments, algebraic comparisons of quadratic payoffs, and strict monotonicity of the break-even cubic. Contributions that prove the listed statements while retaining the realized-payoff definitions are welcome.

Selected references

• Katya Malinova and Andreas Park, Tokenomics: When Tokens Beat Equity, SSRN 3286825, version of June 1, 2023; published in Management Science, 2023. SSRN preprint; journal DOI.