Optimization

Why the final licensing choice matters

A component supplier can influence a product market through both the wholesale price it charges and the technology its customers may share. Wang, Huang and Lee study a supply chain with one upstream supplier and two downstream manufacturers that invest in product quality and then compete in quantities. A cross-licensing policy lets each manufacturer use some of the other's innovation. The supplier may promise a policy before the investments, or leave the decision until after the investments and wholesale price are fixed. The latter choice creates a precise comparison: at that final stage, does permitting cross-licensing reduce the supplier's revenue? The authors answer it in Proposition 1 of their SSRN manuscript, version of 2023-04-27. Its proof is in the attached appendix, p. A.1.

This mission concerns that final-stage comparison. It is one part of the paper's broader study of how a supplier's licensing commitment affects manufacturers' innovation incentives and downstream market structure. The later innovation and initial-contract comparisons are separate questions. Here, investments and wholesale price are fixed, so the result isolates the direct quantity-market effect of licensing at the moment the supplier chooses its policy.

The downstream quantity game

Manufacturers $M_1$ and $M_2$ have already selected nonnegative innovation levels $T_1$ and $T_2$, with $T_1\le T_2$ in the presentation of equations (2) and (3). Each chooses a nonnegative production quantity $q_i$. The wholesale price $r$ is the amount each manufacturer pays the common supplier for one unit. The market-size intercept is normalized to one and per-unit manufacturing cost to zero. If licensing effectiveness is $\beta\in[0,1]$, manufacturer $i$ receives a quality improvement $T_i+\beta T_j$; $\beta=0$ represents no cross-licensing. Its inverse demand is $1+T_i+\beta T_j-q_1-q_2$. These are the model's conventions on pp. 9–10.

At fixed $T_1,T_2,\beta,r$, the manufacturers play a simultaneous quantity game. Their respective profits are

A Nash equilibrium is a pair $(q_1,q_2)\in[0,\infty)^2$ for which neither manufacturer increases its profit by changing its own nonnegative quantity while the other's quantity stays fixed. The supplier's profit at a quantity profile is $r(q_1+q_2)$. The supplier's comparison must therefore account for the manufacturers' responses under each licensing policy; it cannot compare profit at an arbitrary fixed quantity pair.

Formalization targets

The first milestone gives the exact equilibrium quantities of equation (2). Write $r_1=1+T_1(2-\beta)-T_2(1-2\beta)$ and $r_2=1+\beta T_1+T_2$. For $r\le r_1$ both manufacturers can sell; for $r_1<r\le r_2$ only $M_2$ sells; above $r_2$ neither sells. The statement characterizes every equilibrium and thereby gives existence and uniqueness across the two threshold boundaries, including the cases where a manufacturer's equilibrium quantity is zero.

The second milestone identifies the supplier's revenue at an equilibrium with the piecewise expression $\pi_s^{\mathrm{cl}}(r)$ in equation (3). Setting $\beta=0$ in that expression gives the paper's no-licensing expression $\pi_s^{\mathrm n}(r)$ in equation (4). This milestone links the paper's algebraic profit comparison to the strategic quantity game, while keeping the equilibrium property as the premise.

The goal is the supplier's ex-post preference in Proposition 1. If $q^{\mathrm{cl}}$ is any equilibrium with licensing effectiveness $\beta$ and $q^{\mathrm n}$ is any equilibrium at $\beta=0$, then both equilibria exist and

This weak inequality is intentional. At $\beta=0$ the two games coincide, and there are other parameter values at which the profits tie. The comparison holds at the same innovation levels and the same wholesale price; it is not a comparison after re-optimizing the supplier's price or the manufacturers' investment decisions.

What the result establishes

For fixed investments and price, the supplier need not lose revenue by enforcing cross-licensing after observing the manufacturers' innovation. This gives mathematical content to the paper's claim that, without an initial commitment, the supplier will choose to enforce licensing at the final contract stage. The model does not specify a separate final-contract bargaining game, so the formal goal is the profit comparison that supports that interpretation. The result does not settle whether committing to licensing before innovation is preferable: changing the initial policy can change the innovation levels themselves, which the ex-post comparison holds fixed.

The authors prove Proposition 1 by comparing the supplier-profit expressions (3) and (4) in the manuscript's appendix. A machine-checked development would additionally secure the connection from the manufacturers' Nash conditions to those expressions, including the monopoly and zero-sales regimes. These statements are currently posed as open formalization targets; a Lean file with sorry only checks that the statements are well formed, not that the paper's argument has been verified by Lean. The general two-player Nash definition can be reused for other real-strategy games; the payoff and threshold definitions are specific to this supply chain.

Where the argument has to account for cases

The quantity equilibrium changes form as the wholesale price crosses $r_1$ and $r_2$. An argument confined to the two-selling-firms region misses cases in which $M_1$ sells nothing, or neither manufacturer sells. Comparing only the duopoly formulas cannot establish an inequality at every nonnegative price. The first milestone therefore covers all three regimes, and the goal compares the profits of actual equilibria. The fact that $T_2\ge T_1$ orders the possible monopoly toward $M_2$ under the paper's chosen labels; a formulation that silently assumes both equilibrium quantities are strictly positive would lose part of Proposition 1.

Formalization scope

