Optimization

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:

$$(\alpha,\beta)=(\alpha^*,0),\qquad \alpha^*=\frac{1+128Bk-\sqrt{256Bk+1}}{128Bk}.$$

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

$$B<k-\tfrac18\Rightarrow p_A<p_B,\qquad B=k-\tfrac18\Rightarrow p_A=p_B,\qquad B>k-\tfrac18\Rightarrow p_A>p_B.$$

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

$$R_T(\kappa)=E_T(\kappa)-\lambda\sqrt{V_T(\kappa)}.$$

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

$$\kappa_V\leq\kappa_R\leq\kappa_E(T).$$

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

$$\lim_{T\to\infty}\kappa_R(T)=1.$$

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)

$$\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.

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

$$\frac{c}{c+t}\frac{2}{3\theta}\left(\frac{\theta-c}{2}-t\right)^3 =\frac{(\theta-c)^3}{12\theta}-C_0.$$

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,

$$C_0<C_0'\ \Longrightarrow\ t(c,C_0,\theta)<t(c,C_0',\theta),$$ $$c<c'\ \Longrightarrow\ t(c,C_0,\theta)<t(c',C_0,\theta),$$ $$\theta<\theta'\ \Longrightarrow\ t(c,C_0,\theta')<t(c,C_0,\theta).$$

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

$$\pi_j(q,s_P,s_H)=\left(\alpha-z_j(c_P-s_P)-(c_H-s_H)-\beta\sum_iq_i\right)q_j.$$

An equilibrium is a nonnegative output vector at which no farmer gains by changing its own nonnegative output. Costs and subsidies are real-valued: the paper permits a subsidy larger than its associated cost and also permits a negative subsidy, or tax. The formulas in this mission concern equilibria at which every farmer produces a positive quantity.

To compare dispersion, let $T_k(u)$ be the sum of the $k$ largest entries of a vector $u$. A vector $u$ majorizes $v$, written $u\ge^m v$, when $T_k(u)\ge T_k(v)$ for every $k=1,\ldots,N$ and their total sums agree. The weak sub-majorization relation $u\ge_{wm}v$ keeps the top-sum inequalities and drops equal totals. With this direction, $u\ge^m v$ says that $u$ is more dispersed. These are the orders of Definition 1 in Fan et al..

Formalization targets

Active combined-subsidy equilibrium

The first milestone formalizes Proposition 3's active branch. Write $\bar z=N^{-1}\sum_jz_j$ and $\bar a(s_P,s_H)=\alpha-\bar z(c_P-s_P)-(c_H-s_H)$. At an equilibrium with every farmer active, it states

$$q_j=\frac1\beta\left(\frac{\bar a(s_P,s_H)}{N+1}-(z_j-\bar z)(c_P-s_P)\right),\qquad \pi_j=\beta q_j^2.$$

The remaining milestones formalize the increment identities written in the proof of Corollary 1 and the two order properties invoked in the proof of Proposition 2: majorization under an affine map, and weak sub-majorization under an increasing convex map. These are the results used to interpret the change in each farmer's output and profit when a subsidy changes.

Proposition 4: productivity dispersion

Consider markets $A$ and $B$ with the same $N,\alpha,\beta,c_P,c_H$, but with ratio vectors $z_A\ge^m z_B$. Give them the same subsidy $(s_P,s_H)$ and let $\delta>0$. For a vector of equilibrium outputs, $\Delta_{s_P}q$ is the difference between outputs at $(s_P+\delta,s_H)$ and $(s_P,s_H)$; $\Delta_{s_H}q$ is defined using $(s_P,s_H+\delta)$. Profit increments use the corresponding profits at those equilibria. Proposition 4 asserts

$$q_A\ge^m q_B,\quad \Delta_{s_P}q_A\ge^m\Delta_{s_P}q_B,\quad \Delta_{s_H}q_A=^m\Delta_{s_H}q_B,$$ $$\pi_A\ge_{wm}\pi_B,\quad \Delta_{s_H}\pi_A\ge^m\Delta_{s_H}\pi_B.$$

The equality $=^m$ means majorization in both directions. These comparisons form one goal theorem so every part of Proposition 4 remains present. Proposition 4, p. 13 is the source for the target.

What the result supplies

