All missions

Motivation

Online retailers and service providers quote a promised delivery time and are judged on how often they meet it. Platforms increasingly publish delivery-performance information, such as on-time ratings or conformance scores, so that consumers can weigh a quoted time against the firm's record. Producing accurate information is costly: the firm must track deliveries, audit ratings and present them clearly. Whether a firm should pay for precise information, or let consumers infer its reliability from noisy signals, is a question for operations management (capacity, lead-time quotation) and for marketing (pricing, information disclosure) at once.

Leng, Becerril-Arreola, Parlar and Ferguson (MSOM 2024; the mission follows the authors' preprint of April 2nd, 2023) model a firm that jointly sets a price, a promised delivery time and an effort toward the quality of its conformance information, facing consumers who care about all three. Their central analytical result, Theorem 1, says the firm should never invest partially: the optimal effort is either none or full.

The model joins two lines of work. The first is joint price and delivery-time decisions with congestion, as in So (2000), Liu, Parlar and Zhu (2007) and Boyaci and Ray (2006), where delivery reliability enters demand. The second is logit demand from discrete-choice theory (Anderson, de Palma and Thisse 1992), where the scale parameter measures how dispersed consumers' valuations are.

Setting

A firm serves consumers at service rate $\mu$. It sets a price $p$, a promised delivery time $t$, and an information-quality effort $\phi\in[0,1]$. The market has size $\Lambda$. Each consumer compares the firm with an outside option of deterministic utility $V_e$.

If consumers arrive at rate $l$, the firm operates as an M/M/1 queue, and an order is delivered within the promised time with probability

$$q=1-e^{-(\mu-l)t}\qquad\text{(eq. (1))}.$$

The deterministic utility of buying is

$$V=\alpha-p+\beta_r\rho\,q-\beta_t t\qquad\text{(eq. (4))},$$

where $\alpha$ is the base value, $\beta_r$ and $\beta_t$ are the sensitivities to the conformance score and to the promised time, and $\rho$ scales the score. Effort narrows the dispersion of consumers' inferences: the utility shock has scale

$$\omega_\theta(\phi)=\sqrt{\beta_r^2(1-\phi^2)+\omega_Y^2}\qquad\text{(eq. (6))},$$

decreasing from $\sqrt{\beta_r^2+\omega_Y^2}$ at $\phi=0$ to $\omega_Y$ at $\phi=1$.

The demand rate $\lambda(p,t,\phi)$ is the logit share times the market size (eqs. (8)–(9)):

$$\lambda=\frac{\Lambda}{1+\exp[-(V-V_e)/\omega_\theta]}.$$

Since $V$ depends on $\lambda$ through $q$, this is a fixed-point equation in $\lambda$. The firm earns

$$\Pi(p,t,\phi)=\lambda(p,t,\phi)\,(p-b\phi-c)\qquad\text{(eq. (11))},$$

with unit cost $c$ and unit effort cost $b$. A plan $(p,t)$ is feasible when $p\ge c$, $t\ge 0$ and $(\mu-\lambda)t\ge1$. The optimal profit $\Pi^*(\phi)$ is the supremum of $\Pi$ over feasible plans, $\lambda^*(\phi)$ and $V^*(\phi)$ are the demand and utility at the optimal plan, and the gap

$$h(\phi)=\frac{b\,\omega_\theta}{\beta_r^2\phi}-\frac{V^*(\phi)-V_e}{\omega_\theta}$$

measures by how much Lemma 2's condition (19) holds. With $\bar S(\phi)$ the largest attainable market share (eq. (10)), the capacity condition (16) is $\mu\ge\bar S\Lambda+(\beta_t/(\beta_r\rho))\,e$.

Formalization targets

Goal: Theorem 1 (p. 15)

Let $V_1=V^*(1)$. If

$$\frac{b\,\omega_Y^2}{\beta_r^2}\;\ge\;V_1-V_e\qquad\text{(23)},$$

then $\Pi^*$ is strictly decreasing on $[0,1]$ and $\phi^*=0$ is the unique optimum. Otherwise $\Pi^*$ strictly decreases and then strictly increases, with the turn at some $\phi_0\in(0,1)$. In both cases

$$\Pi^*(\phi)<\max\{\Pi^*(0),\Pi^*(1)\}\qquad\text{for all }\phi\in(0,1).$$

Milestones

1. Eq. (10): $\lambda(p,t,\phi)\le\bar S(\phi)\Lambda$.
2. Lemma 1, item 2: the optimal plan exists, is unique, and solves the first-order equations (13)–(14).
3. Lemma 2, item 1 (profit part): if (19) holds at $\phi$, then $\Pi^*$ has non-positive derivative there.
4. Lemma 2, item 2 (demand and profit parts): if (19) fails at $\phi$, then $\lambda^*$ and $\Pi^*$ have positive derivatives there.
5. $h(\phi)\to+\infty$ as $\phi\to0^+$ (p. OA-7).
6. Eq. (35): $h'(\phi_0)<0$ wherever $h(\phi_0)<0$ (p. OA-8).
7. Single crossing: $h(\phi_0)<0$ implies $h<0$ on $[\phi_0,1)$ (pp. OA-8 – OA-9).
8. $h(1^-)=b\omega_Y/\beta_r^2-(V_1-V_e)/\omega_Y$, so (23) holds exactly when $h(1^-)\ge0$ (p. OA-9).

Three supporting items have no counterpart in the paper. They state that the demand fixed point is well posed, that $\Pi^*$ is continuous on $[0,1]$, and the envelope identity $d\Pi^*/d\phi=-(\lambda^*\beta_r^2\phi/\omega_\theta)\,h(\phi)$.

Significance

Theorem 1 is a bang-bang result. A firm choosing how much to spend on delivery-performance information should consider only two options, no effort and full effort, and condition (23) gives a closed-form test for when no effort is optimal. The paper's sensitivity results (Corollaries 1–4) and its numerical study are all built on this reduction, since they compare the two endpoint regimes using the closed forms in Table 1.

The result has an analytical proof in the paper's online appendix, but no machine-checked proof. The formalization adds a precise statement of the model's well-posedness: the demand is a fixed point, and the optimal plan exists and is unique. It also makes the comparative statics explicit. Parts of Lemma 2 as printed are false, namely the directions of $t^*$ and $\lambda^*$ in item 1 and of $p^*$ and $V$ in item 2, and the mission states only the parts that hold. A complete development would certify which of the paper's conclusions survive and by which argument.

Difficulty

The optimal profit $\Pi^*(\phi)$ is the value of a two-dimensional optimization whose objective is defined through an implicit equation, since demand appears on both sides of the logit formula. Differentiating $\Pi^*$ in $\phi$ requires an envelope argument over a constrained problem. That in turn requires knowing that the optimum is interior, unique and a smooth function of $\phi$, and that the queue constraint $(\mu-\lambda)t\ge1$ does not bind.

The single-crossing step is the delicate one. The paper reaches it through a derivative of $\lambda^*$ with respect to $\omega_\theta$ (eqs. (30)–(34)) whose sign claims are partly wrong. The tempting shortcut, to read the sign of $\Pi^{*\prime}$ off the sign of $\lambda^{*\prime}$, is unsound: when (19) holds, $\lambda^*$ can rise while $\Pi^*$ falls.

Formalization scope

Everything is real-valued and lives in the namespace DeliveryDisclosure.InfoEffort. A structure Params holds $\Lambda,\alpha,\beta_r,\beta_t,\rho,V_e,\omega_Y,\mu,c,b$, and the predicate Standing bundles the standing assumptions. The paper writes $\beta_r,\beta_t\ge0$ but divides by them, so Standing requires $\Lambda,\beta_r,\beta_t,\rho,\omega_Y,b>0$, together with $c\ge0$ and condition (16) for every $\phi\in[0,1]$.

• The logit demand (8)–(9) with scale (6) is the primitive. The paper derives it from a Gumbel-plus-$C(\phi)$ decomposition of the utility shock that holds only when $\omega_Y=\phi\beta_r$. Every result from (8) on uses only the logit formula, so neither Claim 1 nor the $C(\phi)$ distribution is formalized.
• Demand is the supremum of the $l\in[0,\Lambda]$ below the logit right-hand side, which is the unique fixed point for $t\ge0$. The function Real.sigmoid gives the logit share.
• The shortest delivery time is $\underline t=0$, so $\bar V=\alpha-c+\beta_r\rho$.
• Effort ranges over the closed interval $[0,1]$. The paper's $0^+$ and $1^-$ are its endpoints, and $V_1$ is $V$ at the $\phi=1$ optimum.
• $\Pi^*$ is the supremum over all feasible plans, not a closed form or a solution of (13)–(14).
• $h$ divides by $\phi$, so it is used only on $(0,1]$.

$\Pi^*$ is defined as a supremum over all feasible plans and $h$ uses $V$ at the optimum, which rules out a trivializing formalization: $\Pi^*$ cannot be replaced by Table 1's closed forms, by profit at a fixed plan, or by a demand with the conformance frozen. Lemma 1's corner case (item 1), Claim 1, Remarks 1–5, Table 1 and Corollaries 1–4 are not formalized.

A complete development needs implicit differentiation of a fixed point, an envelope theorem for a two-variable constrained maximization, and existence of maximizers on a non-compact feasible set. These ingredients apply to other congestion-pricing and logit-demand models. Contributions toward any milestone are welcome, as are proofs of the supporting items.

Selected references

• M. Leng, R. Becerril-Arreola, M. Parlar, M. Ferguson, Disclosing Delivery Performance Information When Consumers Are Sensitive to Promised Delivery Time, Delivery Reliability, and Price, Manufacturing & Service Operations Management, 2024 (authors' preprint, April 2nd, 2023). https://doi.org/10.1287/msom.2023.0223
• K. C. So, Price and time competition for service delivery, Manufacturing & Service Operations Management 2(4):392–409, 2000.
• L. Liu, M. Parlar, S. X. Zhu, Pricing and lead time decisions in decentralized supply chains, Management Science 53(5):713–725, 2007.
• T. Boyaci, S. Ray, The impact of capacity costs on product differentiation in delivery time, delivery reliability, and price, Production and Operations Management 15(2):179–197, 2006.
• S. P. Anderson, A. de Palma, J.-F. Thisse, Discrete Choice Theory of Product Differentiation, MIT Press, 1992.
• N. S. Cardell, Variance components structures for the extreme-value and logistic distributions with application to models of heterogeneity, Econometric Theory 13(2):185–213, 1997.

Motivation

A firm can have valuable operations yet fail when a temporary cash shortfall leaves it unable to pay its bills. Cash reserves protect the firm, but holding them is costly. In Lee and Rivera’s study, the manager also doubts the probability model for future shocks. The manager evaluates a policy under the least favorable model within a prescribed set of plausible models. This makes the composition of pessimism a decision linked to the firm’s cash position. The paper’s central qualitative claim is that adverse beliefs respond to recent shocks in a way resembling extrapolation bias: a recent shock changes the manager’s assessment of future shocks of the same type.

The result belongs to the paper’s 2019 working version, Extrapolation Bias and Dynamic Liquidity Management. The later Management Science article has a different title. The theorem and equation numbers here refer to the working version, especially §2, §3.3, §4.1 and Appendix A.

Setting

The firm has a positive size δ and cash reserves M. Its cash ratio is m=M/δ. The manager chooses an investment rate i, which raises expected size growth but incurs an expenditure g(i)=i+θi²/2. The size process has a permanent shock with volatility σδ; operating cash flow has an independent temporary shock with volatility σY. The manager discounts at rate r. Cash earns r−λ, so λ is its carry cost. At cash exhaustion the firm either issues equity, paying proportional and fixed costs ρ₁ and ρ₀, or liquidates for a fraction ω of the ambiguity-only benchmark value δqᴬ. These objects and their cash-management interpretation follow the working paper’s model and HJB equations.

The manager allows drift changes h=(hᴾ,hᵀ) in an ambiguity ellipse,

$$H=\{h:(h^P/\kappa_P)^2+(h^T/\kappa_T)^2\leq1\}.$$

The superscripts P and T mean permanent and temporary. The two radii κP and κT limit how much each drift can be distorted. A distortion h changes expected size growth by σδhᴾ and expected cash flow by σYhᵀ. The manager chooses i against the least favorable h. On the ellipse boundary, the model writes hᴾ=−κP cos φ and hᵀ=−κT sin φ for an angle φ in [0,2π].

The paper uses a scaled value function F: firm value at size δ and cash M is δF(M/δ). In the no-payout region 0≤m≤m*, F satisfies the max-min Hamilton–Jacobi–Bellman equation (25), with payout boundary m*. The conditions at m=0 compare refinancing with liquidation, and the value is linear in cash above m*. The ambiguity-only benchmark qᴬ is determined by the paper’s equations (36)–(38). For an increasing concave F, the worst-case angle and distortions are defined by (26)–(27).

Formalization targets

Main claim: endogenous extrapolation bias

For every cash ratio in the no-payout region, the angle from (26) is the unique minimizer of the HJB expression among admissible angles. Its associated worst-case distortions satisfy four shock-response inequalities:

$$S_{PP}(m)\geq0,\qquad S_{PT}(m)\leq0,\qquad S_{TP}(m)\leq0,\qquad S_{TT}(m)\geq0 \quad(0\leq m\leq m^*).$$

Here the first subscript names the belief component and the second names the shock. The four coefficients are the derivatives in the display on p. 21, multiplied by the corresponding shock loading of the cash ratio. When F″(m)<0, the temporary-shock inequalities are strict. The permanent-shock inequalities are strict when also m>0. This states the paper’s §4.1 claim at the boundaries where its printed strict wording would otherwise fail.

Supporting results

The attack path follows four statements in the working paper: Lemma 4 equates minimization over the filled ellipse with minimization over its angle-parametrized boundary; Proposition 3 (19) gives the investment and belief-allocation conditions for the two-state HJB; equations (26)–(27) give their scaled counterparts; and §4.1 describes how beliefs change as the cash ratio rises. The milestone list retains the printed passages verbatim and identifies the necessary corrections in its titles.

Significance

The result identifies which adverse cash-flow model the manager uses at a given cash position. With little cash, temporary losses can force costly financing or liquidation, and the adverse model weighs them more heavily. With more cash, the adverse model shifts toward permanent shocks to firm size. The sign pattern translates that change in beliefs into responses to realized shocks. It supplies a precise meaning for the paper’s claim of endogenous extrapolation bias within this cash-management model.

The paper gives analytical HJB conditions and illustrates the time-varying beliefs in Figure 4.1. This mission asks for Lean proofs of the qualitative allocation and sensitivity statements for the paper’s stated variational system. The local formalization records three corrections to the working paper’s formulas and prose, so solvers have a single explicit target rather than relying on incompatible printed expressions.

Difficulty

The obvious appeal to worst-case beliefs does not by itself establish which point of the ellipse minimizes the HJB expression, whether that point is unique, or whether its angle remains in the required quadrant. The HJB also mixes investment and belief allocation, while the target concerns derivatives of the belief allocation with respect to the cash ratio. Finally, the printed strict signs fail at m=0 and at a smooth payout boundary where F″(m*)=0. The theorem must account for both endpoints while preserving the paper’s interior claim.

Formalization scope

Lean represents parameters in a structure, the ellipse as a subset of ℝ×ℝ, and F as a global C² real function restricted to nonnegative cash. The scaled solution predicate includes monotonicity, concavity, the attained max-min equation (25), and the boundary conditions (28)–(31). The HJB angle interval is the closed [0,2π] of (25). No real supremum of an empty or unbounded set is used. The benchmark predicate records (36)–(38) and the positive transversality gap r−µ−iᴬ.

The working paper has three relevant slips. Lemma 4’s h-form HJB omits the volatility multipliers present in (11)–(12), so the formal statement restores them and uses the paper’s γ=2 restriction. Proposition 3 (19) prints an extra δ in the investment condition; the formal statement uses the condition implied by (18). The last sentence of §4.1 p. 20 reverses the belief monotonicity directions implied by the preceding prose and the p. 21 sensitivity display; the formal statement follows the latter. Strictly positive κP, κT, σY, ω and qᴬ specify the nondegenerate regime in which the arctangent formula and liquidation value carry their intended meaning.

The scaled solution predicate prevents an arbitrary concave function from replacing the paper’s value function. The target requires the displayed angle to be the actual unique minimizer of (25), and its divisions have positive denominators under the model assumptions. Reusable work includes the ellipse minimization and real-analysis facts behind the angle’s monotonicity. Contributions proving these milestones or the final sensitivity theorem are within scope.

Selected references

• S. Lee and A. Rivera, Extrapolation Bias and Robust Dynamic Liquidity Management, Management Science, 2021. DOI: 10.1287/mnsc.2020.3765. This mission cites the authors’ working version, Extrapolation Bias and Dynamic Liquidity Management, dated May 24, 2019; its pagination and numbering govern every milestone.

Motivation

Humanitarian organizations (HOs) have long helped refugees with in-kind assistance: food, hygiene and shelter items bought at wholesale cost and handed out. Cash assistance, money that refugees spend at local stores, has grown quickly. In 2014 it was 6% of the $25 billion of humanitarian assistance worldwide; by 2019, cash and vouchers were 18% (High Level Panel on Humanitarian Cash Transfers 2015; Jódar Vidal et al. 2020, both as cited by Kotsi, Wu and Pedraza-Martinez). Cash lets refugees buy what they need and brings revenue to the host community. It also creates demand that a local retailer with market power can exploit: field reports from Swaziland and Uganda describe price increases after cash programmes began, and UNHCR advises in-kind assistance "where increased demand on markets will cause inflation".

Kotsi, Wu and Pedraza-Martinez (MSOM 24(6), 2022) model this as a game between an HO and a monopolist retailer. Without intervention the retailer answers cash assistance by raising its price above the monopoly price it charged before the refugees arrived. That hurts local residents and reduces the quantity of goods refugees receive. The paper then designs interventions run by an HO-government partnership. One of them is price-dependent cash assistance (PDCA): the HO announces how much cash it will give as a function of the retailer's prices. This mission formalizes the paper's result that a correctly designed PDCA schedule makes a chosen target price the retailer's own optimal choice.

Setting

An HO has budget $B > 0$. It gives a fraction $k \in [0,1]$ to the refugees as cash and spends the rest on goods bought at unit cost $c > 0$. A monopolist retailer buys at the same unit cost $c$ and sets the retail price.

In the symmetric-goods case every good has the same cost $c$ and price $p$, and $D(p)$ is the local residents' aggregate demand. Refugees spend their cash $kB$ in full, buying $Q(p,k) = kB/p$ units. The retailer's profits from refugees and from residents are

$$\pi_r(p,k) = (p-c)\,Q(p,k) = kB\Big(1-\frac cp\Big), \qquad \pi_0(p) = (p-c)\,D(p),$$

and its total profit is $\Pi(p,k) = \pi_r(p,k) + \pi_0(p)$. Assumption 2 of the paper: $D$ is continuously differentiable, $D'(p) \le 0$ on $(c, p_{\max})$ where $D(p_{\max}) = 0$, and $\pi_0$ is unimodal with unique maximizer $p_0$. The pre-arrival maximum profit is $\Pi_0 = \pi_0(p_0)$.

The HO-government partnership picks a target $(p^\odot, k^\odot)$. It is feasible if the retailer earns at least its old profit, $\Pi(p^\odot, k^\odot) \ge \Pi_0$, and residents are no worse off, which the paper writes as $p^\odot \le p_0$. The symmetric PDCA scheme (equation (27)) pays the cash fraction

$$k(p) = \min\Big\{\big(k^\odot + S(p^\odot,k^\odot)(p-p^\odot)\big)^+,\, 1\Big\}, \qquad S(p^\odot,k^\odot) = -\,\frac{k^\odot c/(p^\odot)^2 + \pi_0'(p^\odot)/B}{1 - c/p^\odot},$$

when the retailer sets price $p$. The retailer then earns $\Phi(p) = k(p)B(1-c/p) + \pi_0(p)$.

In the general $n$-good model, prices $\mathbf p$ are vectors, $\mathbf Q(\mathbf p,k,\mathbf g)$ is the refugees' demand under cash fraction $k$ and in-kind bundle $\mathbf g$, and the PDCA policy of Proposition 4 is a clipped linear function of a weighted price index $\mathbf p^\top\mathbf v$.

Formalization targets

Goal: the target price is optimal under the symmetric PDCA scheme

Assume Assumption 2, $\pi_0$ concave on $(c,\infty)$, and a feasible target with $c < p^\odot \le p_0$ and $k^\odot \in [0,1]$. Then $k(p^\odot) = k^\odot$, and

$$\Phi(p) \le \Phi(p^\odot) \quad \text{for every } p > c,$$

with $p^\odot$ the unique maximizer when $\Pi(p^\odot,k^\odot) > \Pi_0$ (§6.3, p. 22).

Milestones

1. $c\,Q(p,k) = kBc/p$ and $\pi_r(p,k) = kB(1-c/p)$ (§5, p. 16).
2. The proof of Proposition 4 ($n$ goods, Online Appendix p. 5): the policy (22)–(24) pays $(k^\odot, \mathbf g^\odot)$ at $\mathbf p^\odot$, and the retailer's PDCA objective satisfies the first-order condition (A.13) there. This is the claim the proof verifies, not the global optimality (16) asserted by Proposition 4, which the paper obtains from (A.13) only under an unstated condition on the demand functions.
3. The symmetric scheme (27) pays $k^\odot$ at $p^\odot$, its slope equals $-(\partial\Pi/\partial p)/(\partial\tilde\pi_r/\partial k)$, and the first-order condition holds at $p^\odot$.
4. Where $k(p) \in (0,1)$, the refugee profit $k(p)B(1-c/p)$ is strictly concave in $p$.
5. Where $k(p) = 0$ the retailer earns $\pi_0(p) \le \Pi_0$; where $k(p) = 1$ it earns $B(1-c/p) + \pi_0(p)$.

Significance

The goal is the paper's positive design result. Without a policy, the retailer's best response to cash assistance is a price above $p_0$ (Proposition 1 of the paper). The PDCA scheme reverses this incentive with no price regulation: the government only monitors that announced prices are kept. Every feasible target, including the one that maximizes social welfare, can be implemented this way, and the retailer still earns at least $\Pi_0$. Proposition 4 gives the general $n$-good recipe: weight each price by the retailer's marginal profit, and let the cash fraction fall with the price index at the rate that offsets the marginal gain from raising prices.

The results are proved in the paper, which argues the symmetric case in two paragraphs. No machine-checked version exists. Formalizing them makes several conditions explicit that the text leaves implicit. The slope of the scheme must be non-positive, which needs $p^\odot \le p_0$. The clipped branches must be compared with the unclipped concave profit. The general proposition is established at the level of the first-order condition.

Difficulty

The obvious argument says that the PDCA profit has a critical point at $p^\odot$ by construction, so $p^\odot$ is optimal. This fails twice. First, the schedule is clipped to $[0,1]$, so the profit is only piecewise smooth and is not globally concave: on the branch $k(p) = 1$ the profit $B(1-c/p) + \pi_0(p)$ need not be dominated by a concave function through $p^\odot$ unless the comparison is made explicitly. Second, the middle branch is concave only if the schedule's intercept is non-negative, which depends on the sign of $\pi_0'(p^\odot)$ and hence on $p^\odot \le p_0$ and Assumption 2. The uniqueness clause needs strict versions of each comparison and fails without $\Pi(p^\odot,k^\odot) > \Pi_0$.

Formalization scope

All quantities are real. Prices range over $p > c$; the scheme, the profits and the slope are explicit defs transcribing (18) and (27), with $\pi_0'$ as Lean's deriv, used only at points where Assumption 2 makes $\pi_0$ differentiable. $\Pi_0$ is the value $\pi_0(p_0)$, not a supremum. Assumption 2 is read on $(c,\infty)$: $D$ continuously differentiable there, $D' \le 0$ on $(c,p_{\max})$, and $\pi_0$ nondecreasing on $(c,p_0]$, nonincreasing on $[p_0,\infty)$, with $p_0$ its unique maximizer. "$\pi_0$ concave" is read on $(c,\infty)$. Feasibility uses the retailer clause $\Pi(p^\odot,k^\odot) \ge \Pi_0$ and $p^\odot \le p_0$; the refugee-utility clause of (26) is dropped, which strengthens the goal. In the $n$-good model, $\mathbf Q$ and $\mathbf D$ are abstract functions, partial derivatives are Fréchet derivatives on unit vectors, and Proposition 4 assumes $0 < k^\odot < 1$, $\partial\tilde\pi_r/\partial k \ne 0$ and differentiability at the target, and concludes the first-order condition (A.13) of its proof; the mission does not state the $n$-good global optimality (16).

The goal must not be replaced by the first-order condition alone (milestone 3) or by an assumption that the PDCA profit is concave: it quantifies over every price $p > c$, with the clip of (27) in place.

The development needs only one-variable calculus and convexity from Mathlib. The hypotheses are satisfiable: for $D(p) = 10 - p$, $c = 2$, $B = 8$, $p_0 = 6$, $p^\odot = 5$, $k^\odot = 1/2$, the target profit $17.4$ exceeds $\Pi_0 = 16$. Proofs of any milestone, and statements of the paper's Propositions 1, 3 and 5 for the same model, are welcome.

Selected references

• T. O. Kotsi, O. Q. Wu, A. J. Pedraza-Martinez, Donations for Refugee Crises: In-kind Versus Cash Assistance, Manufacturing & Service Operations Management 24(6), 2022 (authors' manuscript of November 27, 2021). https://doi.org/10.1287/msom.2021.1073
• J. Jódar Vidal et al., The state of the world's cash 2020, The Cash Learning Partnership, 2020. https://perma.cc/8JL5-6LKJ

Motivation

Biopharmaceuticals such as vaccines and therapeutic proteins are produced by living cells grown in a bioreactor. In a batch fermentation the cells multiply until the medium is depleted and the culture enters a stationary phase, after which the batch is harvested. A bleed–feed operation removes part of the culture and replaces it with fresh medium, restarting exponential growth in the same bioreactor and saving the cost of cleaning, sterilising and setting up a new batch. Regulators cap the number of bleed–feeds per batch. The operational question is when to bleed–feed: too early forgoes biomass that would have grown, too late risks the culture entering the stationary phase first and the opportunity being lost.

Koca, Martagan, Adan, Maillart and van Ravenstein model this decision as a finite-horizon Markov decision process and show that, under conditions on the growth and risk profile, the optimal policy is described by three thresholds (SSRN 3659907; published in Manufacturing & Service Operations Management, doi:10.1287/msom.2022.1163). The paper reports an implementation at MSD (Merck), and threshold rules of this form are what can be written into production plans.

Setting

The state of a batch is $(i,\mu,n)$:

• the cultivation age $i\in\{0,1,\dots,I\}$, the number of periods of length $\tau>0$ since the current culture started, reset to $0$ by a bleed–feed;
• the cell growth rate $\mu\in\mathcal M=[\mu_\ell,\mu_u]$ with $0<\mu_\ell\le\mu_u$, known for the first culture and redrawn after every bleed–feed from a probability distribution $G$ carried by $\mathcal M$;
• the bleed–feed count $n\in\{0,1,\dots,N\}$, where $N$ is the regulatory limit.

Starting from biomass $m_0>0$, the biomass at age $i$ is $m_{i\mu}=m_0(1+\mu\tau)^i$, and continuing for one period earns the increment $r_{i\mu}=m_{i+1,\mu}-m_{i\mu}$. The culture stays in exponential growth with probability $p_{i\mu}=1-\nu(m_{i\mu})\tau$, where the rate $\nu$ is zero up to a critical biomass $\tilde m\ge0$ and strictly increasing beyond it; otherwise it enters the stationary phase and earns nothing more. The critical age $\tilde\imath_\mu$ is the least age at which $m_{i\mu}>\tilde m$.

The value function is defined by the optimality equations: $v(I,\mu,n)=0$ and, for $i<I$,

$$v(i,\mu,n)=\max\bigl\{C(i,\mu,n),\,B(n)\bigr\},\qquad C(i,\mu,n)=r_{i\mu}+p_{i\mu}\,v(i+1,\mu,n),\qquad B(n)=\mathbb E\bigl[C(0,M,n+1)\bigr],$$

with $M\sim G$ and $B(N)=0$. Bleed–feed is optimal in $(i,\mu,n)$ when $n<N$ and $C(i,\mu,n)\le B(n)$; continuing is optimal when $B(n)\le C(i,\mu,n)$.

Formalization targets

Goal: Corollary 1, a three-way control limit

Assume Condition (4), $\frac{r_{i\mu}-r_{i-1,\mu}}{r_{i\mu}}\le p_{i-1,\mu}-p_{i\mu}$ for $\tilde\imath_\mu\le i<I$; Condition (5), $\frac{r_{i-1,\mu^+}-r_{i-1,\mu}}{r_{i\mu^+}}\le p_{i-1,\mu}-p_{i-1,\mu^+}$ for $\tilde\imath_{\mu^+}<i<I$ and $\mu\le\mu^+$; and Assumption 1, that bleed–feed is optimal at age $I-1$ whenever $n<N$. Then there are thresholds $i^*(\mu,n)\in\mathbb Z$, $\mu^*(i,n)\in\mathbb R$ and $n^*(i,\mu)\in\mathbb Z$ with

$$\begin{aligned} i\le i^*(\mu,n)&\Rightarrow\text{continue},& i>i^*(\mu,n)&\Rightarrow\text{bleed–feed},\\ \mu<\mu^*(i,n)&\Rightarrow\text{continue},& \mu>\mu^*(i,n)&\Rightarrow\text{bleed–feed},\\ n\le n^*(i,\mu)&\Rightarrow\text{bleed–feed},& n>n^*(i,\mu)&\Rightarrow\text{continue}. \end{aligned}$$

Milestones

In the paper's order: the risk profile facts of §3 (p. 12); Remark 1 and Propositions 1–2, giving monotonicity in the age and Theorem 1; Propositions 3–4, giving monotonicity in the growth rate and Theorem 2; Propositions 5–6, giving monotonicity in the count and Theorem 3. Theorems 1, 2 and 3 are the three clauses of the goal, each under its own hypotheses (Theorem 3 needs none).

Significance

The result turns a dynamic program over a continuous state into three monotone rules, each with a direct operational reading: bleed–feed older cultures, faster-growing cultures, and cultures early in their bleed–feed budget. The thresholds are monotone in the remaining coordinates (Corollary 2 of the paper), which is what makes the policy tabulable for a production plan.

The paper proves the result on paper; nothing about this model is formalized. A complete development gives a machine-checked monotone-comparative-statics argument for a reset-type MDP with a continuum of states and an expectation over a general distribution, including the measure-theoretic content the paper leaves implicit: that $B(n)$ is an honest integral of a bounded measurable function. The formalization also repairs two printed points that matter for correctness (see Formalization scope).

Difficulty

Each monotonicity result is a backward induction a few lines long on paper, but the inductions interact. Monotonicity in $i$ holds trivially before the critical age and needs Condition (4) after it; the age threshold requires gluing the two regions, which the paper does not spell out. Monotonicity in $\mu$ compares two cultures whose critical ages differ, and its base case at age $I-1$ rests on Assumption 1. Monotonicity in $n$ requires $B(n+1)\le B(n)$, an inequality between integrals whose integrands are themselves defined by the recursion, so integrability and measurability in $\mu$ must be carried through the induction. A pointwise argument that ignores the integrals proves nothing about $B$.

Formalization scope

All declarations live in the namespace BleedFeed.ControlLimit. One definition file holds the parameters (Params), the standing assumptions (Standing), $m$, $r$, $p$, the critical age, the value recursion $v$, $C$, $B$, the predicates BleedOpt and ContOpt, Condition (4), Condition (5) and Assumption 1. Ages and counts are natural numbers; everything else is real. $G$ is a probability measure on $\mathbb R$ with $G(\mathcal M^c)=0$, and $B(n)$ is a Bochner integral against it.

Committed conventions, each disclosed in the statements:

• $\nu(\tilde m)=0$, $\nu$ strictly increasing on $[\tilde m,\infty)$, $\nu(m)\tau\le1$, and $\nu$ measurable;
• Condition (5) is stated on $\tilde\imath_{\mu^+}<i<I$. The printed range $\tilde\imath_{\mu^+}\le i<I$ fails for every $\mu<\mu^+$ when $\tilde\imath_{\mu^+}\ge1$, while the proof uses only the corrected range;
• Assumption 1, standing in §4.2, is a hypothesis of Propositions 3–4, Theorem 2 and the goal;
• the growth-rate threshold is strict on both sides, since with a continuum of rates and a jump in $\nu$ the non-strict form can fail at the threshold itself;
• Remark 1's "continue" clause carries $i+1<I$;
• index shifts $i-1$ use natural-number subtraction, which makes the $i=0$ clauses of Condition (4) and Proposition 2 trivial; the page leaves them undefined.

"Optimal" is always the comparison of $C(i,\mu,n)$ with $B(n)$ in the optimality equation, never a threshold policy assumed in advance, and $B(n)$ is the integral, not a free parameter: a formalization in which $B$ could vanish by non-integrability would make continuing always optimal and the thresholds trivial. The hypotheses of the goal are jointly satisfiable with $B(0)>0$ (checked on an explicit instance).

Contributions welcome: proofs of the milestones; general lemmas on measurability and integrability of finite-horizon value recursions over a real parameter; and a sharper, non-vacuous instance witnessing Condition (5).

Selected references

• Y. Koca, T. Martagan, I. Adan, L. Maillart, B. van Ravenstein, Increasing Biomanufacturing Yield with Bleed–Feed: Optimal Policies and Insights, Manufacturing & Service Operations Management, 2022; SSRN 3659907. https://ssrn.com/abstract=3659907, https://doi.org/10.1287/msom.2022.1163
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

Many service providers are paid under a contract that makes them responsible for a customer's costly failures over a fixed window: a hospital penalized for heart-failure readmissions within 30 days, or a maintenance contractor responsible for engine replacements. A preventative appointment lowers the chance of such a failure, and the sooner it takes place the fewer customers fail while waiting. Capacity for appointments is limited. A clinic plans a fixed number of base slots per period at no incremental cost, and can add a limited number of surge slots (overtime, external staff) at a cost per slot. The scheduler therefore trades the cost of surge capacity against the discounted cost of failures caused by delay.

B. Grant, I. Gurvich, R. K. Mutharasan and J. A. Van Mieghem (SSRN 3092667; Manufacturing & Service Operations Management, 2021, doi:10.1287/msom.2020.0932) model this trade-off as an infinite-horizon discounted dynamic program, motivated by follow-up appointments for heart-failure patients at Northwestern Memorial Hospital. Their first optimality result, Proposition 1, identifies when the simplest policy, booking every request in the earliest period with a free slot, is optimal.

Setting

Time is divided into periods. The appointment book at the start of a period is $\mathbf S = (S_0, \dots, S_D)$, where $S_d$ is the number of appointments already booked $d$ periods ahead and $D \ge 1$ is the booking horizon. Each period has $K = K_b + K_s$ slots: $K_b$ base slots and $K_s$ surge slots. A valid book has $S_d \le K$ for every $d$ and $S_D = 0$.

At the start of each period $a$ new requests arrive, i.i.d. across periods with law $\mathbb P(A = a)$ supported on $\{0, \dots, M\}$. The scheduler books them: an action $\mathbf u = (u_0, \dots, u_D)$ is admissible (1) if $u_0 = 0$ (no same-period booking), $u_d + S_d \le K$ for $1 \le d \le D$, and $\sum_{d=1}^D u_d = a$. If the requests do not fit, every free slot is filled and the $n_O$ remaining overflow requests are sent elsewhere at cost $c_F$ each.

Between periods each booked customer independently fails with probability $p_F$, at cost $c_F$, and leaves the book; the others move one period closer, so the next book is a product of binomial thinnings of $\tilde{\mathbf S} = \mathbf S + \mathbf u$ with survival probability $p_{\bar F} = 1 - p_F$ (4). A customer who reaches the appointment shows with probability $p_S$ and afterwards fails within the contract window with probability $p_{F|S}$; a no-show (probability $p_{\bar S} = 1 - p_S$) fails with probability $p_{F|\bar S} > p_{F|S}$. Serving $S_0$ appointments costs $h(S_0) = c_s \max\{S_0 - K_b, 0\}$ (5). The expected one-period cost (7) is

$$g = h(S_0) + \beta c_F\,\mathbb E[\text{failures before the next period}] + S_0\,c_F\,(p_S p_{F|S} + p_{\bar S}p_{F|\bar S}) + c_F\,n_O ,$$

and a policy $\pi$ is valued by its expected total discounted cost $V_\pi(\mathbf S^0) = \sum_{t \ge 0} \beta^t\,\mathbb E[g_t]$ (9), with discount factor $\beta \in (0, 1)$.

The First-Available (FA) policy books the requests into periods $1, 2, \dots, D$ in order, filling every free slot of a period (base, then surge) before using the next.

Formalization targets

Goal: Proposition 1 (p. 12)

If

$$\frac{c_s}{c_F} \le \min_{1 \le d < d' \le D} \big(p_{\bar F}^{d'-d}\beta^{d'-d} - 1\big)\big(p_S p_{F|S} + p_{\bar S} p_{F|\bar S}\big) + \frac{\sum_{i=d}^{d'-1}\beta^{i+1}p_F p_{\bar F}^{i}}{p_{\bar F}^{d}\beta^{d}}, \qquad (13)$$

then FA is optimal: $V_{\mathrm{FA}}(\mathbf S^0) \le V_\pi(\mathbf S^0)$ for every admissible policy $\pi$ and every valid book $\mathbf S^0$.

Milestones

1. (8): the expected one-period cost is bounded, $g \le \bar h + c_F(\beta D K + K + M)$.
2. Policy evaluation (§6.2): the value of a stationary admissible policy solves $V_\sigma(\mathbf S) = \sum_a \mathbb P(A = a)\big(g + \beta\sum_{\mathbf S'}\mathbb P(\mathbf S' \mid \mathbf S + \sigma(\mathbf S, a))V_\sigma(\mathbf S')\big)$.
3. (11): the optimal value $V^*$ solves the Bellman equation, and a stationary policy minimizing its right-hand side exists and is optimal.
4. (18) ⟺ (13): for each pair $d < d'$, the comparison (18) of the bounds (15) at $d$ and (16) at $d'$ is equivalent to the $(d, d')$ term of (13).
5. (18) ⟹ (17), (19), (20): the single inequality (18) implies the other three comparisons of the bounds.

Significance

Proposition 1 gives a closed-form, state-independent and arrival-independent sufficient condition under which the scheduler needs no optimization at all: book every request as early as possible, using surge capacity whenever base capacity is full. The paper's numerical study finds FA optimal in a large fraction of realistic scenarios, so the condition marks out a regime in which a hospital can use the simplest rule without loss. Together with Propositions 2 and 3 of the paper (base-first and base-first/last-surge policies) it maps out which simple policy to use as the surge cost varies.

The paper's argument for Proposition 1 compares the expected discounted cost of one customer booked at delay $d$ with surge against the same customer at delay $d' > d$ without surge, and concludes optimality from the comparison. That step is an incremental-cost heuristic: the passage from the four inequalities (17)–(20) to optimality of FA in the dynamic program is asserted in one sentence, not proved. Milestones 4 and 5 formalize the algebra the paper does carry out; the bridge from (17)–(20) to optimality of the policy is the open part of this mission. As far as is known, no machine-checked proof of this result or of any optimality result for appointment scheduling with surge capacity exists.

Difficulty

The obvious argument is the paper's: each request is cheaper earlier, so book it earlier. In the dynamic program the requests interact. A customer booked early occupies a slot that a later arrival could have used; failures free slots again; surge cost is charged on the realized number of customers present at the appointment, after failures; and overflow depends on how full the book was left by earlier decisions. A single-customer comparison does not account for any of these, and the per-customer cost of FA (12) need not even be monotone in the delay for every parameter choice. Any argument has to account for the whole state of the book, not one customer at a time.

Formalization scope

All objects live in the namespace SurgeAppt.FirstAvail. Costs and probabilities are real numbers and counts are natural numbers. A book is a function $\{0, \dots, D\} \to \mathbb N$, indexed as on the page; the transition reads $\tilde S_{d+1}$ into $S'_d$ and sets $S'_D = 0$. The cost (7) is computed with the surge cost (5) and the expected failure term written as a finite sum over next books. A policy is a sequence of decision rules $U^t(\mathbf S, a)$ (Markov deterministic, possibly non-stationary); it is admissible if each decision at a valid book with $a \le M$ satisfies (1), including the forced action when (1) is empty. The value (9) is the series $\sum_t \beta^t\,\mathbb E[g_t]$ over the law of the book at time $t$; it is never defined as a fixed point. Condition (13)'s minimum is read as "for every pair $1 \le d < d' \le D$", which is vacuous when $D = 1$.

Hypotheses added to the page and disclosed in every statement: $D \ge 1$, $c_s \ge 0$, $c_F > 0$, $0 < p_F < 1$, and $p_S, p_{F|S}, p_{F|\bar S} \in [0, 1]$; the page's $p_{F|S} < p_{F|\bar S}$, $\beta \in (0, 1)$ and $\mathbb P(A \le M) = 1$ with $M \ge 1$ are kept. History-dependent and randomized policies are not modelled; the paper's remark after (11) that a stationary optimal policy exists licenses comparing FA against Markov policies.

The goal is not trivialized: the competitors are every admissible Markov policy, not only first-available-like ones; the admissibility of FA is part of the conclusion, so a rule that skipped bookings could not qualify; and the value is a convergent series of bounded nonnegative costs, not a junk value.

A complete development needs: finite discounted MDP facts (milestones 2 and 3, reusable for any finite-state model with constrained actions), properties of the product-binomial kernel, and a comparison argument for the goal. Proofs of any milestone, alternative arguments for the goal, and counterexample searches that probe the boundary of (13) are welcome.

Selected references

• B. Grant, I. Gurvich, R. K. Mutharasan, J. A. Van Mieghem, Optimal dynamic appointment scheduling of base and surge capacity, SSRN 3092667, revised July 1, 2020. https://ssrn.com/abstract=3092667
• The same, Manufacturing & Service Operations Management, 2021. https://doi.org/10.1287/msom.2020.0932
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887
• A. F. Hernandez et al., Relationship between early physician follow-up and 30-day readmission among Medicare beneficiaries hospitalized for heart failure, JAMA 303(17), 2010. https://doi.org/10.1001/jama.2010.533

Why platforms worry about leakage

On-demand service platforms (home cleaning, tutoring, handyman and care services) match customers with independent providers and keep a commission on every transaction. Once a customer and a provider have met through the platform, both can save the commission by transacting directly the next time. This platform leakage (also called disintermediation) is a central operational concern for such platforms: it erodes revenue and can make the platform unviable. Platforms counter it with lower commissions, perks such as insurance and payment protection, and enforcement.

He, Savin, Goh and Teo (SSRN 3550646; published in Manufacturing & Service Operations Management, doi:10.1287/msom.2022.1179) build a queueing-game model of this trade-off. The platform sets the share of each fee it pays out, providers choose whether to work on the platform, off it, or not at all, and customers choose where to queue. The paper's main result for perfect information, Proposition 3, gives the exact range of the customers' counterparty risk (the extra cost of transacting off-platform) in which leakage occurs at the platform's optimum. This mission formalizes that result and the chain of results its proof rests on.

The model

There are two provider types $j\in\{h,l\}$, with $N^j\ge1$ providers of type $j$. Customers value type-$j$ service at $v^j>0$, every provider serves at rate $\mu>0$, and customers pay $c>0$ per unit of waiting time. With $c_s^2\ge0$ the squared coefficient of variation of service times, put $\phi=(1+c_s^2)/2$. Aggregate demand arrives at rate $\Lambda$ with $\Lambda>(N^h+N^l)\mu$ (supply-constrained service, (1)).

Customers. An on-platform queue of $C$ providers at fee $q$ with demand rate $\lambda$ has expected wait $W_p(C,\lambda)=\frac{\lambda}{C(\mu-\lambda)}\phi$; a single off-platform provider has $W_o(1,\lambda)=\frac{\lambda}{\mu-\lambda}\phi$. Off-platform customers bear an extra cost $R_o\ge0$. Customers join each queue until their net utility equals that of the outside option, which determines the equilibrium demand rates $\lambda^j_p(C,q)$ and $\lambda^j_o(q)$.

Providers. A provider of type $j$ has opportunity cost rate $K^j\ge0$, with $K^h\ge K^l$. Off the platform he sets a fee maximizing $q\lambda^j_o(q)$, earning utility $U^j_o$. On the platform, when $n$ type-$j$ providers share a symmetric fee $Q^j_p(n)$, each keeps the share $\omega^j\in[0,1]$ of the fee and earns $U^j_p(\omega^j,n)$. A provider participation equilibrium (Definition 1) is a pair $(N^j_p,N^j_o)$ of head counts on and off the platform from which no provider wants to switch among on-platform, off-platform and outside options. When several equilibria exist, providers settle on the one with the most providers on the platform.

Platform. Anticipating these responses, the platform chooses payout ratios $(\omega^h,\omega^l)\in[0,1]^2$ to maximize its profit rate

$$\Pi(\omega^h,\omega^l)=\sum_{j=h,l}N^j_p(\omega^j)\big((1-\omega^j)Q^j_p(N^j_p(\omega^j))-R_o\big)\lambda^j_p\big(N^j_p(\omega^j),Q^j_p(N^j_p(\omega^j))\big),$$

absorbing the counterparty risk $R_o$ on every on-platform transaction.

The paper's closed forms are $g_1(n,v)=\big(nv+c\phi-c\phi\sqrt{1+nv/(c\phi)}\big)/n$ and $g_2(n,v)=\frac{c\mu\phi}{n}\big(\sqrt{1+nv/(c\phi)}-1\big)^2$, and the non-platform opportunity cost is $\widehat K^j=\max\{K^j,g_2(1,v^j-R_o)\}$.

Formalization targets

Goal: Proposition 3

With

$$a^j=v^j+c\phi\left(1-\left(\Big(1-\sqrt{\tfrac{N^j-1}{N^j}}\Big)\sqrt{1+\tfrac{N^jv^j}{c\phi}}+\sqrt{\tfrac{N^j-1}{N^j}}\right)^2\right),\qquad b^j=v^j+c\phi\left(1-\Big(1+\sqrt{\tfrac{K^j}{c\phi\mu}}\Big)^2\right),$$

the platform's problem has an optimum, and at every optimal payout pair and in the selected participation equilibrium,

$$N^j_o>0\iff R_o\in(a^j,b^j)\qquad(R_o\notin\{a^j,b^j\}).$$

At the paper's own optimal payout ratio $\omega^{j*}$ the equivalence (25) holds whenever $R_o\ne b^j$.

Milestones

1. Lemma 1: the equilibrium demand rates are uniquely $\lambda^j_p(C,q)=\mu\frac{C(v^j-q)^+}{c\phi+C(v^j-q)^+}$ and $\lambda^j_o(q)=\mu\frac{(v^j-q-R_o)^+}{c\phi+(v^j-q-R_o)^+}$.
2. Lemma 2: optimal fees $Q^j_p(n)=g_1(n,v^j)$ and $Q^j_o=g_1(1,v^j-R_o)$, and utility rates $U^j_p(\omega,n)=\omega g_2(n,v^j)-K^j$ and $U^j_o=g_2(1,v^j-R_o)-K^j$.
3. Monotonicity of $g_2$ in $n$ (p. 16; proof of Proposition 1).
4. Proposition 1: equilibria have $N^j_p\in\{0,N^j\}$, with none joining iff $\omega^j<\widehat K^j/g_2(1,v^j)$ and all joining iff $\omega^j\ge\widehat K^j/g_2(N^j,v^j)$.
5. Proposition 2: the payout ratios $\omega^{j*}$ of (23) are optimal, with profit (24).
6. (A9)(i): $U^j_o>0\iff R_o<b^j$.
7. (A9)(ii): $(1-\omega)g_1(N^j,v^j)<R_o\iff R_o>a^j$ for $\omega=g_2(1,v^j-R_o)/g_2(N^j,v^j)$.

Significance

The result separates the two forces behind leakage. Below $a^j$, counterparty risk is cheap enough that the platform finds it profitable to pay providers enough to stay. Above $b^j$, off-platform service is so unattractive to customers that providers prefer their outside option. Leakage is confined to the interval between, so a platform can read off whether perks that lower $R_o$, or changes in pool size $N^j$, push a provider type into or out of the leakage regime. The interval shrinks as $N^j$ grows, which is the paper's case that larger provider pools protect platforms.

The result is proved in the paper, by hand. No machine-checked version exists. The mission produces a formal model of a queue-based Stackelberg platform game: customer queue-joining equilibria, symmetric fee equilibria among providers, participation equilibria with a selection rule, and an optimizing leader. This structure recurs throughout the platform-operations literature (Taylor 2018 and its successors) and is reusable for related models.

Difficulty

Each step is elementary in isolation; the work is in the chain. The platform's objective depends on $\omega$ through the selected participation equilibrium, which is discontinuous in $\omega$: it jumps from $0$ to $N^j$ providers at $\widehat K^j/g_2(N^j,v^j)$. Optimality must therefore be argued over a piecewise objective, not by first-order conditions. The natural first idea, evaluating everything at the closed-form $\omega^{j*}$, proves only the third clause of the goal. The goal also quantifies over every optimum, including ties at $R_o=a^j$, where the platform is indifferent between keeping and losing a type. The final equivalences then require nontrivial manipulation of nested radicals in (A9)(ii).

Formalization scope

Everything lives in the namespace PlatformLeakage.Perfect, in one definition file and eight theorem files. Parameters are a structure Params, with real values and natural-number head counts; the provider types are an inductive PType with constructors h, l. Every statement assumes Params.Std: $N^j\ge1$, $v^j>0$, $0\le K^l\le K^h$, $\mu,c>0$, $c_s^2\ge0$, $R_o\ge0$, and (1). Positive parts are max x 0, and square roots are Real.sqrt, with every radicand nonnegative under Std.

Committed conventions:

• The demand rates are the closed forms (16)–(17), and Lemma 1 states that they are the unique solutions of (5) with stability $\lambda<\mu$.
• Utilities are defined as suprema of revenue over fees $\ge0$, not by $g_2$, so Lemma 2 is not definitional.
• The on-platform fee is a revenue maximizer (Classical.epsilon).
• Definition 1 is per type and omits the printed clause $U^j_o<U^j_p(\omega,N^j_p-1)$, which contradicts Proposition 1 at the paper's own optimum.
• $\widehat K^j$ uses $g_2(1,(v^j-R_o)^+)$.
• The selected equilibrium maximizes the on-platform head count.
• Optimality means maximizing $\Pi$ over $[0,1]^2$.
• The goal excludes $R_o=b^j$ (where $U^j_o=0$ and Definition 1 sends providers off the platform) and, in its every-optimum clause, $R_o=a^j$.
• The value (24) is stated only when $\widehat K^j>0$.

A formalization that states the goal only at $\omega^{j*}$ of (23), or that defines utilities by $g_2$, would be trivial and is ruled out. Proofs of any milestone, and reusable lemmas on nested radicals or on piecewise-monotone optimization, are welcome.

Selected references

• E. J. He, S. Savin, J. Goh, C.-P. Teo, Off-Platform Threats in On-Demand Services, SSRN working paper 3550646, 2021. https://ssrn.com/abstract=3550646; published in Manufacturing & Service Operations Management, https://doi.org/10.1287/msom.2022.1179
• T. A. Taylor, On-Demand Service Platforms, Manufacturing & Service Operations Management 20(4), 2018. https://doi.org/10.1287/msom.2017.0678
• W. Whitt, Approximations for the GI/G/m Queue, Production and Operations Management 2(2), 1993. https://doi.org/10.1111/j.1937-5956.1993.tb00094.x
• R. Hassin, M. Haviv, To Queue or Not to Queue: Equilibrium Behavior in Queueing Systems, Kluwer, 2003. https://doi.org/10.1007/978-1-4615-0359-0

Motivation

Firms facing a new technology rarely decide in the dark: they run pilots, prototypes and market tests before committing. The management literature on disruptive technologies (Christensen, The Innovator's Dilemma, 1997) argues that incumbents fail because they evaluate new opportunities with tests tuned to their existing business, and that entrants succeed because they test differently. Gans's paper (NBER Working Paper 29091, published as Experimental Choice and Disruptive Technologies, Management Science 2023, doi:10.1287/mnsc.2022.4496) turns this into a decision-theoretic question: when a firm may choose which experiment to run, and experiments differ in how they trade false positives against false negatives, which one does it choose?

The first result of the paper, Proposition 1, is the building block for everything after it (incumbent versus entrant choices, competition, cooperation). It says that the optimal experiment is biased toward the firm's own predisposition, echoing the result of Che and Mierendorff (Optimal Dynamic Allocation of Attention, American Economic Review, 2019) that information seekers choose news sources that reflect their own bias.

Setting

A firm decides whether to exploit a new technology. The state of the world is $W$ (the technology works) or $N$ (it does not). Exploiting earns $v_W$ in state $W$ and $v_N$ in state $N$; not exploiting, the status quo, earns $v_S$. The payoffs satisfy $v_W>v_S>v_N$. The firm's prior probability of $W$ is $p$, with $0<p<1$.

Without information the firm exploits when $p\,v_W+(1-p)\,v_N\ge v_S$, that is, when $p\ge\hat p$, where the no-information threshold is

$$\hat p=\frac{v_S-v_N}{v_W-v_N}.$$

An experiment yields a signal $w$ or $n$, with $\Pr[w\mid W]=\lambda_w$ and $\Pr[n\mid N]=\lambda_n$ (Table 1 of the paper; $\lambda_w$ is the sensitivity and $\lambda_n$ the specificity). Experiments are costless; the firm runs exactly one, chosen from the experiment set

$$\mathbf E=\bigl\{(\lambda_w,\lambda_n)\in(0,1]^2:\ 1<\lambda_w+\lambda_n\le\Lambda\bigr\},\qquad 1<\Lambda<2 .$$

Put $\lambda=\Lambda-1\in(0,1)$. The w-biased experiment is $\sigma_w=(1,\lambda)$: a working technology always produces $w$, so the signal $n$ is conclusive bad news. The n-biased experiment is $\sigma_n=(\lambda,1)$: the signal $w$ is conclusive good news.

After observing the signal, the firm decides whether to exploit. A decision rule assigns an action to each signal; there are four. The value $\mathrm{value}(e)$ of an experiment $e$ is the expected payoff under the best of the four rules. An experiment is optimal if it lies in $\mathbf E$ and no experiment in $\mathbf E$ has a larger value.

Formalization targets

Goal: Proposition 1 over the whole experiment set

$$p>\hat p\ \Longrightarrow\ \bigl(e \text{ optimal in } \mathbf E\iff e=\sigma_w\bigr),\qquad p<\hat p\ \Longrightarrow\ \bigl(e \text{ optimal in } \mathbf E\iff e=\sigma_n\bigr).$$

The paper states Proposition 1 as "the firm optimally chooses the w-biased experiment" if $p>\hat p$ and the n-biased one if $p<\hat p$, and adds that, "for all but a degenerate case, these are the only two experiments that will be optimally chosen". The goal records both: the biased experiment is optimal over $\mathbf E$, and it is the unique optimum. The degenerate case $p=\hat p$ is excluded, as in the paper.

Milestones

1. The no-information threshold: $0<\hat p<1$ and exploiting without information is optimal iff $p\ge\hat p$ (§2, p. 11).
2. The posteriors of $\sigma_w$ and $\sigma_n$, including $\Pr[N\mid n,\sigma_w]=1$ and $\Pr[W\mid w,\sigma_n]=1$ (§2.1, p. 12; p. 31).
3. The optimal responses under $\sigma_w$: after $n$, keep the status quo; after $w$, exploit iff $p>t_w=\frac{(1-\lambda)(v_S-v_N)}{v_W-v_S+(1-\lambda)(v_S-v_N)}$, with $t_w<\hat p$ (proof of Proposition 1, p. 31).
4. The optimal responses under $\sigma_n$: after $w$, exploit; after $n$, exploit iff $p>t_n=\frac{v_S-v_N}{(1-\lambda)(v_W-v_S)+v_S-v_N}$, with $t_n>\hat p$ (p. 31).
5. Proposition 1 in pairwise form: $\mathrm{value}(\sigma_n)<\mathrm{value}(\sigma_w)$ if $p>\hat p$, and the reverse if $p<\hat p$.
6. The indifference-curve display $V=p\lambda_wv_W+(1-p)(1-\lambda_n)v_N+((1-p)\lambda_n+p(1-\lambda_w))v_S$ for the rule "exploit iff $w$", and its unique maximisers over $\mathbf E$ at the kinks $\sigma_w$ (point A of Figure 1) and $\sigma_n$ (point B) (§2.2, pp. 13–14).

Significance

The result. Proposition 1 says that a firm predisposed to exploit designs its test so that only a conclusive "no" can change its mind, and a firm predisposed not to exploit designs it so that only a conclusive "yes" can. The rest of the paper applies it with firm-specific payoffs: an incumbent, whose status quo is valuable, has a higher threshold than an entrant (Proposition 2), and this difference drives the paper's account of why incumbents and entrants experiment differently with disruptive technologies (Propositions 3–5). Without Proposition 1 none of these comparisons is defined.

Formalizing it. The result is proved in the paper (§7.1, p. 31), but the proof covers only the comparison between the two biased experiments; the claim that no other experiment is optimal is argued graphically from Figure 1, and the proof leaves the case $p<\hat p$ to "the same way". The mission produces a machine-checked proof of the full statement over $\mathbf E$, with uniqueness. To our knowledge no part of it has been formalized before.

Difficulty

The obvious argument compares $V$ along the frontier of $\mathbf E$ with the slope of the indifference curves. That argument fixes the decision rule "exploit iff $w$", while the firm's value is the best of four rules: for priors far above $\hat p$ the firm exploits after both signals of $\sigma_n$, and the comparison then changes form (the two cases of the proof on p. 31). A proof over $\mathbf E$ must handle the maximum of four piecewise-linear functions of $(\lambda_w,\lambda_n)$ and show that it is uniquely maximised at one vertex. The printed slope expression on p. 13 also has its axes interchanged relative to Figure 1, so it cannot be transcribed as it stands.

Formalization scope

All quantities are real numbers. States and signals are Bool; a decision rule is a function Bool → Bool; the value of an experiment is Finset.sup' of the expected payoff over the four rules, so the firm's post-signal choice is optimal by construction. Joint probabilities are prior times Table 1 entry; posteriors use real division and are stated only for signals of positive probability. Two hypotheses are added to the paper's and recorded in the definitions: $0<p<1$ (at $p\in\{0,1\}$ the biased experiments tie) and $\Lambda>1$ (otherwise $\mathbf E$ is empty and $\lambda\le0$). Optimality is maximisation over $\mathbf E$, and experiments are equal when both precisions are equal.

Defining the value as the payoff of the single rule "exploit iff $w$" (the display $V$) would trivialize the goal into milestone 6 and is ruled out: the value is always the best rule. Comparing only $\sigma_w$ and $\sigma_n$ is milestone 5, not the goal.

The development needs only finite sums and elementary real inequalities; no probability library is required. Contributions of proofs of any milestone, and of alternative proofs of the goal, are welcome.

Selected references

• J. S. Gans, A Synthetic Model of Disruption and Experimentation, NBER Working Paper 29091, July 2021. https://www.nber.org/papers/w29091
• J. S. Gans, Experimental Choice and Disruptive Technologies, Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4496
• Y.-K. Che and K. Mierendorff, Optimal Dynamic Allocation of Attention, American Economic Review, 2019. https://doi.org/10.1257/aer.20171000
• C. M. Christensen, The Innovator's Dilemma, Harvard Business School Press, 1997.