All parameters and quantities are real. The permitted quantity strategies and wholesale prices are nonnegative. The paper treats $r$ as a wholesale price without writing a bound in Proposition 1; $r\ge0$ is made explicit because a negative price can reverse the supplier-profit inequality. The innovation ordering $0\le T_1\le T_2$ is the convention immediately preceding equation (2). Licensing effectiveness lies in $[0,1]$. Innovation costs $k_iT_i^2$ and the paper's bound $k_2>49/144$ are unnecessary once innovation levels are fixed, so they do not enter this mission's statements.

The formalization uses an explicit pair $(q_1,q_2)$, with the first coordinate for $M_1$. The quantity-game equilibrium is defined by unilateral payoff comparisons over $[0,\infty)$, and it is not defined by equation (2). Equation (2) is instead a theorem characterizing the equilibrium. The supplier's profit is defined as $r(q_1+q_2)$ for any pair, independently of equation (3). These choices prevent the goal from becoming an inequality between two expressions whose connection to the game has merely been assumed. Equation (2)'s missing closing parenthesis in the manuscript is interpreted as the displayed first quantity divided by three. No division in the model's displayed formulas has a variable denominator.

Selected references

• J. Wang, T. Huang and J. Lee, Cross-licensing in a Supply Chain with Asymmetric Manufacturers, SSRN manuscript 3053682, version of 2023-04-27, pp. 9–11 and Appendix p. A.1; published in Manufacturing & Service Operations Management, 2023. Manuscript; DOI.

Why this formulation matters

Clustering separates observations into groups whose members resemble one another. In kernel clustering, a matrix $K$ records a similarity score for each pair of observations, and an assignment seeks groups with high total within-group similarity. Real data can also contain outliers, observations that should not be assigned to any cluster. Srivastava, Sarkar, and Hanasusanto use a binary assignment program that permits those unassigned observations and then express the same exact problem through a matrix of pairwise co-memberships. The relationship is stated as Proposition 1 of their preprint. It is the algebraic starting point for the tractable relaxations introduced immediately after the proposition in §3.

The two exact programs have different variables. The assignment program describes each observation's cluster directly. The lifted program records whether each pair belongs to the same cluster. The latter representation makes positive semidefiniteness and rank explicit, and it is the one the paper relaxes to obtain its semidefinite program. A precise equivalence matters because a relaxation of the wrong feasible set would no longer be a relaxation of the stated assignment problem.

The two finite matrix programs

Let $N$ be the number of observations and $r$ the number of available clusters. A binary assignment matrix $Z\in\{0,1\}^{N\times r}$ has one row per observation and one column per cluster. In formulation (3), each row sums to at most one. A row with one nonzero entry assigns its observation to that cluster; a zero row leaves the observation unassigned. Thus the same matrix represents both inliers and outliers. Cluster sizes need not be equal, and unused cluster columns are allowed.

The clustering matrix $X=ZZ^\top$ has one row and column per observation. Its entry $X_{ij}$ is one when observations $i$ and $j$ share a cluster and zero otherwise, including when either observation has a zero assignment row. Formulation (4) asks instead for an $N\times N$ matrix $X$ whose entries lie in $\{0,1\}$, that is positive semidefinite, and whose rank is at most $r$. The rank bound limits the number of distinct nonzero cluster directions. Positive semidefiniteness is a property of the full real matrix, including its symmetry; it is not merely a condition on its diagonal.

Let $K\in\mathbb R^{N\times N}$ be the similarity matrix, $\gamma\in\mathbb R$ a penalty parameter, and $E_N$ the all-ones $N\times N$ matrix. The entrywise Frobenius inner product is $\langle A,B\rangle=\sum_{i,j}A_{ij}B_{ij}$. The programs maximize, respectively, $\langle K-\gamma E_N,ZZ^\top\rangle$ over feasible $Z$ and $\langle K-\gamma E_N,X\rangle$ over feasible $X$. Both have a feasible zero matrix, even at the boundary values $N=0$ and $r=0$.

Formalization targets

The goal is Proposition 1, stated with its factor and rotation. If $X^*$ is an optimal matrix for (4), there must exist $G\in\mathbb R^{N\times r}$ and an orthogonal $O\in\mathbb R^{r\times r}$ such that $Z^*=GO$ is feasible and optimal for (3), with

Here “feasible and optimal” includes the zero-one entry condition, the row-sum bound, and comparison with every feasible assignment matrix. The objective identity alone would say little: once the Gram factorization and orthogonality hold, it follows algebraically. The substantive result is the existence of an assignment-compatible rotation of a factor of every lifted optimum.

The milestone list follows the five claims in Appendix B of the preprint: lifting a feasible assignment to a feasible $X$ without changing its value; factoring a rank-bounded positive semidefinite $X$ through $r$ columns; classifying factor rows as zero or unit vectors; showing that distinct nonzero rows are orthogonal; and rotating those rows into assignment coordinates. These statements address both directions of the feasible-set correspondence used by Proposition 1.

What the result supplies

The proposition says that the matrix constraints in (4) describe the same exact clustering choices as the assignment constraints in (3), up to a choice of orthogonal coordinates for the factor. A lifted optimum therefore represents an assignment optimum rather than merely a matrix with the same numerical objective. Conversely, an assignment can always be lifted to a matrix accepted by (4). The paper can then drop the binary or rank constraints to obtain relaxations while keeping a clear exact program as their reference point; see §3 of the preprint.

