All missions

Motivation

Non-profit organizations such as food banks run on volunteer labour. Volunteers sign up for shifts, wait on a sign-up list, work, rest, and may or may not return; the organization can spend money on engagement activities (reminders, recognition events, recruitment drives) that raise the rate at which volunteers come back or arrive. Spending too little leaves shifts unstaffed; spending too much wastes a scarce budget. Ata, Tongarlak, Lee and Field (arXiv:2312.02920, Operations Research, 2024) model this as a multiclass queueing network, pass to a heavy-traffic limit, and obtain a one-dimensional drift-rate control problem: a reflected diffusion for the scaled workload whose drift is chosen, at a cost, from an interval of feasible drifts. The optimal policy they derive is a nested threshold policy: as the workload falls below successive thresholds $\tau_1>\tau_2>\dots>\tau_L$, one more engagement activity is switched on.

To compute that policy one needs the thresholds, and the paper obtains them from a closed-form description of the solution of the Bellman equation between consecutive thresholds. That closed form, Proposition 3 of the paper, is the goal of this mission. A companion mission formalizes Theorem 1, the existence of a solution of the same Bellman equation.

Setting

There are $L\ge1$ engagement activities. The data are a lowest drift $\theta_0<0$, drift increments $\eta_1,\dots,\eta_L>0$, per-unit-drift costs $0<c_1<c_2<\dots<c_L<p$, an idleness cost rate $p$, a mean-reversion rate $\kappa>0$ and a volatility $\sigma>0$. The breakpoints are

$$\theta_l=\theta_0+\sum_{i=1}^{l}\eta_i,\qquad l=0,\dots,L,$$

and the feasible drifts form the interval $A=[\theta_0,\theta_L]$. The engagement cost $c:A\to\mathbb R_+$ is the convex, increasing, piecewise linear function with $c(\theta_0)=0$ and slope $c_l$ on $(\theta_{l-1},\theta_l]$:

$$c(x)=\sum_{i=1}^{l-1}c_i\eta_i+c_l(x-\theta_{l-1}),\qquad \theta_{l-1}<x\le\theta_l .$$

Its convex conjugate is

$$\phi(y)=\sup_{x\in A}\{yx-c(x)\},\qquad y\in\mathbb R .$$

The Bellman equation of the drift-rate control problem asks for a constant $\beta>0$ and a continuously differentiable function $v$ on $[0,\infty)$ with

$$\beta=\tfrac12\sigma^2v'(x)+x\kappa\,\big(p-v(x)\big)-\phi\big(p-v(x)\big),\qquad x\ge0,$$

such that $v(0)=0$, $v$ is strictly increasing, and $v(x)\to p$ as $x\to\infty$. Here $\beta$ is the optimal long-run average cost and $v=g'$ is the derivative of the transformed relative value function $g$ of the paper's §4 (p. 20).

Put $\hat c_l=c_l$ for $l=1,\dots,L$ and $\hat c_{L+1}=p$. Since $v$ is strictly increasing from $0$ towards $p$, each level $p-\hat c_l\in(0,p)$ is attained exactly once; the thresholds are

$$\tau_l=v^{-1}(p-\hat c_l),\quad l=1,\dots,L,\qquad \tau_{L+1}=0,\qquad \tau_0=\infty .$$

With $\Phi$ the standard normal cumulative distribution function, the paper defines for $l=1,\dots,L+1$

$$u_l(x)=p-\hat c_l\exp\Big\{\tfrac{-2\theta_{l-1}(x-\tau_l)+\kappa(x^2-\tau_l^2)}{\sigma^2}\Big\}+\tfrac{2(\beta-c(\theta_{l-1}))\sqrt\pi}{\sigma\sqrt\kappa}\exp\Big\{\tfrac{(\kappa x-\theta_{l-1})^2}{\kappa\sigma^2}\Big\}\Big[\Phi\Big(\tfrac{\kappa x-\theta_{l-1}}{\sigma\sqrt{\kappa/2}}\Big)-\Phi\Big(\tfrac{\kappa\tau_l-\theta_{l-1}}{\sigma\sqrt{\kappa/2}}\Big)\Big].$$

Formalization targets

Goal: Proposition 3 (p. 25)

For every solution $(\beta,v)$ of the Bellman equation and every $l=1,\dots,L+1$,

$$v(x)=u_l(x)\qquad\text{for all }x\in[\tau_l,\tau_{l-1}).$$

The statement fixes nothing beyond the model: it holds for any solution, with the thresholds defined from that solution.

Milestones

1. (E9), Online Supplement p. 13: the conjugate is piecewise linear,

$$\phi(y)=\theta_0y\ (y\le c_1),\qquad \phi(y)=\theta_{m-1}y-c(\theta_{m-1})\ (c_{m-1}<y\le c_m),\qquad \phi(y)=\theta_Ly-c(\theta_L)\ (y>c_L).$$

2. Lemma 2(i), (D1), Online Supplement p. 9: for $\kappa,\sigma>0$,

$$\int_\tau^x e^{(2\theta z-\kappa z^2)/\sigma^2}\,dz=\frac{\sigma\sqrt\pi}{\sqrt\kappa}e^{\theta^2/(\kappa\sigma^2)}\Big[\Phi\Big(\tfrac{x-\theta/\kappa}{\sigma/\sqrt{2\kappa}}\Big)-\Phi\Big(\tfrac{\tau-\theta/\kappa}{\sigma/\sqrt{2\kappa}}\Big)\Big].$$

3. Lemma 2(ii), (D2), Online Supplement p. 9: the companion formula for $\int_\tau^x z\,e^{(2\theta z-\kappa z^2)/\sigma^2}dz$.

Significance

The result. Proposition 3 turns the nested threshold policy into something computable. Evaluating $u_l$ at the right end of its interval and inverting gives $\tau_{l-1}$ from $\tau_l$, so the thresholds $\tau_L,\tau_{L-1},\dots,\tau_1$ follow by a one-dimensional recursion once $\beta$ is known. The paper's simulation study of a food bank (§5) uses these thresholds to set engagement policy. The result also shows that the value-function derivative, although defined through a nonlinear equation involving a supremum, is an explicit combination of Gaussian-type functions on each threshold interval.

Formalizing it. The result is proved in the paper (Online Supplement §D); no machine-checked version of it, of the conjugate formula (E9), or of the truncated Gaussian integrals (D1)–(D2) is known to exist. A formal proof checks the transcription of a long explicit formula with many constants, which is exactly where printed closed forms tend to go wrong, and produces reusable pieces: the conjugate of a convex piecewise linear function and two interval-integral identities for the normal cdf.

Difficulty