The first output comparison says that greater dispersion in input-to-output ratios leads to greater dispersion in equilibrium production under the same combined subsidy, while the total output stays equal. The increment comparisons identify which changes preserve or distinguish that dispersion when planting and harvesting payments increase. The profit statements give the corresponding order for farmer earnings. They make the distributional effect of a subsidy explicit rather than reducing it to a claim about aggregate crop supply.

A formal development supplies reusable definitions for finite majorization, this Cournot market, and best-response equilibrium. It also separates the paper's claimed order relations from the algebraic equilibrium formula. Proofs of the paper's known results remain to be checked in Lean. The mission makes no claim that Proposition 4 is an open research problem.

Why the comparison is delicate

Directly comparing farmer $j$ in the two markets cannot establish majorization: the order compares sums of the largest coordinates, which need not belong to the same farmers in each market. The sign of $c_P-s_P$ can change because planting payments are unrestricted, so the ordering of farmers by output can reverse. Profit is quadratic in output, and the profit comparison is weak sub-majorization rather than equality of totals. Subsidy increments introduce additional equilibria; an increase in the planting payment can also alter which farmers are active. These features must be accounted for in a statement that retains every clause of Proposition 4.

Formalization scope

Lean represents the paper's $N$ farmers by Fin N, so paper farmer $j$ has Lean index $j-1$. The shared parameter record contains $\alpha,\beta,c_P,c_H$; each market supplies its own sorted vector $z$. A standing predicate records $N>0$, $\alpha,\beta>0$, the ordering of $z$, and $z_j>0$. The positive-ratio condition makes explicit that each ratio is formed from positive physical quantities. The two markets have the same parameter record, and no sign restriction is imposed on costs or subsidies.

The combined payment is a per-unit-output vector $t_j=z_js_P+s_H$. Equilibrium is a best-response condition over nonnegative output, not a definition by Proposition 3's formula. The top-sum order uses all subsets of $k$ farmers, with equal total sums required for majorization. Averages range over all $N$ farmers because the theorems work in the all-active regime. This rules out treating a formula-defined output vector or a weakened order as the market result.

The goal explicitly assumes positive output at the baseline and at both shifted subsidies. Positivity at the planting-shifted subsidy is needed for the paper's fixed-active-set increment formula but is unstated in Proposition 4. Positivity at the harvesting-shifted subsidy is implied by this market model; it is kept explicit without assuming an equilibrium-uniqueness theorem. The supporting increment milestone also includes an active equilibrium at the midpoint harvesting subsidy. The majorization lemmas can be reused for other finite-vector models, and the equilibrium characterization can support later analyses of this paper's subsidy programs.

Selected references

• T. Fan, Q. Feng, Y. Li, J. G. Shanthikumar, and Y. Wu, Output-Oriented Agricultural Subsidy Design, SSRN preprint 4378693, version of March 18, 2023; forthcoming in Management Science. SSRN copy, journal DOI.

Motivation

Repair access changes more than the cost of fixing a broken product. It also changes how many used products reach a resale market, what those products sell for, and whether a manufacturer prefers to sell another new unit or earn a repair margin. Jin, Yang, and Zhu study these connected pricing decisions in a two-period durable-goods model in Right to Repair: Pricing, Welfare, and Environmental Implications. Their Proposition 1 identifies the manufacturer's prices and the resulting market outcome when independent and manufacturer repair restore the same product quality. This mission formalizes that proposition, including all seven rows of its Table 1.

The question is relevant to work on durable-goods markets because a repaired product can compete with a new one in the next period. A lower independent-repair cost can affect the manufacturer's behavior even if consumers do not choose independent repair in the final equilibrium. The paper's setting makes that effect precise through the used-product price, new-product demand, and the manufacturer's repair decision.

Setting

A new product provides one period of use and then fails with probability $f\in(0,1)$. If it remains functional, or if a failed unit is repaired, it can be used for one more period as a used product. After two periods of use it has no value. Consumers have types $\theta$ uniformly distributed on $[0,1]$. A new product gives per-period gross utility $\theta$; a functional used product gives $\delta\theta$, with $\delta\in(0,1)$. This mission takes the paper's identical-repair-quality case $\mu=\delta$ and zero resale transaction cost $\tau=0$.