The proposition is proved in the source paper. This mission seeks a machine-checked proof of that known claim and reusable finite-matrix results about binary positive semidefinite Gram matrices. In particular, the factorization and row-structure milestones can be used beyond spectral clustering whenever a zero-one Gram matrix appears with a rank bound. The Lean declarations here are proposed statements; their sorry proofs remain for solvers to complete.

Where the difficulty lies

The forward implication is immediate once a valid assignment matrix is given: its Gram matrix is positive semidefinite and has rank at most the number of cluster columns. The reverse implication carries the mathematical work. Positive semidefiniteness and low rank alone produce a real factor, but the factor need not have zero-one entries. A generic factor rotation also need not yield one-hot rows. The zero-one condition on every Gram entry is what constrains the relative positions of the nonzero rows strongly enough to recover assignment directions. The result must work when several observations share a direction, when some rows vanish, and when fewer than $r$ clusters are occupied.

Formalization scope

The formalization uses Mathlib matrices indexed by Fin N and Fin r over $\mathbb R$. Feasibility of (3) is entrywise membership in $\{0,1\}$ together with row sums at most one. Feasibility of (4) is entrywise membership in $\{0,1\}$, Matrix.PosSemidef, and Matrix.rank ≤ r. The objectives use the explicit sum of entrywise products, so no operator norm or alternate matrix inner product enters the statement. Global optimality is defined by comparison against the corresponding whole feasible set. The factor $G$ has exactly $r$ columns, and the rotation belongs to the real orthogonal group of dimension $r$.

The paper obtains $K$ from a Gaussian kernel and takes $\gamma\in(0,1)$ for the clustering application. Proposition 1 and Appendix B use only the displayed algebraic programs, so the formal statement permits arbitrary real $K$ and $\gamma$. No probability model, symmetry assumption on $K$, positive dimension assumption, or nonempty-cluster condition is needed. The boundary cases $N=0$ and $r=0$ retain their literal meanings. The formalization cannot assume that a feasible $X$ is already block diagonal or is already a Gram matrix of a binary assignment; that is the conclusion being established.

Useful contributions include proofs of the five Appendix B milestones, a finite-dimensional factorization theorem with the prescribed number of columns, and the rotation theorem that handles repeated or zero rows. These pieces should share the stated definitions so that the eventual proof of Proposition 1 uses precisely formulations (3) and (4).

Selected references

• P. R. Srivastava, P. Sarkar, and G. A. Hanasusanto, A Robust Spectral Clustering Algorithm for Sub-Gaussian Mixture Models with Outliers, Operations Research 71(1), 2023; arXiv:1912.07546v3, §3, Proposition 1 and Appendix B.

Motivation

Recommender systems on online platforms are usually trained to maximize engagement: time spent, items consumed, sessions returned. The implicit justification is revealed preference: a user who consumes more must value the content more. Behavioural economics questions that inference when a person's choices are driven by two conflicting processes, a deliberate one that weighs long-run utility and an impulsive one that reacts to the item in front of it.

Kleinberg, Mullainathan and Raghavan (2023) build a minimal model of such a user and ask when engagement is a good proxy for utility. Their first characterization (Theorem 4.1, a separate mission) says that the engagement-maximizing content differs from the utility-maximizing content only through higher moreishness, or higher span with lower value. This mission formalizes the complementary positive result, Theorem 4.2: on a content manifold where no content is very moreish and all content has roughly equal value (a "salad"-like manifold), maximizing engagement loses only a small, explicitly bounded amount of user utility.

Setting

A content distribution is a triple $\omega=(p,q,\bar v)$ in the parameter space

The user consumes items one at a time. System 2, the deliberate agent, collects utility with mean $\bar v$ per item while it is still interested, and pays an outside option $W>0$ per step spent on the platform. After each item system 2 stays interested with probability $q$, the span. System 1, the impulsive agent, is hooked by each item with probability $p$, the moreishness, and then consumes the next item without consulting system 2. Define

System 2 visits the platform only if this is worthwhile, so its expected utility is equation (1),

and the session length $T$ is $0$ when the user does not visit ($g_S(\omega)<0$) and otherwise has expectation $\mathbb E[T(\omega)]=g_T(\omega)$, equation (2).

A platform chooses content from a content manifold $\mathcal M\subseteq\Omega$, which the paper assumes contains a point with $\mathbb E[S]>0$. The utility maximizer $\omega_S=(p_S,q_S,\bar v_S)$ maximizes $g_S$ over $\mathcal M$ (3). The engagement maximizer $\omega_T=(p_T,q_T,\bar v_T)$ maximizes $g_T$ over the points of $\mathcal M$ at which the user participates, $\{\omega\in\mathcal M:g_S(\omega)\ge0\}$ (4). The proof uses $a_i=\frac{1}{1-p_i}$ and $b_i=\frac{1}{1-q_i}$ for $i\in\{S,T\}$, so that $\mathbb E[T(\omega_S)]=a_S+b_S-1$.

Formalization targets

Goal: Theorem 4.2 (p. 17)

Suppose $p\le\alpha<1$ for every $(p,q,\bar v)\in\mathcal M$, and $|\bar v-v_0|<\beta$ for every $(p,q,\bar v)\in\mathcal M$, for some $v_0$. Then

Milestones (p. 18)

1. Inequality (5): if $g_T(\omega_T)\ge g_T(\omega_S)$, then $b_S-b_T\le a_T-a_S$.
2. Inequality (7): if $0\le p_i\le\alpha<1$, then $1\le a_i\le\frac{1}{1-\alpha}$.
3. The gap identity: when $g_S\ge0$ at both points,