The Bellman equation is nonlinear in $v$ through $\phi(p-v)$. The obvious approach, solving it directly, fails because $\phi$ has no single formula. What makes it tractable is that on $[\tau_l,\tau_{l-1})$ the argument $p-v(x)$ stays in one linearity interval of $\phi$; this is a property of the solution, derived from its monotonicity and the definition of the thresholds, not a hypothesis. A complete proof must therefore combine the piecewise description of a supremum, a uniqueness argument for a linear first-order equation on a half-open interval (with the one-sided derivative at the left end and, for $l=1$, an unbounded interval), and the evaluation of Gaussian integrals over finite intervals in terms of the normal cdf, matching every constant of the printed formula. The two expressions for the $\Phi$ arguments, $(\kappa x-\theta)/(\sigma\sqrt{\kappa/2})$ in $u_l$ and $(x-\theta/\kappa)/(\sigma/\sqrt{2\kappa})$ in (D1)–(D2), are equal, but the identification must be made.

Formalization scope

All objects live in the namespace VolunteerEngage.Thresholds, Lean 4 with Mathlib.

• The parameters form a structure Model; $\eta$ and $c$ are $\mathbb N$-indexed sequences of which the indices $1,\dots,L$ are used. The standing assumptions ($L\ge1$, $\theta_0<0$, $\eta_l>0$, $0<c_1<\dots<c_L<p$, $p>0$, $\kappa>0$, $\sigma>0$) form the predicate Standing, a hypothesis of every model-level theorem. The paper states them in the model's derivation ((15), (24), (42), (43), (50), p. 18) rather than for the abstract control problem.
• The cost (52) is written as one sum, equal to (52) on $A$; values off $A$ are never used. $\phi$ is the supremum (66) over $A$, never its closed form, so (E9) is a genuine statement.
• A solution of the Bellman equation includes $\beta>0$ and a pair $(v,v')$ with $v'$ continuous on $[0,\infty)$ and the one-sided derivative of $v$ within $[0,\infty)$ at every point. "Increasing" is strict.
• The thresholds enter the goal as a sequence $\tau$ with $\tau_{L+1}=0$ and, for $l\le L$, $\tau_l\ge0$ and $v(\tau_l)=p-\hat c_l$; strict monotonicity makes this the definition $\tau_l=v^{-1}(p-\hat c_l)$, so the proposition's clause "$\tau_l=v^{-1}(p-\hat c_l)$", which restates that definition, is not posed separately. $\tau_0=\infty$ is encoded by dropping the upper bound for $l=1$.
• The goal is stated for every solution $(\beta,v)$; $\beta>0$ is part of the solution predicate, as on p. 21. It is not vacuous: the companion mission's goal (Theorem 1) asserts that a solution exists. A formalization that assumed the closed form of $\phi$, that $p-v$ stays in one linearity interval, or that took $u_l$ as the definition of $v$ would make the goal trivial and is ruled out.
• $\Phi$ is the published definition Cohen2019.Robust.Phi, which is Mathlib's cdf (gaussianReal 0 1). Integrals in (D1)–(D2) are oriented interval integrals of continuous functions.

The source is the arXiv preprint v2 including its Online Supplement. The queueing network (§2) and the Brownian control problem (§3) motivate the Bellman equation but are not part of any formal statement; the optimality of the threshold policy (Theorem 2) is not formalized here. Proofs of any milestone, of the goal, and general lemmas on conjugates of piecewise linear functions or on Gaussian integrals over intervals are welcome.

Selected references

• B. Ata, M. H. Tongarlak, D. Lee, J. Field, A Dynamic Model for Managing Volunteer Engagement, arXiv:2312.02920v2, 2023; Operations Research, 2024. https://arxiv.org/abs/2312.02920

Why inspection timing matters

Banks and other financial firms lose money through operational errors: mistyped trades, missed reconciliations, compliance lapses. Regulators require the firm to hold capital against these losses, and internal audit teams spend most of their effort deciding when to inspect. Two inspection schedules are common in practice: a periodic schedule (inspect every month) and a random schedule (surprise audits). A periodic schedule leaves no error undetected for long, but an employee who knows the date can relax right after an inspection and work hard only before the next one. A random schedule removes that back-loading, but leaves some errors undetected for long stretches.

Y. Kim and Y. Xu, Operational Risk Management: Optimal Inspection Policy (SSRN 3491006; published in Management Science, DOI 10.1287/mnsc.2021.00322), model this trade-off as a principal–agent problem with moral hazard. They show that neither pure schedule dominates the other (their Proposition 4, the subject of mission I of this series), and then propose a hybrid schedule that combines them. This mission formalizes their Proposition 5: the best hybrid schedule beats the best random schedule strictly and the best periodic schedule weakly.

The source used throughout is the authors' SSRN preprint, version of July 2023. All labels (Proposition 5, Lemma 5, (EC.55), …) and page numbers are those of that version, not of the published article.

The model

A firm (the principal) employs an agent whose errors arrive as a Poisson process with rate $\lambda e^{-a_t}$. Here $a_t\ge0$ is the agent's effort at time $t$ since the last inspection, at unit cost $c$. Each undetected error costs the principal $L$ per unit of time until an inspection finds it. At each inspection the agent pays a penalty $P$ per error found. The principal pays a wage $w$ per unit of time and an inspection cost $K$ per inspection, earns base profit $\mu$, and both parties discount at rate $r$. The agent accepts the job only if his payoff is at least his reservation payoff $\bar\pi$. Write $\bar\mu=\mu-r\bar\pi$.

The time $\tau$ between two inspections is drawn independently in every cycle from a law chosen by the principal, with mean $1/v$ (the frequency $v$):

• random policy $R$: $\tau\sim\mathrm{Exp}(v)$;
• periodic policy $D$: $\tau=1/v$;
• hybrid policy $H(q)$, $q\in[0,1]$: inspect at time $q/v$ with probability $q$; otherwise wait a further $\mathrm{Exp}(v)$ time. Its distribution function is (21):

$$F_\tau(t)=\begin{cases}1-(1-q)e^{-v(t-q/v)}, & t>q/v,\\ q, & t=q/v,\\ 0, & t<q/v.\end{cases}$$

$H(1)$ is the periodic policy and $H(0)$ the random one.

Given a policy and a strategy $(v,P,w)$, the agent chooses an effort path that maximizes his discounted payoff (1). The principal's discounted payoff is (3):

$$\Pi(v,P,w)=\frac{\mu-w}{r}-L\,\frac{\mathbb E[\int_0^\tau N^{a^*}_t e^{-rt}dt]}{1-\mathbb E[e^{-r\tau}]}+P\,\frac{\mathbb E[N^{a^*}_\tau e^{-r\tau}]}{1-\mathbb E[e^{-r\tau}]}-\frac{K}{e^{r/v}-1},$$

where $a^*$ is the agent's optimal effort and $N^{a}_t$ is the number of errors made by time $t$ in a cycle. The principal maximizes $\Pi$ over $v,P,w\ge0$ subject to participation (4)–(5). Throughout, Assumption 1 holds: $c<L\lambda/r<\bar\mu$. The optimal payoff under policy $I$ is written $\Pi_I(S^*_I)$.

Formalization targets

Goal: Proposition 5 (p. 20)

For every inspection cost $K>0$ there is a payoff $x_H$ achievable by some hybrid policy such that

$$x_R<x_H\ \text{ for all achievable random payoffs } x_R,\qquad x_D\le x_H\ \text{ for all achievable periodic payoffs } x_D .$$

In the paper's notation, $\Pi_{H(q^*)}(S^*_{H(q^*)})>\Pi_R(S^*_R)$ and $\Pi_{H(q^*)}(S^*_{H(q^*)})\ge\Pi_D(S^*_D)$.

Milestones

1. (6), p. 10. At an optimal strategy the participation constraint binds, and $\Pi_I=V_I(v,P)$, the reduced payoff (6).
2. Lemma 3, p. 13. Under $R$ the optimal effort is constant, with $e^{-a^*}=\min\{\frac{c}{P\lambda}\frac{r+v}{v},1\}$, and it is zero when $P\le c/\lambda$.
3. Lemma 5(a), pp. 19–20. Under $H(q)$ the optimal effort is given by (22): dynamic before $q/v$, constant after it.
4. Lemma EC.3, p. ec8. The optimal random strategy is $S^1_R$ (effort inducement) or $S^0_R$ (error correction).
5. Proposition 1, p. 14. $S^1_R$ is optimal above a threshold $K_R$ and $S^0_R$ below it, in closed form with an implicitly defined $\alpha$ and $v^0_R$.
6. (EC.55), pp. ec34–ec35. With zero effort, $V^0_{H(q)}(v)>V^0_R(v)$ if and only if $v>v^q$, where $e^{qr/v^q}=1+qr/v^q+(qr/v^q)^2$, and $v^q<qr$.

Significance

Proposition 5 says that reducing the randomness of a surprise-audit schedule, in the hybrid way, strictly improves the principal's optimal payoff whatever the inspection cost. Combined with Proposition 4 it yields the paper's Corollary 1: when inspections are expensive, the optimal mix lies strictly between the two pure policies. The comparison is between optima: each policy is evaluated at its own best frequency, penalty and wage, with the agent best-responding.

The result is proved in the paper (pp. ec34–ec35); to our knowledge it has no machine-checked proof. Formalizing it requires a measure-theoretic treatment of renewal-type payoffs against three inspection laws, the agent's optimal control problem under each law, and the closed-form solution of the random policy (Proposition 1). The model layer (laws, payoffs, best response, achievable payoffs) is shared with mission I of this series.

Where the difficulty lies

The weak part is immediate, because the periodic policy is the hybrid policy with $q=1$. The strict part is not a comparison of two closed forms: the hybrid optimum has no closed form, and the optimal mix $q^*$ is not computed. The random optimum itself is one of two strategies of different nature (Lemma EC.3), effort-inducing or error-correcting, and the agent's response under $H(q)$ has a different shape from his response under $R$ (Lemma 5), so the regime boundaries of the two policies do not coincide. The naive claim that $H(q)$ beats $R$ at every strategy is false: with zero effort, $V^0_{H(q)}(v)<V^0_R(v)$ whenever $v<v^q$ (EC.55), so whether mixing helps depends on the frequency.

Formalization scope

• Model layer. The $\mathcal M$ error classes enter only through $\lambda=\sum_m\lambda_m$ and $L=\sum_m(\lambda_m/\lambda)L_m$, as in the paper from p. 10 on. The model starts at the reformulated payoffs (1) and (3): the cycle decomposition of EC.4.1 is not formalized, and expected counts are $\mathbb E[N^a_t]=\lambda\int_0^te^{-a_s}ds$, independent of $\tau$.
• Standing assumptions. $r,c,\lambda,L,\mu,\bar\pi,K>0$ and Assumption 1 ($c<L\lambda/r<\bar\mu$).
• Effort paths are functions of the time since the last inspection, the same in every cycle. They are measurable, nonnegative and bounded; boundedness keeps every integral finite and loses no optimal effort of Lemmas 3–5.
• Frequencies are $v>0$, because (6) contains $e^{r/v}$.
• Laws. $\mathrm{Exp}(v)$ is Mathlib's ProbabilityTheory.expMeasure v; the periodic law is a Dirac mass at $1/v$; the hybrid law is $q\,\delta_{q/v}$ plus $(1-q)$ times the shifted exponential law.
• Optima. "Policy $A$'s optimum beats policy $B$'s" is stated as: some achievable $A$-payoff is larger than every achievable $B$-payoff. No supremum is used, so no junk value of an empty or unbounded set can make a statement true. The argmax $q^*$ of (25) is not formalized, because the paper does not prove that it exists; one dominating hybrid payoff is exactly what the comparison with $\Pi_{H(q^*)}$ asserts.
• Agent optimality is tested at wage $0$; the wage enters (1) only as $w/r$.
• Divisions. The effort formulas (11) and (22) divide by $P$; they are stated under $P>c/\lambda$, with the zero-effort case stated separately.
• Implicit numbers. $\alpha$, $v^0_R$ and $v^q$ are variables carrying their defining equations and positivity.

The goal cannot be satisfied vacuously: it asserts the existence of an achievable hybrid payoff, so an empty achievable set does not make it true.

Contributions are welcome at every level: the integral identities for the three laws (Fubini for $\mathbb E[\int_0^\tau\cdot]$), the pointwise solution of the agent's problem, the two-variable optimization behind Proposition 1, and the final perturbation argument. The law lemmas and the agent's problem are reusable for any renewal-type inspection model.

Selected references

• Y. Kim and Y. Xu, Operational Risk Management: Optimal Inspection Policy, SSRN 3491006, version of July 2023. https://ssrn.com/abstract=3491006
• Y. Kim and Y. Xu, Operational Risk Management: Optimal Inspection Policy, Management Science (published version; not the numbering used here). https://doi.org/10.1287/mnsc.2021.00322

Motivation

Online marketplaces such as Airbnb, Amazon, eBay, Preply or Upwork earn most of their revenue from transaction fees: a seller who sells through the marketplace pays a fee on every sale. Many of these sellers also run their own sales channel, and a buyer who discovers a seller on the marketplace can often complete the purchase directly with that seller, avoiding the fee. This is marketplace leakage (also called disintermediation or showrooming of the platform). Marketplaces respond with measures the paper lists on its first pages: bundling transaction-related services, restricting buyer–seller communication before a transaction, and penalizing sellers caught taking clients off the platform.

Hagiu and Wright (Marketplace Leakage, Management Science, 2023) build a minimal model of this tension. Their baseline analysis answers the first question any of the later strategies depends on: if the marketplace can only choose its fee, what fee does it set, how much leakage remains in equilibrium, and how do these respond when buying directly becomes more costly for buyers? This mission formalizes that baseline result, Proposition 1 of the paper, for uniformly distributed switching costs.

Setting

There is one marketplace $M$, one seller $S$ and a unit mass of buyers, each wanting one unit of $S$'s product. Every buyer values the product at $v$; $S$'s marginal cost is $c$, with $c<v$; the outside option is worth $0$.

$S$ can sell through $M$, paying $M$ a fee $f$ per transaction, or through its direct channel, which carries no fee. It sets a price $p_m$ on $M$ and a direct price $p_d$. A buyer who buys directly bears a switching cost $s$; in this mission $s$ is uniformly distributed on $[0,\mu]$ with $\mu>0$, so its CDF is

$$G(s)=\min\Bigl\{\max\Bigl\{\frac s\mu,0\Bigr\},1\Bigr\}.$$

The timing is: $M$ sets $f$; observing $f$, $S$ sets its prices; buyers then choose. The paper's Lemma 1 lets one fix $p_m=v$, so $S$ only chooses $p_d\le v$. A buyer buys directly iff $s\le v-p_d$, so a share $G(v-p_d)$ of buyers — the leakage — buys directly. $S$'s profit at fee $f$ is

$$\pi_f(p_d)=(p_d-c)\,G(v-p_d)+(v-c-f)\,\bigl(1-G(v-p_d)\bigr),$$

and $M$ earns $\Pi=f\,(1-G(v-p_d))$. A direct price is seller-optimal at $f$ if it maximizes $\pi_f$ over $p_d\le v$. An equilibrium outcome is a pair $(f,p_d)$ with $f\le v-c$, $p_d$ seller-optimal at $f$, such that no other fee $f'\le v-c$, followed by a seller-optimal response, gives $M$ more.

Formalization targets

Goal: Proposition 1

For every $\mu>0$ an equilibrium outcome exists, and every equilibrium outcome $(f^*,p_d^*)$ satisfies

$$f^*(\mu)=\min\{\mu,v-c\},\qquad p_d^*(\mu)=v-\min\Bigl\{\frac\mu2,\frac{v-c}2\Bigr\},\qquad \Pi^*(\mu)=\begin{cases}\mu/2 & \mu\le v-c,\\ (v-c)\bigl(1-\frac{v-c}{2\mu}\bigr) & \mu\ge v-c,\end{cases}$$

with leakage $G(v-p_d^*)=\frac1\mu(v-p_d^*)\in(0,1)$. As $\mu$ increases, the fee weakly increases, the direct price and the leakage weakly decrease, and the marketplace's profit strictly increases.

Milestones

1. (4): for every fee $f\ge0$ the seller's optimal direct price is unique and equals $v-f/2$ if $f\le2\mu$ and $v-\mu$ if $f\ge2\mu$.
2. (5): at such a response the marketplace earns $f(1-f/(2\mu))$ if $f\le 2\mu$ and $0$ if $f\ge2\mu$.
3. The optimal fee (proof of Proposition 1): $(f,p_d)$ is an equilibrium outcome iff $f=\min\{\mu,v-c\}$ and $p_d$ is seller-optimal at $f$.
4. Equilibrium leakage (proof of Proposition 1): $G(v-p_d^*)=f^*/(2\mu)=\min\{1/2,(v-c)/(2\mu)\}$.

Significance

Proposition 1 is the baseline against which the paper measures every anti-leakage strategy: investment in transaction benefits, communication bans, referral fees and price-parity clauses are each compared with the fee-only outcome $\Pi^*(\mu)$, and Proposition 3 of the paper uses the closed form (6) directly. The result also has a substantive message: a fee-setting marketplace never eliminates leakage, but never lets it become total, and it gains from higher switching costs even though its own fee response offsets part of their effect on leakage.

The proposition is proved in the paper by elementary calculus. To our knowledge it has no machine-checked proof. Formalizing it produces a checked version of the baseline game, a verified statement of the seller's best response and the marketplace's value as functions of the fee, and a template that the companion missions on this paper reuse.

Difficulty

The seller's problem is not a smooth concave program: the clamped distribution $G$ creates a kink at $v-p_d=\mu$, below which every buyer switches and the profit is linear in $p_d$. The first-order condition $p_d=v-f/2$ is the optimum only while $f\le2\mu$; above that the optimum sits at the kink. The marketplace's objective inherits a kink at $f=2\mu$, and its feasible set $f\le v-c$ adds a corner that binds exactly when $\mu>v-c$. Negative fees are feasible and must be ruled out. The comparative statics compare equilibrium objects across two parameter values that may lie in different regimes, so the statement cannot be read off one formula.

Formalization scope

All parameters are real numbers, with the standing assumptions $c<v$ and $\mu>0$ as explicit hypotheses. $G$ is the clamped uniform CDF above. The statements use the reduced seller problem (1) with $p_m=v$, as the paper does after Lemma 1; Lemma 1 itself, which concerns the full game in which $S$ also chooses $p_m$, is not posed. Seller-optimality is an optimality predicate over $p_d\le v$, and the equilibrium is an optimality predicate over feasible fees $f\le v-c$ (negative fees included); "max" is attained, not a supremum. The displays (4) and (5) are stated for $f\ge0$, which is what they require; the paper's preface "Assuming $f\le v-c$" is not needed and does not exclude $f<0$.

Trivializing formalizations are ruled out: the seller's response and the marketplace's profit are not defined by the closed forms (4)–(5), the marketplace's value is not an unattained sSup, the equilibrium fee is not selected by Classical.choose, and the comparative statics are stated about equilibrium outcomes at two values of $\mu$, not about the formulas alone.

The development needs only Mathlib's real arithmetic, min/max and order lemmas. A proof of the seller's best response for a clamped uniform distribution is reusable in the companion missions on transaction benefits, communication bans and price parity, which restate the same model. Proofs of any milestone are welcome independently.

Selected references

• A. Hagiu and J. Wright, Marketplace Leakage, Management Science, 2023. https://doi.org/10.1287/mnsc.2023.4757 (formalized from the authors' manuscript dated March 2023; Proposition 1 on pp. 9–10, proof in §8.2, p. 34).

Motivation

Digital businesses (search engines, social networks, marketplaces) record what their users do and decide how well to protect what they record. Both choices affect users: stored data can improve the service, and it can also be accessed by adversaries such as hackers, fraudsters or data brokers, whose activity harms users. Regulation of data collection and data protection (the GDPR, the CCPA, liability rules for breaches) presupposes an answer to a basic question: in which direction does a profit-maximizing business's data strategy deviate from the one a benevolent planner would choose?

I. P. Fainmesser, A. Galeotti and R. Momot, Digital Privacy (Management Science 69(6), 2023; author manuscript SSRN 3459274), answer it in a model where users, adversaries and the business all respond to each other. Their Theorem 2 shows that the deviation is not arbitrary: one combination of errors never occurs, and the sign of the error is pinned down completely for a business whose revenue depends only on usage. This mission formalizes those two claims.

Setting

A data strategy is a pair $(\xi, C)$: the share $\xi \in [0,1]$ of each user's activity that the business stores, and a protection level $C \ge 0$, which costs $\psi C$. The parameters are real numbers: a network effect $\beta \in [0,1)$, the users' marginal benefit from stored data $\rho \in [0,1)$, the cost $\psi$, the revenue model $P \in [0,1]$, and the planner's weight $\alpha \in [0,1]$.

Given $(\xi, C)$, a unit mass of identical users choose activity levels and a large population of adversaries decide whether to access the stored data. The resulting equilibrium (Proposition 1 of the paper, display (3)) has average user activity

$$\bar a^*(\xi, C) = \frac{C(1+\rho\xi)}{C(1-\beta)+\xi^2}, \qquad \bar a^*(0, C) = \frac{1}{1-\beta}.$$

The value at $\xi = 0$ is the activity when nothing is stored, the value the paper uses where (3) reads $0/0$. From $\bar a^*$ one builds the consumer surplus (4), the business's profit (2) and the planner's objective (7):

$$\mathrm{CS}(\xi,C) = \tfrac12 \bar a^*(\xi,C)^2, \qquad \Pi(\xi,C) = (1-P)\,\bar a^*(\xi,C) + P\,\xi\,\bar a^*(\xi,C) - \psi C, \qquad W(\xi,C) = \alpha\,\mathrm{CS}(\xi,C) + (1-\alpha)\,\Pi(\xi,C).$$

The revenue model $P$ interpolates between a purely usage-driven business ($P = 0$, revenue proportional to activity) and a purely data-driven one ($P = 1$, revenue proportional to stored data $\xi \bar a^*$). A business optimum $(\xi^*, C^*)$ maximizes $\Pi$ over the feasible set $[0,1] \times [0,\infty)$; a social optimum $(\xi^W, C^W)$ maximizes $W$ over the same set. The business under-collects if $\xi^* \le \xi^W$ and over-protects if $C^* \ge C^W$, and so on.

Formalization targets

Goal: Theorem 2, first two sentences

The paper's Theorem 2 (p. 13) reads:

Relative to the socially optimal strategy, the equilibrium data strategy of a purely usage-driven business (P = 0) prescribes under-collection and under-protection of users' data, i.e., ξ* ≤ ξ^W and C* ≤ C^W. The equilibrium data strategy of a business with any data-driven component in its revenue model (P > 0) never prescribes under-collection and over-protection of users' data i.e., it is never the case that ξ* ≤ ξ^W and C* ≥ C^W with at least one of the inequalities being strict. Any other direction in which the optimal business's data strategy deviates from the socially optimal strategy is the outcome for some specification of the business's revenue model and values of other model parameters.

The goal is its first two sentences, for every business optimum and every social optimum:

$$P = 0 \;\Longrightarrow\; \xi^* \le \xi^W \text{ and } C^* \le C^W,$$ $$P > 0 \;\Longrightarrow\; \neg\bigl(\xi^* \le \xi^W,\ C^* \ge C^W,\ \text{at least one strict}\bigr).$$

The third sentence is established numerically in the paper (Figure 3) and is not a target.

Milestones

1. Display (11), p. 34: under $\xi^* \le \xi^W$ and $C^* \ge C^W$, the social optimum has weakly higher activity, $\bar a^*(\xi^W, C^W) \ge \bar a^*(\xi^*, C^*)$.
2. Display (12), p. 34: under the same assumptions, $\bar a^*(\xi^W,C^W)\,\xi^W \ge \bar a^*(\xi^*,C^*)\,\xi^*$.
3. Proposition 5(i), first claim (Online App. p. 8): for fixed $C$ and $P = 0$, a collection level maximizes $\Pi(\cdot, C)$ on $[0,1]$ if and only if it maximizes $W(\cdot, C)$.
4. The $P = 0$ step of the proof (App. A.4, p. 34): if $P = 0$ and $\xi^* > \xi^W$, then $C^* > C^W$.

Significance

The result. Theorem 2 identifies the one inefficiency that no revenue model produces: a business never stores too little data while protecting it too much. All other combinations occur for some parameters, so a regulator cannot infer the direction of a business's error without knowing its revenue model; but for a purely usage-driven business the direction is known, and it is too little protection. This underlies the paper's discussion of policy in §6, where the instruments considered (liability for data breaches, taxes on data) are compared by how they move $(\xi^*, C^*)$ towards $(\xi^W, C^W)$.

The formalization. The result is proved in the paper (App. A.4, with Proposition 5 in Online App. C.5); it has not been machine-checked. The paper's argument for the purely usage-driven case refers to first-order conditions and does not treat the boundary strategies ($\xi = 0$, $C = 0$) or parameter corners ($\rho = 0$) separately; a formal proof has to handle them. A complete development also yields reusable facts about the equilibrium activity $\bar a^*$: its sign, its behaviour in $\xi$ for fixed $C$, and the monotonicity in $C$ of the activity-maximizing collection level.

Difficulty

Both optima are defined only implicitly, as maximizers over a non-compact feasible set of a non-concave objective, and neither has a closed form that this mission may use. The comparison must therefore work from the optimality inequalities alone. The tempting approach, comparing first-order conditions, does not give a global statement: $\Pi$ and $W$ may have several local maxima, the maximizers need not be unique (both optima are $(0,0)$ in a whole region of parameters), and the constraint $\xi \le 1$ binds for large protection. In the purely usage-driven case the profit and welfare share their maximizers in $\xi$ for each fixed $C$, but turning that into a comparison of $C^*$ with $C^W$ requires control of how the maximizing $\xi$ moves with $C$, including at $C = 0$.

Formalization scope

All objects are real-valued functions of explicit real parameters $\beta, \rho, \psi, P, \alpha$ and of the strategy $(\xi, C)$, in the namespace DigitalPrivacy.Welfare, which imports $\bar a^*$, CS, the feasible set and the business optimum from the shared module DigitalPrivacy.Strategy.Setting. The equilibrium activity takes the value $1/(1-\beta)$ at $\xi = 0$ for every $C$, as in the paper; Lean's default $0/0 = 0$ is not used. Optima are predicates (IsBusinessOpt, IsSocialOpt): a feasible point at which the objective is at least its value at every feasible point. Theorem 2 quantifies over every pair of optima and asserts neither existence nor uniqueness. The P > 0 clause keeps the "at least one strict" condition; without it the clause is false, because both optima coincide at $(0,0)$ in part of the parameter space.

The standing assumptions are the paper's ranges $0 \le \beta < 1$, $0 \le \rho < 1$, $0 \le P \le 1$, $\alpha \le 1$, with two disclosed strengthenings: $\psi > 0$ (with $\psi = 0$, $\rho = 0$, $P = 0$, every $(0, C)$ is both a business and a social optimum and the $P = 0$ sentence fails) and $\alpha > 0$ (with $\alpha = 0$ the planner's problem is the business's, and step (11) does not hold). Proposition 5(i) is stated with the printed ranges, $\alpha = 0$ included. No other hypothesis is added, so the hypotheses on the optima cannot be made vacuous by the encoding; a sanity check exhibits parameters at which $(0,0)$ is both a business and a social optimum.

A complete development needs elementary real analysis of the rational function $\bar a^*$ on $[0,1] \times [0,\infty)$ and nothing beyond Mathlib. Proofs of the milestones, of lemmas about $\bar a^*$, and alternative arguments for the goal are all welcome. The paper's proofs are in App. A.4 (pp. 33–35) and Online App. C.5 (Online pp. 8–9).

Selected references

• I. P. Fainmesser, A. Galeotti, R. Momot, Digital Privacy, Management Science 69(6):3157–3173, 2023. https://doi.org/10.1287/mnsc.2022.4513. Author manuscript, This Draft: April 2022, https://ssrn.com/abstract=3459274 (the version cited for all page and display numbers).

Motivation

Two classical online selection problems sit at opposite ends of an information spectrum. In the secretary problem items arrive in uniformly random order, only their relative ranks are observed, and the best possible probability of stopping on the best item tends to $1/e$. In the i.i.d. prophet inequality the values are independent draws from a known distribution, and the best guarantee against the expected maximum is the constant $\approx 0.745$ of Hill and Kertz (1982), shown tight by Correa, Foncea, Hoeksma, Oosterwijk and Vredeveld (2017).

Correa, Cristi, Epstein and Soto (arXiv:2011.06516) interpolate between the two with the $p$-sample-driven optimal stopping problem. Each of $N$ items is sampled independently with probability $p$; the decision maker observes the relative rankings of the sampled items, then faces the remaining items online, observing relative rankings, and makes irrevocable stop/continue decisions. Stopping on the item of overall rank $i$ earns a reward $Y_i$, with $Y_1\ge Y_2\ge\cdots$. At $p=0$ and $Y=(1,0,0,\dots)$ this is the secretary problem; for adversarial $Y$ the optimal guarantee tends to $0.745$ as $p\to1$, the i.i.d. prophet constant.

For known $Y$, the paper writes a linear program over the stopping probabilities of rank-based algorithms (after Buchbinder, Jain and Singh, 2014) and takes its limit as $N\to\infty$. The analysis rests on one structural result, Theorem 2: this limiting program can be restricted, without loss, to solutions of an explicit threshold form, so that the optimal algorithm stops on an item of current rank $i$ after a time $t_i$. This mission is that theorem.

Setting

Fix $p\in[0,1)$. Time runs over $[p,1]$ (time $t$ is the fraction of the $N$ items seen so far; the sample accounts for the first fraction $p$ in the limit), and ranks $\ell=1,2,\dots$ refer to the relative rank of the current item among all items seen so far. A candidate solution is a function $q(t,\ell)$, the density of stopping at time $t$ on an item of relative rank $\ell$.

The cumulative mass of $q$ is $M_q(t)=\int_p^t\sum_{s\ge1}q(\tau,s)\,d\tau$. A solution is feasible for the continuous linear program CLP$_p$ when $q(t,\ell)\ge0$, each $q(\cdot,\ell)$ is integrable on $[p,1]$, and

$$t\,q(t,\ell)+M_q(t)\le1\qquad\forall t\in[p,1],\ \forall\ell\ge1 .$$

For $k\ge1$ the negative-binomial term is $\mathrm{nb}_{k,\ell}(t)=\sum_{j=\ell}^{k}\binom{j-1}{\ell-1}(1-t)^{j-\ell}t^{\ell}$, the probability that a NegativeBinomial$(\ell,t)$ variable is at most $k$, and

$$F_k(q)=\sum_{\ell=1}^{k}\int_p^1 q(t,\ell)\,\mathrm{nb}_{k,\ell}(t)\,dt .$$

$F_k(q)$ is the limit of the probability that the algorithm stops on an item of overall rank at most $k$. The objective of CLP$_p$ is $Y_1-\sum_{k\ge1}(Y_k-Y_{k+1})(1-F_k(q))$ for a non-increasing sequence $Y$, so any solution that increases every $F_k$ is at least as good.

A threshold sequence is a non-decreasing $(t_i)_{i\ge0}\subseteq[p,1]$ with $t_0=p$; put $T_i=\prod_{j=1}^{i}t_j$.

Formalization targets

Goal: Theorem 2 (p. 8)

For every feasible $q$ there are a feasible $q^*$ and a threshold sequence $(t_i)$ with $F_k(q^*)\ge F_k(q)$ for all $k\ge1$, such that for every $\ell\ge1$ and $t\in[p,1)$

$$t\,q^*(t,\ell)+\int_p^t\sum_{s\ge1}q^*(\tau,s)\,d\tau=1\ \ (t\ge t_\ell),\qquad q^*(t,\ell)=0\ \ (t<t_\ell),\tag{5–6}$$ $$q^*(t,\ell)=\begin{cases}T_i/t^{i+1}&t\in[t_i,t_{i+1}),\ \ell\le i,\\0&\text{else.}\end{cases}\tag{7}$$

Milestones

1. Lemma 17 (p. 28): $\mathrm{nb}_{k,\ell}$ is non-decreasing on $[0,1]$ for $1\le\ell\le k$.
2. Lemma 18 (p. 29): $\mathrm{nb}_{k,\ell}(t)$ is non-increasing in $\ell\ge1$ for $t\in[0,1]$.
3. (8) (p. 9): one mass-moving step $q_{n-1}\mapsto q_n$, which pushes each component to the right up to the envelope $\frac1t(1-M_{q_{n-1}}(t))$, keeps each component's mass, satisfies $M_{q_n}\le M_{q_{n-1}}$ in the form (8), and preserves feasibility.
4. $F_k(q_{n-1})\le F_k(q_n)$ (p. 9) for the same step.
5. Uniqueness (p. 10): for fixed thresholds, (5)–(6) have at most one feasible solution on $[p,1)$.
6. Existence (p. 10): the function (7) satisfies (5)–(6).

Significance

Theorem 2 turns an infinite-dimensional linear program over functions of two variables into the reduced problem RP$_p$, an optimization over a single non-decreasing sequence of thresholds. Every quantitative result of the paper is read off RP$_p$: the optimal ratio for each $p$, its limit as $p\to1$ (Theorem 8, mission II of this series) and the explicit lower bound $\alpha^*p$ (Theorem 9, mission III). It also identifies the optimal rank-based algorithms as threshold rules: accept the current item if it is among the $i$ best seen so far, where $i$ grows at the times $t_i$.

The result is proved in the paper. It has not been formalized, and neither has any part of the continuous-LP approach to secretary and prophet problems. The formal development produces a reusable layer: continuous stopping LPs with extended-real cumulative constraints, monotonicity of negative-binomial distribution functions in both parameters, and a rearrangement argument for integrals against monotone weights.

Difficulty

The obvious argument is to improve $q$ greedily: push each component's mass as far right as the constraint allows. One step is easy, but the step changes the constraint itself, since the envelope $\frac1t(1-M_q(t))$ depends on all components. The proof iterates, needs the thresholds $t_\ell(n)$ to be monotone in $n$, and must pass to a limit $q_\infty$ in $L^1$ with a dominating function that exists only because the smallest threshold is bounded away from $0$. The limit thresholds need not be monotone in $\ell$, and the components must then be reordered using Lemma 18. Finally, (5)–(6) are an integral equation in which each component depends on the sum of all others; identifying their unique solution with (7) needs both a uniqueness argument for a linear ODE and a telescoping computation.

Formalization scope

• A solution is a function q : ℝ → ℕ → ℝ, a representative of an element of $L^1([p,1]\times\mathbb N)$. Ranks, $k$, $i$, $j$ are 1-based; $q(\cdot,0)$ is never used. Constraints are imposed pointwise for all $t$, as printed.
• The cumulative mass $M_q(t)$ is the lower Lebesgue integral of $\sum_{s\ge1}q(\tau,s)$ in $[0,\infty]$, never a Bochner integral of a real series, which Lean would set to $0$ on divergent data.
• Integrability of each $q(\cdot,\ell)$ is part of feasibility, so $F_k$ is never a junk value.
• Equations (5)–(7) are imposed on $[p,1)$, not on $[p,1]$. At the single point $t=1$ the printed (5) and (7) contradict each other whenever finitely many thresholds are below $1$ (already for $q=0$). Feasibility of $q^*$ is required on all of $[p,1]$.
• The threshold intervals $[t_i,t_{i+1})$ are half-open, as in (7); they are pairwise disjoint because $(t_i)$ is non-decreasing.
• "Increasing" in Lemma 17 and "decreasing" in Lemma 18 are read as non-decreasing and non-increasing.
• The mass-moving step (milestones 3–4) takes the thresholds $t_\ell(n)$ as hypotheses satisfying their defining equation, and requires them to be positive (this only matters at $p=0$, where the paper's equation already forces it).
• Milestone 6 assumes $t_1>0$, and claims (5) at $t$ when $t<t_i$ for some $i$ or when $T_m/t_m^m\to0$; on the page these conditions are implicit, and without them the claim fails.
• A statement of Theorem 2 that keeps only "there is a feasible $q^*$ with $F_k(q^*)\ge F_k(q)$" is trivial ($q^*=q$); equations (5)–(7) are part of the goal and must not be dropped.
• Mathlib supplies interval and lower Lebesgue integrals, series in $[0,\infty]$ and binomial coefficients. Contributions welcome: the negative-binomial lemmas, the rearrangement inequality for monotone weights, and a Grönwall-type uniqueness argument for the integral equation.

Selected references

• J. Correa, A. Cristi, B. Epstein, J. A. Soto, Sample-Driven Optimal Stopping: From the Secretary Problem to the i.i.d. Prophet Inequality, arXiv:2011.06516v2, 2021. https://arxiv.org/abs/2011.06516
• T. P. Hill, R. P. Kertz, Comparisons of stop rule and supremum expectations of i.i.d. random variables, Annals of Probability 10(2), 1982. https://doi.org/10.1214/aop/1176993861
• J. Correa, P. Foncea, R. Hoeksma, T. Oosterwijk, T. Vredeveld, Posted price mechanisms for a random stream of customers, ACM EC 2017. https://doi.org/10.1145/3033274.3085137
• N. Buchbinder, K. Jain, M. Singh, Secretary problems via linear programming, Mathematics of Operations Research 39(1), 2014. https://doi.org/10.1287/moor.2013.0604

Motivation

Many service relationships pay an agent per unit of output whose arrival is random: a salesperson closing deals, a call-centre worker resolving tickets, a contractor delivering jobs. When effort is unobservable, the classical tool for keeping an agent motivated is the threat of termination after poor performance. In practice firms often use a milder punishment, suspension: the agent is sent home for a while and later called back. Restarting work is not free, and each restart costs the firm a fixed switching cost.

P. Cao, P. Sun and F. Tian, Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost (Management Science, 2024), characterise the optimal dynamic contract in this setting. The optimal contract depends on the size of the switching cost: when it is large the firm should not hire, when it is moderate the firm should keep the agent working forever, and when it is small the firm uses a control-band contract with suspension episodes. Their proof is "guess and verify": a stochastic verification theorem (their Theorem 1) turns any pair of functions satisfying a system of quasi-variational inequalities into an upper bound on the principal's value, and Propositions 2–7 exhibit such pairs in each parameter region.

This mission formalizes the certificate for the medium-switching-cost region under Condition 2 (Area II of the paper's Figure 2), where the agent is never suspended.

Setting

The principal faces a Poisson stream of arrivals, each worth revenue $R$. Without effort the arrival rate is $\underline\mu\ge0$; an agent who exerts effort, at cost $b>0$ per unit time, raises it to $\mu>\underline\mu$. Write $\Delta\mu=\mu-\underline\mu$. The principal's total cost rate while the agent works is $c\ge b$, every start of work costs a switching cost $K>0$, and the principal and agent discount at rates $0<r\le\rho$. Assumption 1 is $R\Delta\mu>c$.

The paper's derived constants are

$$\beta=\frac{b}{\Delta\mu},\quad \bar w=\frac{\beta\mu}{\rho},\quad \underline v=\frac{\underline\mu R}{r},\quad \bar V=\frac{R\mu-c-(\rho-r)\bar w}{r},\quad \bar K_2=\bar V-\underline v-\bar w,$$

together with the revenue thresholds $\hat R$ (28) and $\bar R$ (34) and the switching-cost threshold $\underline K$ (33). Condition 2 is $\mu<\rho-r$ and $R\ge\hat R$: the agent is much more impatient than the principal and revenue is high.

The state variable is the agent's promised utility $w\ge0$. Two operators act on functions $f$ of $w$, where $f'$ is the left derivative:

$$(\mathcal A_I f)(w)=(\mu+r)f(w)-\mu f(w+\beta)+\rho(\bar w-w)f'(w)-(\mu R-c)+(\rho-r)w,$$ $$(\mathcal A_\emptyset f)(w)=rf(w)-\rho wf'(w)+(\rho-r)w-R\underline\mu.$$

The first is a delay-differential operator for the working state, the second a first-order operator for the suspended state. A pair $(V_I,V_\emptyset)$ satisfies the optimality condition (20)–(22) when $\mathcal A_IV_I\ge0$, $\mathcal A_\emptyset V_\emptyset\ge0$, $0\le V_I-V_\emptyset\le K$ and $V_I(0),V_\emptyset(0)\ge\underline v$.

The suspended-state equation $\mathcal A_\emptyset V=0$ with $V(0)=\underline v$ is solved by $V_c(w)=\underline v+w+c\,w^{r/\rho}$ (24). In the region of this mission the paper builds

$$V_\emptyset(w)=\begin{cases}V_{c_K}(w),&w\le\bar w,\\ \bar V-K,&w>\bar w,\end{cases}\qquad V_I(w)=\begin{cases}V_{c_K}(w),&w\le\underline\theta_K,\\ \bar V+m_K(w-\bar w),&\underline\theta_K<w\le\bar w,\\ \bar V,&w>\bar w,\end{cases}$$

from parameters $(c_K,m_K,\underline\theta_K)$ chosen so that $V_{c_K}$ pastes smoothly onto the line at $\underline\theta_K$ and ends at $\bar V-K$ at $\bar w$.

Formalization targets

Goal: Proposition 5 (first claim)

Under Condition 2 and $K\in[\underline K,\bar K_2)$, for every triple $(c_K,m_K,\underline\theta_K)$ with $\underline\theta_K\in(0,\bar w)$, $c_K>0$, $m_K\in[\frac{\rho-r}{\rho-r-\mu},\frac{\bar V-\underline v}{\bar w})$ and

$$V_{c_K}(\underline\theta_K)=\bar V+m_K(\underline\theta_K-\bar w),\qquad V'_{c_K}(\underline\theta_K)=m_K,\qquad V_{c_K}(\bar w)=\bar V-K,$$

the functions $V_I,V_\emptyset$ above satisfy (20)–(22).

Milestones

1. (EC.67): explicit $C^1(\underline\theta)$ and $m(\underline\theta)$ solve the value-matching and smooth-pasting equations at any $\underline\theta\in(0,\bar w]$.
2. Lemma EC.3: $\psi_1(\underline\theta)=\bar V-\underline v-\bar w-C^1(\underline\theta)\bar w^{r/\rho}$ is continuous and strictly decreasing on $[0,\bar w]$, so $\psi_1=K$ has a unique root $\underline\theta_K\in(0,\bar w)$ for $K\in(0,\bar K_2)$; the root decreases in $K$ and tends to $\bar w$ as $K\downarrow0$.
3. Lemma 5: for every $K\in[\underline K,\bar K_2)$ the triple exists, and $c_K$, $m_K$, $\underline\theta_K$ are monotone in $K$.

Lemma 5 guarantees that the goal is not vacuous.

Significance

Proposition 5 is the analytic half of the paper's Theorem 4: combined with the verification theorem, it shows that in Area II the principal's optimal value is attained by a contract that pays the agent $\beta$ per arrival and never suspends. The threshold $\underline K$ separates this region from the control-band region of Proposition 7, so the explicit formula for $\underline K$ is the boundary of the phase diagram.

The result is proved in the paper. No machine-checked version exists. A formal proof checks a delicate sign argument near $w=0$, where $V_{c_K}$ has infinite slope, and it checks the threshold $\underline K$, whose printed formula contains an error (see Formalization scope). The paper's companion identity (41), $U(\bar\Gamma)=\bar V-\bar w-K=V_\emptyset(\bar w)-\bar w$, is about the utility of a contract and is not part of this mission; its deterministic half is immediate from (39).

Difficulty

The cases $w\in[\underline\theta_K,\bar w]$ and $w>\bar w$ are algebraic. The difficulty is $w\in(0,\underline\theta_K)$: there $V_I$ is the curve $V_{c_K}$, and $w+\beta$ lands beyond $\bar w$ (Condition 2 gives $\beta>\bar w$), so $\mathcal A_IV_I$ couples the curve with the constant $\bar V$. Positivity there needs more than the sign of the smooth-pasting slope: it uses the lower bound on $m_K$ in (35), which is exactly where the threshold $\underline K$ enters. A direct sign check at $\underline\theta_K$ alone does not cover the interval. The existence lemma requires monotonicity of $\psi_1$, whose expression mixes powers $\underline\theta^{r/\rho-1}$ with a linear factor.

Formalization scope

All functions are ℝ → ℝ and every quantifier ranges over $w\ge0$; powers are Real.rpow. The standing assumptions $0\le\underline\mu<\mu$, $0<b\le c$, $K>0$, $0<r\le\rho$, $R\Delta\mu>c$ are one hypothesis Standing; $\underline\mu\ge0$ and $b>0$ are read off the model and stated explicitly. The left derivative is derivWithin f (Set.Iic w) w, following the paper's convention on p. 15. Condition (20) is posed for $w>0$ only: at $w=0$ the right derivative of $V_{c_K}$ is $+\infty$, so the paper's (20) there is an extended-real statement and Lean's junk derivative would make it false. (21) and (22) are posed as printed.

The threshold $\underline K$ of (33) is corrected: the printed bracket contains $\frac r\rho\beta$, but the paper's own proof identifies $\underline K$ with $\check K_2$ of (EC.69), which gives $\frac{\rho-\mu}{\rho}\beta$. With the printed term Lemma 5 fails (for $r=0.2,\rho=1.2,b=c=1,R=5,\mu=0.9,\underline\mu=0.1$, the printed value is $-0.069$, the corrected one $7.2533$). Equation (36) is printed with a free $w$ that should read $\underline\theta_K$. The range $\underline\theta_K\in(0,\bar w)$, given by the proof, is stated.

The goal quantifies over all triples satisfying Lemma 5's conclusions; such a triple is unique, so this is the paper's claim, and Lemma 5 rules out a vacuous goal. Dropping the bound $K$ in (21), the condition (22), or the lower bound on $m_K$ would trivialize or change the statement.

The development needs the derivative of $w\mapsto w^{r/\rho}$, sign analysis of explicit real functions, and the intermediate value theorem. The Setting file is shared with the other missions of this series and will be consolidated. Proofs of the milestones in any order are welcome; (EC.67) is a self-contained calculus exercise.

Selected references

• P. Cao, P. Sun, F. Tian, Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost, Management Science, 2024. https://doi.org/10.1287/mnsc.2023.4845 (cited from the authors' manuscript and e-companion: §4.2 pp. 24–26, EC.3.7–EC.3.8 pp. ec32–ec34).
• Y. Sannikov, A Continuous-Time Version of the Principal-Agent Problem, Review of Economic Studies 75(3), 2008. https://doi.org/10.1111/j.1467-937X.2008.00486.x
• B. Biais, T. Mariotti, J.-C. Rochet, S. Villeneuve, Large Risks, Limited Liability, and Dynamic Moral Hazard, Econometrica 78(1), 2010. https://doi.org/10.3982/ECTA7261