The manufacturer chooses a new-product price $p_n$ and a manufacturer repair price $p_r$. Producing a unit costs $c$ and repairing it costs $c_M$. A consumer can instead pay $c_I\ge c_M$ for independent repair. A manufacturer repair price of $\infty$ means that service is unavailable. The used-product price $p_u$ emerges from the secondary market. Consumers who face a failure repair with probability $\alpha$: they repair whenever the resale gain exceeds $\min\{c_I,p_r\}$, do not repair when it falls short, and may mix at equality.

Consumers can be inactive, buy a used unit every period, or buy a new unit every period. Their corresponding per-period utilities are $0$, $\delta\theta-p_u$, and

$$\theta-p_n+(1-f)p_u+f[p_u-\min\{c_I,p_r\}]^+.$$

The thresholds $\theta_1\le\theta_2$ partition these choices. In a market with a positive used price, used demand equals the supply generated by new buyers: $\theta_2-\theta_1=(1-\theta_2)(1-f+f\alpha)$. At $p_u=0$, used supply may exceed demand. The manufacturer's per-period profit combines new-unit margin $(p_n-c)(1-\theta_2)$ with its repair margin on units it actually repairs. These primitives and Assumption 1 appear in §4.1 of the paper.

Formalization targets

Consumer behavior and reduced pricing problems

Lemma 1 states that consumer utility has the three-segment form above. The appendix then compares reduced pricing problems for no repair, full repair, and partial repair. One milestone records the full-repair optimum:

$$\max\pi_4=\frac{(c-\delta+c_Mf-1)^2}{4(1+3\delta)},\qquad p_n+fp_r=\frac{c+\delta+c_Mf+1}{2}$$

at a feasible full-repair maximizer. Other milestones record the profit-gap identities, the ordering of two production-cost cutoffs, and the appendix results for the two higher ranges of independent-repair cost. Their statements follow Online Appendix G.

Proposition 1 and Table 1

The goal is the complete equilibrium characterization of Proposition 1 and Table 1. When $c_I\ge(\delta+c_M)/2$, the optimal outcome changes at $\underline c$ and $\bar c$ from no repair to partial repair to full repair. When $c_I<(\delta+c_M)/2$, three cutoffs $\hat c_1,\hat c_2,\hat c_3$ give four rows: two no-repair regimes, partial repair, and full repair. Each row specifies $p_n^*$, $p_r^*$, $p_u^*$, and $\alpha^*$; the partial-repair rows require $0<\alpha^*<1$. The target fixes the paper's explicit formulas rather than only the number or order of the regimes.

Significance

The theorem gives a simultaneous answer for manufacturer pricing and the secondary-market outcome. It identifies when manufacturer repair is unused, offered to some consumers, or offered to all consumers facing failure. In the low-$c_I$ case it also distinguishes two no-repair regimes with different used prices. Those distinctions matter for subsequent welfare and environmental comparisons in the paper: a price change can alter new production and resale quantities even when the repair count does not change.

The paper proves Proposition 1 analytically; this mission asks for a machine-checked proof of its exact statement. A complete development would also establish reusable interfaces for a market-clearing equilibrium with a zero-price excess-supply corner, price optimization across several feasible regimes, and comparisons between algebraic cutoff formulas. The draft theorem statements are open Lean goals; the local sanity check proves that one specified market equilibrium is inhabited, not the proposition itself.

Difficulty

The manufacturer's choice affects both the direct repair margin and the resale price that determines demand for new and used goods. Optimizing the new-product price in isolation therefore does not give the global result. The appendix's candidate solutions come from distinct repair and market-clearing regimes, and their feasible sets meet at cutoffs where different prices can tie. A global claim has to compare each candidate against all admissible price pairs and their equilibria. The radical and rational cutoff formulas add boundary cases: a formula may be used only in the regime where its denominator and square-root argument have the intended meaning.

Formalization scope

Lean uses real prices, costs, probabilities, and consumer thresholds. The standing assumptions are $0<f<1$, $0<\delta<1$, $c_M\le c_I$, and the paper's Assumption 1, $c_M<\delta$ and $c<1+\delta-c_Mf$. It also pins the three unit costs to $c,c_M\ge0$, consistent with the paper's nonnegative-cost appendix domain. An unavailable manufacturer repair service is represented by none, not by an arbitrary large real number. A real repair price must be nonnegative.