A supporting statement, implicit in the proof, is that participation $g_S(\omega)\ge0$ at a point of $\Omega$ forces $\bar v\ge W$.

Significance

The theorem is the paper's sufficient condition for engagement optimization to be benign. It is quantitative: the utility loss is linear in the value spread $\beta$, scaled by the engagement $\mathbb E[T(\omega_S)]$ of the utility-optimal content, plus a term that vanishes as the moreishness bound $\alpha$ goes to $0$. The paper notes that the linear dependence on engagement is unavoidable, since a user can lose a constant utility per step when $\bar v_T<\bar v_S$. Together with Theorem 4.1 it delimits when a platform that observes only engagement can safely optimize it, and it motivates the paper's §5, on how a platform might learn which kind of manifold it is on.

The result is proved in the paper, with a short proof. As far as is known, neither the model nor the theorem has been machine-checked. The formalization fixes the participation convention for $\mathbb E[T]$, the feasibility of $\omega_S$ in the engagement problem, and the implicit hypotheses listed below, which the printed proof uses without stating.

Difficulty

The algebra is elementary once the denominators are known to be positive. The difficulty lies in the bookkeeping the printed proof leaves implicit. Inequality (5) is derived from "$\mathbb E[T(\omega_T)]>\mathbb E[T(\omega_S)]$", but (4) only gives $\ge$, and only once $\omega_S$ is shown feasible for (4), which needs $g_S(\omega_S)>0$, i.e. the standing assumption on $\mathcal M$. Multiplying (5) by $\bar v_T-W$ needs $\bar v_T\ge W$, which follows from $g_S(\omega_T)\ge0$ and $W>0$. The bound on $(a_T-a_S)\bar v_T$ splits on the sign of $a_T-a_S$, and uses $\alpha\ge0$ (from $\mathcal M\neq\emptyset$) and $v_0+\beta>\bar v_T\ge0$. Finally, $\mathbb E[T(\omega_S)]$ must be identified with $a_S+b_S-1$ through participation at $\omega_S$. Using $g_T$ in place of $\mathbb E[T]$, or dropping the participation constraint from (4), changes the theorem.

Formalization scope

The Lean development lives in the namespace EngagementOpt.Salad and imports the frozen shared model in EngagementOpt.Misalign. There, a content distribution is a structure Params with real fields p, q, v; InOmega ω states $0\le p<1$, $0\le q<1$, $0\le\bar v$. The shared functions gS W, gT and this chunk's ES W, ET W, aCoef, bCoef are as above, with ET W ω = if gS W ω < 0 then 0 else gT ω. The shared maximizer predicates IsUtilityMaximizer W M ωS (membership and IsMaxOn (gS W) M ωS) and IsEngagementMaximizer W M ωT (membership, 0 ≤ gS W ωT, and IsMaxOn gT {ω ∈ M | 0 ≤ gS W ω} ωT) hold for every maximizer, so the theorem holds for any tie-breaking rule. Closedness of $\mathcal M$ only guarantees that maximizers exist and is not assumed. The goal's hypotheses are: $W>0$; $\mathcal M\subseteq\Omega$; a point of $\mathcal M$ with $g_S>0$; the two maximizer predicates; $\alpha<1$ and $p\le\alpha$ on $\mathcal M$; and $|\bar v-v_0|<\beta$ on $\mathcal M$ for a given $v_0$.