The equilibrium predicate requires actual utility-maximizing consumer segments, the repair rule, and market clearing. It allows excess used-product supply only at $p_u=0$. It also admits the appendix's zero-demand outcome, in which neither product yields positive utility, no units sell, and profit is zero. An optimal outcome contains an equilibrium and beats every equilibrium at every admissible competing price pair. Thus an empty equilibrium relation cannot make the goal true. At cutoff ties the theorem asserts that the displayed prices are an optimum, without claiming uniqueness. The two partial-repair rows assert strict bounds on $\hat\alpha$, excluding a vacuous $0/0$ value.

The appendix's Problems 1, 4, and 5 are separate reduced objectives and feasible sets. The rational partial-repair objective is accompanied by its polynomial continuation for the profit-gap identity; that continuation is used only where the printed rational form could produce $0/0$. The source's second identity in (G.41) omits a factor $\delta$ in its denominator. The Lean statement uses the corrected algebraic identity, while the milestone preserves the printed line. Contributions that prove the consumer, reduced-problem, cutoff, and global-optimality milestones are all within scope. The remaining propositions on welfare, quality differences, and environmental effects are outside this mission.

Selected references

• Chenyu Jin, Lihong Yang, and Chen Zhu, Right to Repair: Pricing, Welfare, and Environmental Implications, Management Science, 2022. Authors' manuscript used here, DOI 10.1287/mnsc.2022.4401, PDF SHA-256 b869b33a21376a298a2355fb4de697d59b1362d5895f166f3255348812bc1763.

Motivation

On-demand delivery platforms for meals and groceries promise delivery within minutes, and the main operational lever they control is how a courier is dispatched. A courier can carry each order as soon as it is ready (dedicated delivery), or wait until two orders are available and deliver them in one trip (batch delivery). Batching saves travel per order but makes the first customer wait for a second order to arrive. Which mode gives the shorter wait, and hence the higher revenue, is a question practitioners face daily; it is the subject of M. Chen and M. Hu, Courier Dispatch in On-Demand Delivery (SSRN 3675063; published in Management Science, DOI 10.1287/mnsc.2023.4858).

The paper answers the question in closed form for a stylized disk model. This mission formalizes its first headline result, for the case in which the demand rate is fixed exogenously (for example by a growth target or by kitchen capacity), as stated in Propositions 1 and 2 of the authors' version dated 2022-09-21.

Setting

A vendor sits at the centre of a disk of radius $r>0$ and employs one courier with unit travel speed, so travel time equals travel distance. Customer orders arrive as a Poisson process of rate $\lambda>0$, the demand rate, and each customer's location is independent and uniformly distributed on the disk.

Under dedicated delivery each trip is a round trip to one customer, of length $X_D=2\|U\|$ with $U$ uniform on the disk. Its moments are $\mathbb E[X_D]=\tfrac43 r$ and $\mathbb E[X_D^2]=2r^2$, so the courier is an M/G/1 server with

$$\mu_D=\frac{3}{4r},\qquad C_D=\frac98 ,$$

where $\mu_D$ is the service rate and $C_D$ the summed coefficients of variation. The paper defines the expected wait under dedicated delivery as the M/G/1 in-line delay

$$W_D(\lambda,\mu,C)=\frac{\lambda}{\mu(\mu-\lambda)}\cdot\frac C2 .$$

Under batch delivery the courier leaves only with two orders and visits both, so a trip has length $X_B=\|U\|+\|U-U'\|+\|U'\|$ for two independent uniform points, with $\mathbb E[X_B]=\big(\tfrac{128}{45\pi}+\tfrac43\big)r$. This gives

$$\mu_B=\frac{45\pi}{4r(32+15\pi)},$$

and a variability coefficient $C_B\approx 0.583$ that the paper obtains by numerical integration. The paper defines the batch wait as the time for a second order to arrive, plus Kingman's approximation of the E$_2$/G/1 in-line delay, plus the expected delay of being second in a batch:

$$W_B(\lambda,\mu,C)=\frac1{2\lambda}+\frac{\lambda}{\mu(2\mu-\lambda)}\cdot\frac C2+\frac r3 .$$

Customers have valuations with c.d.f. $F$ on $[0,1]$ and a wait cost $c>0$ per unit time; at price $p$ the potential arrival rate $\Lambda r^2$ thins to $\lambda$. The vendor's revenue rate at demand rate $\lambda$ and expected wait $w$ is