Three of these are implicit in the paper and are disclosed: $W>0$ (§2.1 normalizes $W=1$); $\alpha<1$, without which condition 1 is vacuous on $\Omega$ and the bound fails (Lean's $x/0=0$ would turn $\alpha=1$ into a false statement); and the standing assumption of p. 16. Neither $0\le\alpha$ nor $0<\beta$ is assumed; both follow from the hypotheses. Inequality (5) is posed with $\le$ rather than the printed $<$, because only $\ge$ is available from (4). The hypotheses are satisfiable: with $W=1$, $\mathcal M=\{(0,\tfrac12,3),(\tfrac12,\tfrac12,3)\}$, $\alpha=\tfrac12$, $v_0=3$, $\beta=0.1$, the maximizers are $\omega_S=(0,\tfrac12,3)$ and $\omega_T=(\tfrac12,\tfrac12,3)$, and the bound reads $3\ge0.5$.

Everything needed is in Mathlib (real arithmetic, max, |·|, IsMaxOn). Proofs of the milestones and the goal are welcome; the base model module is shared with the Theorem 4.1 mission of the same paper.

Selected references

• J. Kleinberg, S. Mullainathan, M. Raghavan, The Challenge of Understanding What Users Want: Inconsistent Preferences and Engagement Optimization, Management Science, 2023. DOI 10.1287/mnsc.2022.03683; read as arXiv:2202.11776v3.
• G. S. Becker, K. M. Murphy, A Theory of Rational Addiction, Journal of Political Economy 96(4), 1988. DOI 10.1086/261558.

Motivation

Treatments for rare diseases can require substantial research and development spending while reaching a small patient population. A public subsidy can cover part of the manufacturer's development cost, part of the patient's price, or both. Which recipient should receive the subsidy depends on how the manufacturer responds. A further design choice is whether the manufacturer is paid when a drug is sold or only when treatment succeeds. Olsder, Martagan, and Tang formulate these choices as a sequential game between the government, a manufacturer, and patients in their SSRN working paper, §§3–4. This mission concerns their results for the case in which the manufacturer sets the price.

The paper reports that a manufacturer subsidy alone is optimal under either payment scheme and that the relative prices under the two schemes change with the government budget. The price comparison is useful because a payment contract intended to protect patients can change the price set by the manufacturer. The mission uses the working paper dated 2019-11-13. Its page and equation numbers are those of that version, which precedes the published article.

Setting

The government first chooses two subsidy shares: $\alpha\in[0,1)$ covers the fraction $\alpha$ of research cost and $\beta\in[0,1)$ covers the fraction $\beta$ of the unit price paid on a patient's behalf. The manufacturer then chooses a nonnegative unit price $p$ and a positive target efficacy $e$. Research cost is $ke^2$, with $k>0$, so the manufacturer's effective cost is $(1-\alpha)ke^2$. The government has a budget $B>0$. The market size is one, and patient valuations are uniform on $[0,1]$; these conventions are given in §3.1–§3.2.

In Setting (1A) the manufacturer receives the price for every sale. Its profit is $\pi_A=p(1-(1-\beta)p/e)-(1-\alpha)ke^2$. At price and efficacy $(p,e)$, patient welfare is $W_A=(e-(1-\beta)p)^2/(2e)$, while government spending is $M_A=\alpha ke^2+\beta p(1-(1-\beta)p/e)$. These are the paper's equations (2), (3), and (5). In Setting (1B) payment occurs only if treatment succeeds. The corresponding expressions are $\pi_B=ep(1-(1-\beta)p)-(1-\alpha)ke^2$, $W_B=e(1-(1-\beta)p)^2/2$, and $M_B=\alpha ke^2+e\beta p(1-(1-\beta)p)$, from equations (7), (8), and (10) of the same source.

For each scheme, a manufacturer best response is a pair $(p,e)$ maximizing that scheme's profit over all $p\ge0$, $e>0$. A government policy is optimal when it has a best response at which spending does not exceed $B$, and its patient welfare is at least the welfare of every feasible policy evaluated at every manufacturer best response. This expresses the government's leader role and the manufacturer's follower role in the game's sequence of events, rather than assigning the closed forms of §§4.1–4.2 to either player by definition.

Formalization targets

Government policy under each payment scheme

Proposition 1 of the working paper, p. 12, gives the unique optimal policy under sales-based payment. The paragraph after (16) on p. 13 says the same policy is optimal under outcome-based payment:

The budget binds at this policy. In both settings the optimal patient welfare and the manufacturer's profit equal $2B/(\sqrt{256Bk+1}-1)$. These policy claims, the two best-response formulas, and the two welfare and spending reductions form the six milestones.

Price comparison

Corollary 1 on p. 13 compares the manufacturer's optimal price in the two payment schemes. If $p_A$ and $p_B$ denote prices at optimal policies and best responses, the goal is the three-way statement

The printed second clause uses $B\ge k-1/8$ and says “higher”; equality of the two prices at the threshold is a boundary slip. The formal target records equality separately and preserves the strict high-budget comparison.

Significance

The policy result identifies which subsidy reaches patients most effectively within this model: when the manufacturer sets the price, the government uses its entire budget on the manufacturer's development cost, regardless of whether payment is per sale or contingent on treatment success. The price result adds a distinct comparison. Equal optimal subsidies and equal patient welfare do not imply equal prices; the sign of the price difference depends on $B$ relative to $k-1/8$. This distinction appears explicitly in the paper's discussion following Corollary 1, pp. 13–14.

The working paper proves these results mathematically. The mission's remaining work is to give machine-checked proofs for the game definitions, both best-response results, both welfare and spending reductions, the unique optimum, and the final price comparison. It does not assert that those proofs have already been formalized. The definitions of attained best response and government optimality can also support later analyses of different subsidy or payment rules.

Difficulty

The government cannot compare the two schemes by holding the manufacturer's choices fixed. The manufacturer optimizes both price and efficacy after observing the subsidy policy, and the two profit functions have different price terms. Even after determining each manufacturer's response, identical formulas for government welfare and spending do not themselves establish an attained and unique optimum on the continuous half-open policy region $[0,1)^2$. The price comparison then concerns the actual best-response prices at that optimum, including the threshold where the two prices coincide. These dependencies explain why the reduced expressions alone cannot serve as the definition of the game.

Formalization scope

Lean represents all parameters, policies, prices, efficacies, profit, welfare, and spending in $\mathbb R$. The policy predicate requires $\alpha,\beta\in[0,1)$. Every theorem assumes $k>0$; the budget results also assume $B>0$. These positivity conditions make the paper's denominators meaningful and state its implicit economic regime. Prices chosen by the manufacturer satisfy $p\ge0$. Its efficacy choice satisfies $e>0$ and has no imposed upper bound of one: equations (3) and (8) maximize over $e$, and in the high-budget part of Corollary 1 their optimizer can exceed one. This is a convention of the paper's algebraic model, even though efficacy is introduced as a probability.

The demand expressions used in the paper's equations are left unclipped. At the stated best responses, they lie in the relevant nonnegative range. Best responses are represented as sets of all maximizers, and the goal compares every response at every optimal policy. Government optimality requires a feasible best response and comparison with every feasible competing policy and response, so neither existence nor uniqueness is obtained from an empty set. In particular, the reduced welfare and budget formulas (13) and (16) are milestone conclusions, not definitions of government choice. Reusable contributions include real optimization arguments for joint price and efficacy maximization and for attained welfare maxima over subsidy policies.

Selected references

• W. Olsder, T. Martagan, and C. S. Tang, Improving Access to Rare Disease Treatments: Optimal Subsidies, Pricing, and Payment, SSRN working paper 3481150, version of 2019-11-13, §§3–4, pp. 8–14. SSRN.
• W. Olsder, T. Martagan, and C. S. Tang, Improving Access to Rare Disease Treatments: Subsidy, Pricing, and Payment Schemes, Management Science, 2023. DOI: 10.1287/mnsc.2022.4634.

Why parameter uncertainty changes portfolio choice

An investor selecting a portfolio from estimated returns faces two distinct outcomes: the average utility the chosen rule delivers across possible historical samples, and the variation of that utility from one sample to another. A portfolio rule can perform well on average while being sensitive to the particular observations used to estimate it. Lassance, Martín-Utrera, and Simaan quantify this sensitivity for portfolios estimated from Gaussian returns and propose a mean-risk criterion that penalizes the standard deviation of out-of-sample utility (OOSU). This mission concerns the shrinkage intensity that maximizes that criterion. Its source is the authors' SSRN manuscript dated August 18, 2023, including the Internet Appendix; page labels IA1–IA45 refer to that appendix.

The paper's Proposition 1 provides an exact finite-sample variance for OOSU, and Proposition IA.1 restates a closed-form OOSU mean from Kan, Wang, and Zhou. Those formulas make it possible to compare choices that maximize average utility, minimize utility variance, or balance the two. Proposition 4 characterizes the balancing choice without fixing the risk weight to a particular numerical calibration. Lassance, Martín-Utrera, and Simaan, §§4–5 and Internet Appendix IA.1.

The market and the shrinkage rule

There are $N$ risky stocks. Their excess-return vector has population mean $\mu$ and positive-definite covariance matrix $\Sigma$. An investor with risk-aversion coefficient $\gamma>0$ holds weights $w$ summing to one and evaluates their mean-variance utility as $U(w)=w^\top\mu-(\gamma/2)w^\top\Sigma w$. The population global-minimum-variance portfolio has mean $\mu_g$ and variance $\sigma_g^2>0$. The zero-cost portfolio that accounts for mean-return opportunities has return variance $\psi^2\geq0$. These constants are defined from $\mu$ and $\Sigma$ in equations (5)–(7). Source, §3.1.

From $T$ independent Gaussian observations, the investor estimates the mean and covariance, using a $1/T$ factor in the sample covariance. The sample mean-variance portfolio and sample global-minimum-variance portfolio are mixed using an intensity $\kappa\in[0,1]$: $\kappa=0$ selects the latter and $\kappa=1$ the former. Because the data are random, this portfolio's OOSU is random. Let $E_T(\kappa)$ and $V_T(\kappa)$ denote its OOSU mean and variance. In this mission they are the exact analytic expressions in (IA1)–(IA2) and (13)–(19), respectively. The formulas depend on $N,T,\gamma,\mu_g,\sigma_g^2,\psi^2$, and $\kappa$; the variance formula is a fourth-degree polynomial in $\kappa$. Source, §§3.2–4.1 and Appendix IA.1.

For a fixed robustness weight $\lambda\geq0$, the mean-risk OOSU is

The robust intensity $\kappa_R$ maximizes $R_T$ on $[0,1]$. A variance-minimizing intensity is denoted $\kappa_V$, while $\kappa_E(T)$ maximizes $E_T$ and has the explicit form (IA3). The sample-size condition throughout finite-sample claims is $N\geq2$ and $T>N+7$. Source, Assumption 1 and equations (20)–(21).

Formalization targets

The main target is Proposition 4. For every finite sample size allowed by Assumption 1, maximizers of $R_T$ and minimizers of $V_T$ exist, and every such pair obeys

When $\psi^2>0$, every sequence of robust maximizers for increasing $T$ also obeys

The ordered milestones establish that $\kappa_E(T)$ is the OOSU mean maximizer and lies in $[0,1]$; that it tends to one for $\psi^2>0$; that OOSU variance decreases with sample size and tends to zero for each fixed admissible $\kappa$; and that variance is nondecreasing as $\kappa$ rises from $\kappa_E(T)$ to one. The last milestone isolates the shrinkage-intensity clause of Proposition 2(2). Source, Proposition IA.1, Proposition 2, and Proposition 4.

What the result supplies

The inequality puts the risk-balanced choice on a single interval with two interpretable endpoints. A user of the model can compare robust allocations with the mean-optimal and variance-optimal portfolios without solving an unconstrained optimization problem over all intensities. The asymptotic statement says that, for fixed market parameters and positive $\psi^2$, any robust choice approaches the sample mean-variance endpoint as the historical sample grows. The theorem itself is proved in the manuscript; this mission asks for machine-checked statements and proofs of that known result, not for a new mathematical claim. Source, §5.2 and proof of Proposition 4, pp. IA44–IA45.

Formalizing the closed-form analysis also produces reusable tools for optimizing a polynomial mean and a polynomial variance under a square-root risk penalty on a compact interval. The supporting items separate the paper's exact formulas from the statements about their extrema and limits. The probabilistic derivation of the variance is the target of the separate Proposition 1 mission; the closed-form identities here let this mission focus on the optimizer comparison. No proof of this mission's goal is claimed to be machine checked yet.

The central difficulty

The mean has a transparent quadratic maximum, but the variance is a fourth-degree expression whose coefficients are rational functions of $T,N,\gamma,\sigma_g^2,$ and $\psi^2$. A direct comparison of objective values at arbitrary intensities does not expose the ordering of all possible extrema. Moreover, the risk penalty uses $\sqrt{V_T}$, so its behavior cannot be inferred from the mean and variance formulas by treating the penalty as $V_T$ itself. The sample-size limit concerns every sequence of optimizers, while the variance milestone gives a pointwise limit for each fixed $\kappa$; relating the two requires control over the entire admissible interval. Source, Proposition 1 and proof of Proposition 4.

Formalization scope

Lean stores $N$ and $T$ as natural numbers and casts them to real numbers before every subtraction in the rational formulas. A fixed parameter structure holds $N,\gamma,\sigma_g^2,\psi^2,\mu_g,$ and $\lambda$; $T$ remains an argument so that limits as $T\to\infty$ keep the other parameters fixed. The standing predicate requires $N\geq2$, $\gamma>0$, $\sigma_g^2>0$, $\psi^2\geq0$, and $\lambda\geq0$. Individual finite-sample statements require $T>N+7$. The positivity and nonnegativity of the population variances come from positive definiteness of $\Sigma$; the Gaussian sampling model is what identifies the closed forms as actual OOSU moments in Proposition 1 and Proposition IA.1.

The variance function is the exact sum of (14) and the polynomial (15) with coefficients (16)–(19), including the displayed polynomial $C(T,N,\psi^2)$. The mean function is (IA1)–(IA2); $\kappa_E(T)$ is (IA3); and the robustness function uses Real.sqrt of the variance, exactly as (20) requires. Extrema are taken on Set.Icc 0 1, with explicit existence and quantification over every optimizer. The goal does not choose a convenient maximizer or rely on a potentially empty optimizer set. The added $\psi^2>0$ condition appears only in the two limit statements, since at $\psi^2=0$ the printed limits fail. The manuscript's claim that the underlying estimated portfolio is consistent is outside this closed-form model, which does not contain that random portfolio.

The complete development needs real polynomial and rational inequalities, continuity and extrema on compact intervals, and limits of the coefficient functions. These tools can serve other mean-risk optimization problems. Contributions that close the four cited milestones or supply reusable analytic lemmas for them fit this mission. The paper's monotonicity claim in the stock count $N$ is excluded because it is false for some admissible parameters; its variance and zero-cost-variance clauses are outside the focused milestone list. Source, Proposition 2(2) and proof, pp. 16 and IA39–IA44.

Selected references

• N. Lassance, A. Martín-Utrera, and M. Simaan, The Risk of Expected Utility under Parameter Uncertainty, authors' SSRN manuscript dated August 18, 2023, later published in Management Science (2024). SSRN 3855546; DOI 10.1287/mnsc.2023.00178.
• R. Kan, X. Wang, and G. Zhou, Optimal Portfolio Choice with Estimation Risk: No Risk-Free Asset Case, Management Science 68(3), 2047–2068 (2022). DOI 10.1287/mnsc.2021.3989.

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)

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,