$$V(\lambda,w)=\lambda\Big[F^{-1}\Big(1-\frac{\lambda}{\Lambda r^2}\Big)-c\,w\Big].$$

Dedicated delivery is stable exactly when $\lambda r<\tfrac34$; batch delivery when $\lambda r<T_2=\frac{45\pi}{2(32+15\pi)}\approx0.893$.

Formalization targets

Goal: one threshold in $\lambda r$ (Propositions 1 and 2)

For every $C_B\in[0.58,0.59]$ there is a constant $a_1\in(0,\tfrac34)$ such that for all $r>0$, $\lambda>0$ with $\lambda r<\tfrac34$,

$$W_D(\lambda,\mu_D,C_D)<W_B(\lambda,\mu_B,C_B)\iff \lambda r<a_1,\qquad W_B(\lambda,\mu_B,C_B)<W_D(\lambda,\mu_D,C_D)\iff \lambda r>a_1,$$

and the same two equivalences hold for the revenues $V(\lambda,W_D)$ and $V(\lambda,W_B)$, for every $F^{-1}$, every $\Lambda>0$ with $\lambda\le\Lambda r^2$, and every $c>0$. The paper reports $a_1\approx0.5689$; the goal asserts only the existence and the location in $(0,\tfrac34)$.

Milestones

1. The dedicated trip moments $\mathbb E[X_D]=\tfrac43r$, $\mathbb E[X_D^2]=2r^2$, and the resulting $\mu_D$, $C_D$ (display (3)).
2. The mean batch trip $\mathbb E[X_B]=(\tfrac{128}{45\pi}+\tfrac43)r$ and the resulting $\mu_B$ (display (8), first moment).
3. The reduction (A.1): $W_D(\lambda,\mu_D,C_D)-W_B(\lambda,\mu_B,C_B)=f_A(\lambda r)/\lambda$ for an explicit rational function $f_A$ of one variable.
4. The single crossing: $f_A$ has exactly one zero $a_1$ on $(0,\tfrac34)$, negative before and positive after, with $0.56<a_1<0.58$.
5. Proposition 1: for each $r$, a threshold $\lambda_{ex}\in(0,\mu_D)$ in the demand rate.
6. Proposition 2: for each $\lambda$, a threshold $r_{ex}\in(0,\tfrac3{4\lambda})$ in the radius.

Significance

The result says that, with demand fixed, the choice between dedicated and batch delivery depends on the market only through the product $\lambda r$: dedicated delivery is better when demand is low or the area small, batching when demand is high or the area large. The threshold is a single universal number, independent of the valuation distribution and of the wait-cost rate, because at a fixed demand rate the strategy with the shorter wait always earns more. This is the efficiency-driven benchmark against which the paper's second main result (endogenous demand in a crowded market, where the order reverses) is contrasted.

To our knowledge none of this has been machine-checked. The mission produces a checked version of the paper's closed-form comparison and, in milestones 1–2, checked computations of classical geometric-probability moments of the disk (the mean distance $128r/(45\pi)$ between two uniform points). The paper's own argument for the single crossing is numerical ("solved using standard methods"); a formal proof must replace it by an exact argument with rigorous bounds on $\pi$.

Difficulty

The reduction to one variable is algebra. The difficulty is the sign analysis of $f_A$ on $(0,\tfrac34)$: it is a difference of two rational functions with poles at $\tfrac34$ and $T_2\approx0.893$, involving $\pi$, and clearing denominators gives a cubic whose roots the paper only reports numerically. The natural first idea, showing $f_A$ is monotone on the whole interval, does not apply directly, since $f_A$ starts at $-\tfrac12$, first decreases, and only later rises to $+\infty$; a proof must establish that it crosses zero exactly once. A further point is that $C_B$ is not a closed-form number, so the crossing must be shown uniformly over an interval of values.

The moment milestones need integration in polar coordinates on the plane; the mean distance between two uniform points of a disk is a classical but nontrivial four-dimensional integral.

Formalization scope

All objects live in the namespace CourierDispatch.Exogenous. Real numbers are ℝ, $\lambda$ is lam, $\Lambda$ is Lam, and $F^{-1}$ is an arbitrary function Q : ℝ → ℝ (no property of it is needed, since at equal $\lambda$ the price terms cancel). The plane is EuclideanSpace ℝ (Fin 2) and the uniform law on the disk is Lebesgue measure conditioned on the closed ball.