(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):

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

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:

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.

Motivation

Firms can raise money before production by selling claims on future output. In the model of Malinova and Park, these claims are tokens: a buyer prepays for a quantity of the good, and the final contract also gives token holders a share of tokens issued after demand becomes known. The firm must choose how many tokens to pre-sell. A larger pre-sale brings in more finance but changes the allocation of later sales revenue. The paper identifies contract terms that preserve the firm's monopoly output choice and determines the pre-sale quantity by investors' break-even condition (Proposition 3, p. 24). Proposition 4 asks how that quantity responds when financing need, production cost, or expected demand changes. These comparative statics make the contract's financing response explicit rather than leaving the break-even equation as an isolated root.

Setting

An entrepreneur pays a set-up cost $C_0>0$ to launch production and then incurs a marginal cost $c>0$ per unit. After financing, a demand intercept $x$ is drawn uniformly from $(0,\theta)$, where $c<\theta$. At output $q$, the inverse demand price is $x-q$. Without financing distortions, the monopoly quantity is $q^m(x)=\max\{(x-c)/2,0\}$ and its profit is $\pi^m(x)=\max\{x-c,0\}^2/4$. For a realized payoff $g(x)$, expectation means the average $E_\theta[g]=\theta^{-1}\int_0^\theta g(x)\,dx$. The venture's net present value is $E_\theta[\pi^m]-C_0$, equal in this domain to $(\theta-c)^3/(12\theta)-C_0$ (equation (3), p. 14).

Under the optimal token contract of Proposition 3, investors buy $t$ tokens at time zero, and token holders receive the fraction $\alpha_t=t/(t+c)$ of new tokens issued when output exceeds the pre-sale. A refund rule applies when output falls below the pre-sale. The resulting positive break-even pre-sale size is determined by equation (16):

For a positive-NPV venture, this equation has one positive root, in $(0,(\theta-c)/2)$ (Appendix A, pp. 40–41). The mission treats the root as a solution of the equation, so statements about the optimal quantity apply to every value satisfying it.

Formalization targets

The comparative-statics goal

Proposition 4, p. 25, asserts three strict directions. If $t(c,C_0,\theta)$ denotes the unique positive root of (16), then, while both endpoint ventures have positive NPV,

Thus a larger set-up cost or marginal cost requires more pre-sold tokens, while a higher demand level requires fewer. The Lean goal compares arbitrary positive roots directly. It places the NPV condition at the higher cost in the second comparison and at the lower demand level in the third; these are the restrictive endpoints. The first comparison places it at the higher set-up cost.

Source milestones

The milestone list follows the Appendix A proof: existence and uniqueness of the root of (41); the negative $t$ derivative (42); the positive $c$ derivative (45); the negative $\theta$ derivative (46); and the derivative in $t$ of the expression in (46), equation (47). These are source claims, with their displayed constants retained. Equation (42) and equation (45) contain printing errors in the SSRN copy; the formal statements use the actual derivatives and the milestone quotes retain the printed text.