Committed conventions:

• The expected waits are the paper's closed-form formulas (5) and (12): the M/G/1 in-line delay for dedicated delivery and Kingman's approximation for the E$_2$/G/1 batch queue. The paper introduces them as definitions ("$:=$"), and the mission does not formalize the queues behind them; no statement here is about the true stationary delay of an E$_2$/G/1 queue.
• $C_B$ is a real parameter with the standing hypothesis $0.58\le C_B\le 0.59$, which contains the paper's value $0.583$ and a Monte-Carlo estimate $0.58297$.
• Every comparison is restricted to $r>0$, $\lambda>0$, $\lambda r<\tfrac34$, the range where both queues are stable; above it only batch delivery is defined and the paper makes no comparison. This also keeps every formula away from Lean's junk values for division by zero.
• Revenue comparisons additionally require $\Lambda>0$ and $\lambda\le\Lambda r^2$, the effective-demand range in §3, p. 8. The arbitrary function Q stands for $F^{-1}$; its properties cancel when the two strategies are compared at the same demand rate.
• Both directions of each threshold are stated as strict equivalences, so equality at $\lambda r=a_1$ follows.

The threshold $a_1$ (and $\lambda_{ex}$, $r_{ex}$) is existential in every statement; it is never a definition and never an infimum of a sign set, and $W_D$, $W_B$ are never defined through $f_A$, so the goal cannot be made true by construction.