Significance

Proposition 3 establishes that the chosen token contract can finance a positive-NPV venture while keeping the efficient monopoly output. Proposition 4 then describes the contract's response to the model's three principal parameters. Its strict inequalities distinguish an actual response from a weak monotonicity claim that could allow the pre-sale to remain unchanged. The demand comparative static is economically specific: a higher $\theta$ raises the demand intercept on average, but the quantity of tokens needed to finance the same set-up cost falls.

The paper proves these results analytically. This mission seeks machine-checked proofs of the root comparison and its stated derivative milestones. A completed development would provide reusable results about parameter-dependent roots of rational functions, especially when the root is specified by a break-even condition rather than by an explicit formula. The current Lean files are compiled statements with proof placeholders; compilation does not establish the mathematical results.

Difficulty

Equation (16) is cubic in a quantity that also occurs in a denominator, so the root does not offer a convenient closed expression for direct comparison. The endpoint restrictions matter: the meaningful root lies strictly between zero and $(\theta-c)/2$, and derivatives that have the desired sign in that interval need not keep the same sign outside it. In particular, the $t$ derivative in (42) reaches zero at the upper boundary. The demand derivative in (46) also vanishes at $t=0$, making its strict sign in the interior a separate claim. A literal transcription of two printed derivatives would give incorrect equalities even though their intended sign conclusions survive. The formal development therefore needs both careful domain control and the corrected expressions.

Formalization scope

The namespace TokenFinance.Statics represents all quantities as real functions. Uniform expectation is the interval integral divided by $\theta$. Monopoly output and profit use max to encode zero production below cost. The common Setting definition file also records the equity and debt payoffs and the token contract's case split, following the series-wide model. The break-even condition is exactly the closed-form equation (16), while NPV remains the integral of realized monopoly profit minus $C_0$. The goal assumes the paper's standing $c>0$, $C_0>0$, $c<\theta$, and positive NPV, written as $C_0<(\theta-c)^3/(12\theta)$ using equation (3). Derivative statements state their own regions and nonzero-denominator conditions. The token size is quantified over positive roots rather than chosen by an arbitrary selection function.

The root cannot be defined to have the claimed monotonicity, and the derivative signs cannot be inserted as hypotheses of the goal. The missing work includes real-variable derivative calculations, root existence and uniqueness on the economic interval, and the strict parameter comparisons. The secondary token market, redemption mechanics beyond the contract payoffs, bankruptcy costs, consumer welfare, and the paper's institutional discussion are outside this mission's scope.

Selected references

• Katya Malinova and Andreas Park, Tokenomics: When Tokens Beat Equity, SSRN 3286825, version of June 1, 2023, pp. 14, 24–25, 40–42. SSRN preprint.
• Katya Malinova and Andreas Park, Tokenomics: When Tokens Beat Equity, Management Science, 2023. DOI:10.1287/mnsc.2023.4882. The mission's equation and page references follow the SSRN version above.

Why the distribution of subsidies matters

Agricultural subsidies can raise total crop supply while changing which farmers produce it. A payment tied to planted input gives a larger reward per unit of harvested output to a farmer who needs more input for that output. A payment tied to harvested output gives the same reward per unit of output to every farmer. These differences matter when a government cares about the distribution of production and income across farms as well as total supply. Fan et al. (2023) study these effects in a finite market where farmers choose quantities and compete through a common market price.

This mission isolates the paper's distribution result for a combined subsidy, which pays on both planted input and harvested output. It asks how a difference in the dispersion of farmers' input-to-output ratios between two otherwise identical markets affects their equilibrium output and profit. The result is Proposition 4 of the SSRN version. The paper proves it in Online Appendix A, p. 4. The result is mathematically stated and proved in the paper; the machine-checked formalization of its statement and proof is the work here.

Market and order

There are $N\ge1$ farmers, indexed in the paper by $j=1,\ldots,N$. Farmer $j$ must plant $z_jq_j$ units of input to harvest $q_j$ units of output. Thus $z_j>0$ is an input-to-output ratio; a smaller ratio means more output per unit of input. The ratios are listed in nondecreasing order. Planting costs $c_P$ per unit of input, harvesting costs $c_H$ per unit of output, and total harvested output is $Q=\sum_jq_j$. The market-clearing price is $p=\alpha-\beta Q$, where $\alpha,\beta>0$.

Under a combined subsidy $(s_P,s_H)$, farmer $j$ receives $z_js_P+s_H$ per unit of output. The first part is payment for planted input and the second for harvested output. A farmer choosing $q_j\ge0$ while the other farmers' outputs stay fixed has profit