Needed infrastructure: polar-coordinate integration on the plane (Mathlib's integral_comp_polarCoord_symm), and rigorous rational bounds on $\pi$ (Real.pi_gt_d6, Real.pi_lt_d6). The goal does not depend on the moment milestones 1–2, which ground the constants $\mu_D$, $C_D$, $\mu_B$ in the geometry of the disk and are welcome as separate contributions.

Selected references

• M. Chen, M. Hu, Courier Dispatch in On-Demand Delivery, SSRN 3675063, version of 2022-09-21; Management Science, 2023. https://ssrn.com/abstract=3675063, https://doi.org/10.1287/mnsc.2023.4858
• J. F. C. Kingman, On queues in heavy traffic, Journal of the Royal Statistical Society B 24 (1962). https://doi.org/10.1111/j.2517-6161.1962.tb00465.x
• H. Solomon, Geometric Probability, SIAM CBMS-NSF Regional Conference Series 28, 1978. https://doi.org/10.1137/1.9781611970418
• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651

Motivation

Best subset selection fits a linear model $y\approx X\beta$ using at most $k$ of the $p$ available features: it minimizes the residual sum of squares subject to the sparsity constraint $\|\beta\|_0\le k$, where $\|\beta\|_0$ counts the nonzero coordinates of $\beta$. Mazumder, Radchenko and Dedieu (arXiv:1708.03288v4; Operations Research, 2023) show that best subsets overfits when the signal-to-noise ratio is low, and propose adding a shrinkage penalty $\lambda\|\beta\|_q$ with $q\in\{1,2\}$ to the same constrained problem. Their statistical results (oracle inequalities, a lower bound for best subsets, a BIC-type choice of $k$) are the subject of the companion missions II–VI of this series.

The estimator is a mixed-integer program. To compute it in practice, and to warm-start the mixed-integer solver that certifies optimality, the paper uses a discrete first-order (DFO) method: a proximal-gradient iteration in which the proximal step is a projection-like operation onto the set of $k$-sparse vectors with a norm penalty. The method descends from iterative hard thresholding (Blumensath & Davies, 2009), from proximal gradient methods for composite problems (Nesterov, 2013), and from the discrete first-order algorithms of Bertsimas, King and Mazumder (Annals of Statistics, 2016). This mission formalizes the paper's convergence guarantee for it, Proposition 2.

Setting

Vectors live in $\mathbb R^p$ with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|_2$. Write $\|\beta\|_0$ for the number of nonzero coordinates and $\|\beta\|_1=\sum_i|\beta_i|$. For $q\in\{1,2\}$ the penalty is the norm $\|\beta\|_q$ itself, not its $q$-th power.

Let $f:\mathbb R^p\to\mathbb R$ be a differentiable convex function whose gradient is $L_0$-Lipschitz:

$$\|\nabla f(\beta)-\nabla f(\alpha)\|_2\le L_0\|\beta-\alpha\|_2\qquad\forall\,\beta,\alpha .$$

The motivating case is $f(\beta)=\tfrac12\|y-X\beta\|_2^2$ with $L_0=\sigma_{\max}(X)^2$. The composite problem (7) is

$$\text{minimize}\quad F(\beta):=f(\beta)+\lambda\|\beta\|_q\quad\text{s.t.}\quad\|\beta\|_0\le k .$$

For $L\in\mathbb R$ the quadratic model of $f$ around $\alpha$ is

$$Q_L(\beta;\alpha)=f(\alpha)+\langle\nabla f(\alpha),\beta-\alpha\rangle+\tfrac L2\|\beta-\alpha\|_2^2 ,$$

and the thresholding operator is the set of minimizers

$$\mathrm S(u;k;\mu\ell_q)=\operatorname*{arg\,min}_{\|b\|_0\le k}\ \tfrac12\|b-u\|_2^2+\mu\|b\|_q ,$$

which can contain several points when the $|u_j|$ have ties. A DFO sequence with constant $L>0$ starts at a $k$-sparse $\beta^{(1)}$ and, for $m\ge1$, picks any

$$\beta^{(m+1)}\in\mathrm S\Big(\beta^{(m)}-\tfrac1L\nabla f(\beta^{(m)});\,k;\,\tfrac\lambda L\ell_q\Big).$$

Formalization targets

Goal: Proposition 2 (p. 10)

Assume in addition $f\ge0$ and $\lambda\ge0$. For every DFO sequence:

(a) if $L\ge L_0$, then $F(\beta^{(m)})$ is non-increasing in $m\ge1$ and converges to some $F^*\ge0$;

(b) if $L>L_0$, then for every $M\ge1$

$$\min_{1\le m\le M}\|\beta^{(m+1)}-\beta^{(m)}\|_2^2\le\frac{2\big(F(\beta^{(1)})-F^*\big)}{M(L-L_0)} .$$

The statement holds for any $f$ of the stated class and any choice in the set-valued operator; nothing about least squares is assumed.

Milestones (proof in Supplement A.1, p. 35)

1. (9), p. 8: $f(\beta)\le Q_L(\beta;\alpha)$ for all $\alpha,\beta$ and every $L\ge L_0$, the bound the paper takes from Nesterov (2004).
2. (20)–(21), p. 35: completing the square, $Q_L(\eta,\beta)+\lambda\|\eta\|_q=\tfrac L2\|\eta-(\beta-\tfrac1L\nabla f(\beta))\|_2^2-\tfrac1{2L}\|\nabla f(\beta)\|_2^2+f(\beta)+\lambda\|\eta\|_q$. Hence the minimizers of $Q_L(\cdot,\beta)+\lambda\|\cdot\|_q$ over $\|\eta\|_0\le k$ are exactly $\mathrm S(\beta-\tfrac1L\nabla f(\beta);k;\tfrac\lambda L\ell_q)$.
3. (22), p. 35: for $\|\beta\|_0\le k$ and $\hat\eta$ in that set, $F(\beta)\ge\tfrac{L-L_0}2\|\hat\eta-\beta\|_2^2+F(\hat\eta)$.
4. (23) and the next display, p. 35: summed over $m=1,\dots,M$,

$$F(\beta^{(1)})-F(\beta^{(M+1)})\ge\tfrac{M(L-L_0)}2\min_{m\le M}\|\beta^{(m+1)}-\beta^{(m)}\|_2^2 .$$

5. Proposition 1, p. 9 (companion, not used by the goal): every $\hat\beta\in\mathrm S(u;k;\lambda\ell_q)$ keeps the $k$ largest entries of $u$ in magnitude, for some ordering of ties. For $q=1$ it soft-thresholds them coordinatewise, and for $q=2$ it shrinks them as a group by $\max\{\tau_u-\lambda,0\}/\tau_u$, with $\tau_u$ the norm of those $k$ entries.

Significance

Proposition 2 is what makes the DFO method a sound component of the paper's computational pipeline. The objective values never increase, so every iterate is a feasible point at least as good as the warm start. Part (b) says that the step length $\|\beta^{(m+1)}-\beta^{(m)}\|_2^2$ is small after $O(1/\epsilon)$ iterations. A point whose step vanishes is a fixed point of the update, which the paper calls a first-order stationary point (Definition 1). The stopping rule of the algorithm ($\|\beta^{(m+1)}-\beta^{(m)}\|_2^2\le\tau$) is therefore reached in at most $\lceil 2(F(\beta^{(1)})-F^*)/(\tau(L-L_0))\rceil$ steps.

The result is proved in the paper, in half a page that defers its central inequality (22) to Proposition 6 of Bertsimas, King & Mazumder (2016). It has not been formalized. A machine-checked version produces three reusable pieces: a descent lemma for functions with Lipschitz gradient on $\mathbb R^p$, the variational characterization of the sparse proximal step, and a sufficient-decrease-to-rate argument for any descent method. These are the same pieces that iterative hard thresholding, proximal gradient, and block-coordinate methods for $\ell_0$ problems need.

Difficulty

The difficulty is moderate, and it lies in the infrastructure rather than in any single step. The descent lemma (9) needs the fundamental theorem of calculus along a segment for a function on a Euclidean space, combined with the Lipschitz bound on the gradient. The feasible set $\{\|\beta\|_0\le k\}$ is not convex, so no convex-analysis argument (subgradient optimality, firm nonexpansiveness of a proximal map) applies to the thresholding step. Inequality (22) must instead be obtained by comparing the minimizer $\hat\eta$ with the feasible competitor $\beta$ itself, which is why the hypothesis $\|\beta\|_0\le k$ appears. Part (a) also needs a lower bound on $F$ for its limit to exist and be nonnegative, which the general class of $f$ does not provide on its own.

Formalization scope

$\mathbb R^p$ is EuclideanSpace ℝ (Fin p), the gradient is Mathlib's gradient f, and coordinates are $0$-based. Membership in $\mathrm S(u;k;\mu\ell_q)$ is a predicate: feasibility plus minimality against every $k$-sparse competitor. No selection from the set is fixed, and existence of minimizers is not assumed. A DFO sequence is any β : ℕ → ℝᵖ satisfying the update for every $m\ge1$, indexed from $1$ as printed. The stopping rule and the support-restricted polishing Step 2 are not part of it. The penalty is $\|\cdot\|_1$ for $q=1$ and the Euclidean norm for $q=2$, and every theorem assumes $q\in\{1,2\}$ and $k\ge1$. The minimum over $1\le m\le M$ is a finite infimum over a nonempty index set.

Three hypotheses are added to Proposition 2 as printed, each disclosed in the item. The proof's claim "$F(\beta)\ge0$" is false for a general convex $f$ with Lipschitz gradient ($f(\beta)=-\beta_1$ sends $F$ to $-\infty$), so $f\ge0$ and $\lambda\ge0$ are assumed. The update divides by $L$, and $L\ge L_0$ allows $L=0$, so $L>0$ is assumed. "Decreasing" is read as non-increasing. Convexity of $f$ is kept as in the paper's setting (7)–(8), though only the gradient bound is used. Proposition 1 is stated with an existential ordering: for a fixed sorting permutation the printed claim fails under ties.

The statement cannot be trivialized by restricting $f$ or the run. The goal quantifies over every $f$ of the class and every sequence obeying the update, the limit $F^*$ in (b) is the actual limit of the objective values, and the rate holds for every $M\ge1$. Not formalized here: the mixed-integer formulations, the continuation and local-search heuristics of §2.4, Definition 1, and the paper's statistical results (missions II–VI). Contributions of reusable infrastructure, such as a general descent lemma or a lemma turning summed decrease into a $1/M$ rate, are welcome as separate theorems.

Selected references

• R. Mazumder, P. Radchenko, A. Dedieu, Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low, arXiv:1708.03288v4, 2022; Operations Research 71(1), 2023. https://arxiv.org/abs/1708.03288v4
• D. Bertsimas, A. King, R. Mazumder, Best Subset Selection via a Modern Optimization Lens, Annals of Statistics 44(2), 2016. https://doi.org/10.1214/15-AOS1388
• Y. Nesterov, Gradient Methods for Minimizing Composite Functions, Mathematical Programming 140, 2013. https://doi.org/10.1007/s10107-012-0629-5
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• T. Blumensath, M. E. Davies, Iterative Hard Thresholding for Compressed Sensing, Applied and Computational Harmonic Analysis 27(3), 2009. https://doi.org/10.1016/j.acha.2009.04.002