Operations Research

Motivation

In atomic dynamic routing, indivisible agents (vehicles, packets, travellers) enter a network over time and travel along fixed routes. Each road admits a limited number of agents per unit of time, so agents queue at its entrance. A basic question for traffic models, packet-switching networks and dynamic routing games is how long an agent can stay in the network, its residence time. Upper bounds on residence times are what make it possible to bound queue lengths and the price of anarchy in dynamic routing games.

Greedy packet scheduling, where an edge never idles while packets wait for it, was studied by Cidon, Kutten, Mansour and Peleg (SIAM J. Comput. 1995), who showed that cycles can make delays large, and by Mansour and Patt-Shamir (J. Algorithms 1993), who bounded delivery times when every route is a shortest path. Cao, Chen, Chen and Wang (MOR 2022) prove a bound for arbitrary routes on acyclic networks. It holds under any rule that decides which waiting agent may leave next, and agents may keep entering forever. Their Theorem 1 is the goal of this mission. The paper then uses it to show that equilibria of three dynamic routing games on series-parallel networks have bounded queues (§6).

Setting

A network $G=(V,E)$ is a finite directed multigraph (parallel edges allowed) that is acyclic. Every edge has unit length and unit capacity. A path is a sequence of edges, each starting where the previous one ends. $L_{vw}$ is the number of edges of a longest $v$-$w$ path.

Time is discrete, $0,1,2,\dots$. Agents form a set $\Delta$, possibly infinite. At each time finitely many agents enter. Agent $i$ enters at time $r_i$ at his origin $o_i$ and follows a fixed route, a nonempty $o_i$-$d_i$ path. The tail of each edge holds a buffer. Two rules govern the dynamics:

• (A1) an agent reaching a vertex that is not his destination enters the buffer of his next edge at once;
• (A2) at every integer time, whenever a buffer is nonempty, exactly one agent leaves it and reaches the head of the edge one time unit later; the others wait.

No rule says which agent leaves. Every choice consistent with (A2) is an admissible run. An agent exits $G$ on reaching his destination. His residence time is his exit time minus his entry time (Definition 1).

Fix a focal agent $\zeta$ with entry time $r$. $G_\zeta$ is the subnetwork formed by all $o_\zeta$-$d_\zeta$ paths. For an integer time $r_0$:

• $A_{\zeta,p}$ is the set of agents who enter after time $r$ and use an edge of $G_\zeta$;
• $B_{\zeta,p}(r_0)$ is the set of agents $i\neq\zeta$ who entered by time $r$, are still inside $G$ at time $r_0$, and use an edge of $G_\zeta$.

An agent exits $G_\zeta$ when he reaches the head of the last edge of his route lying in $G_\zeta$.

Formalization targets

Goal: Theorem 1 (p. 7)

For every admissible run and every integer $r_0\ge r$: if no agent of $A_{\zeta,p}$ exits $G_\zeta$ before $\zeta$ exits $G$, then

$$t_\zeta\ \le\ r_0+L_{o_\zeta d_\zeta}+\bigl|B_{\zeta,p}(r_0)\bigr|,$$

where $t_\zeta$ is the exit time of $\zeta$.

Milestones (§3.2, p. 9)

When $\zeta$ is still inside $G$ at $r_0$, the proof follows tokens: imaginary markers that $\zeta$ produces from time $r_0$ on, and that travel with the agents leaving buffers ((s1), (s2), p. 8). The milestones are the paper's statements about them, with $L=L_{o_\zeta d_\zeta}$:

1. (p1) each agent holds at most one token, and a buffer never contains more tokens than agents;
2. (p2) the agent leaving $\zeta$'s buffer always holds exactly one token;
3. (p3) after $r_0$, $\zeta$ produces a new token only while he waits;
4. Claim 1 the induction step of Lemma 1 at the vertices where token $k$ departs right after a smaller token;
5. Lemma 1 token $k$ departs every vertex $v$ of its trail inside $G_\zeta$ by time $r_0+(L-L_{vd_\zeta}+k-1)$;
6. token exit token $k$ exits $G_\zeta$ by time $r_0+(L+k-1)$.

Significance

The result. The bound does not depend on the rule that selects the leaving agent, so it covers every queueing discipline at once: FIFO, global agent priorities, and the edge-priority rules of earlier dynamic routing games. With $r_0=r$ and no later entrants on $G_\zeta$, it gives Corollary 1: the residence time of $\zeta$ is at most $L_{o_\zeta d_\zeta}+|B_{\zeta,p}(r)|$. Example 1 (p. 8) shows that the bound can be attained. The freedom in $r_0$ is what §6 uses to show that queue lengths stay bounded at equilibria of dynamic routing games on series-parallel networks.

Formalizing it. The theorem is proved on paper. No machine-checked version is known to exist, and the platform has no rule-free model of atomic dynamic routing. The mission adds that model: a run is a set of leave times constrained by (A1)–(A2), not a fixed simulation. It also adds the multi-token process and the paper's chain of statements leading to Theorem 1.

Difficulty

The obvious argument is wrong. One might reason that $\zeta$ travels at most $L_{o_\zeta d_\zeta}$ edges and each earlier agent delays him at most once, giving the bound at once. The paper notes (p. 7) that this intuition fails even with two agents: a single agent can delay $\zeta$ more than $|\Delta|$ times, because delays propagate through other buffers. Bounding the total therefore means tracking chains of delays across the network rather than charging each delay to one agent.

Formally, the hard parts are:

• the run is only constrained, not determined;
• the token process is defined by recursion over time, using the unique leaver of each buffer;
• (p1)–(p3) are invariants proved by induction on time;
• Lemma 1 combines induction on the token index with longest-path inequalities in an acyclic graph.

Formalization scope

• Model. Network V E (tail and head maps) with finite V, E and a hypothesis Acyclic: no nonempty closed walk. Paths are edge lists. longest v w is the supremum of path lengths in $\mathbb N$; it is a maximum wherever it is used.

• Runs. RunData holds entry times, routes, origins and destinations, and leave times leave i j in $\mathbb N\cup\{\infty\}$ for the $j$-th edge of $i$'s route, numbered from $0$. IsADR states that:

  • routes are nonempty origin–destination paths;
  • finitely many agents enter per time;
  • nobody leaves a buffer before entering it;
  • (A2) holds, as unique existence of the leaver of each nonempty buffer at each time.

  Agents form an arbitrary type and may be infinitely many. An agent may never be served (leave time $\infty$), as in the paper, so the theorem also asserts that $\zeta$ exits.

• Derived objects. Exit times, $G_\zeta$, $A_{\zeta,p}$, $B_{\zeta,p}(r_0)$ and the exit time from $G_\zeta$ are definitions computed from the run, never free parameters. $|B_{\zeta,p}(r_0)|$ is Set.ncard of a set that is finite under IsADR.

• Tokens. The token milestones assume that $\zeta$ is inside $G$ at $r_0$, as §3.1 requires when starting the construction. Tokens are indexed from $1$. A new token gets index one plus the number produced so far. Bounds with subtraction are written additively over $\mathbb N$, e.g. $s+L_{vd_\zeta}+1\le r_0+L+k$, which is the same inequality over the integers.

• Ruled out. None of these is used, since each proves a different statement: a fixed tie-breaking rule (FIFO or priorities), exit times as free parameters, finitely many agents, or dropping acyclicity, which Remark 2 shows is necessary.

Contributions welcome: proofs of the token invariants, of Lemma 1, and of the goal. The network and run definitions can be reused for the paper's other results (Theorem 2 on uniform capacities, the routing games of §5–6).

Selected references

• Z. Cao, B. Chen, X. Chen, C. Wang, Bounding residence times for atomic dynamic routings, Mathematics of Operations Research, 2022 (accepted manuscript: WRAP 160244). https://doi.org/10.1287/moor.2021.1242 , https://wrap.warwick.ac.uk/160244
• Y. Mansour, B. Patt-Shamir, Greedy packet scheduling on shortest paths, Journal of Algorithms 14(3):449–465, 1993.
• I. Cidon, S. Kutten, Y. Mansour, D. Peleg, Greedy packet scheduling, SIAM Journal on Computing 24(1):148–157, 1995.
• T. Harks, B. Peis, D. Schmand, B. Tauer, L. Vargas Koch, Competitive packet routing with priority lists, ACM Transactions on Economics and Computation 6(1):4:1–4:26, 2018.

Why financing can convey venture quality

An entrepreneur who knows more about a venture than its investors can convey information through the share of the venture that she keeps. A larger retained share exposes her to more of its uncertain payoff. The cost of this signal depends on what investors buy: an equity claim receives revenue after production costs, while a token claim receives a share of gross revenue. Chod and Lyandres examine how that difference affects the ability of high- and low-quality ventures to separate in an initial coin offering. Their analysis identifies a range of venture heterogeneity and payoff volatility in which tokens support separation and equity does not. The source for this mission is their SSRN working paper, version of December 14, 2019, §4 and Proposition 6.

This result concerns a specific information problem. Investors cannot observe venture quality before buying; an entrepreneur knows her own type. If the same financing contract is used regardless of type, investors cannot identify quality from the offering. A separating outcome instead assigns different sale fractions to the two types and makes the resulting investor beliefs consistent with each type's incentives. The paper compares the feasibility of such outcomes for the two securities, under a model in which the agency effects studied in its earlier sections are set aside.

The two-type financing game

There are two venture types, high $H$ and low $L$. The entrepreneur observes the type; investors observe the fraction $\alpha$ offered for sale. Type $i$ has uncertain shock $X_i=\xi_i^2$ with a normal approximation of mean $\mu_i$ and standard deviation $\sigma$, where $\mu_H>\mu_L$. Revenue is $R_i=X_i/4$. The entrepreneur pays fixed production cost $C$ and initial investment $I$. Her CARA utility at terminal wealth $\omega$ is

$$u_\gamma(\omega)=\gamma^{-1}-\gamma^{-1}\exp(-\gamma\omega),\qquad\gamma>0.$$

Under a belief that the venture has type $j$, investors value the revenue using that type's distribution. An actual type $i$ who sells fraction $\alpha$ therefore receives the cash value $\alpha\mathbb E_j[R_j]$, retains fraction $1-\alpha$ of her own realized revenue, and has expected utility

$$U_{ij}(\alpha)=\mathbb E_i\left[u_\gamma\!\left(\alpha\mathbb E_j[R_j]+(1-\alpha)R_i-C-I\right)\right].$$

The financing method changes the smallest fraction she must sell. The equity financing threshold is $\bar\alpha_j^E=I/(\mathbb E_j[R_j]-C)$, and the token financing threshold is $\bar\alpha_j^T=I/\mathbb E_j[R_j]$. The cost $C$ appears in the equity denominator because equity buyers receive a claim after that cost. With a positive cost, the token threshold is strictly smaller.

Investors use a threshold belief: they infer $H$ when $\alpha\le t$ and $L$ when $\alpha>t$. A separating equilibrium requires both types to prefer the side of the threshold assigned to them, subject to their financing constraints. The paper's conditions (23) and (24) compare the best feasible payoffs on the two sides. A least-cost separating equilibrium is a separating equilibrium that is not Pareto-dominated by another such equilibrium. The paper defines an interior share $\alpha^*$ in equation (25); Proposition 5 identifies its role as the least-cost threshold whenever separation is feasible.

Formalization targets

The central question is when tokens have a signaling advantage: a separating equilibrium exists with tokens, and none exists with equity. Proposition 6 gives two parameter windows. For fixed values of the other parameters, there are thresholds $\mu_l<\mu_u$ and $\sigma_l<\sigma_u$ such that

$$\text{token signaling advantage}\quad\Longleftrightarrow\quad\mu_l\le\mu_L<\mu_u,$$

and, in a separate comparison,

$$\text{token signaling advantage}\quad\Longleftrightarrow\quad\sigma_l\le\sigma<\sigma_u.$$

The first window varies the low-type mean while keeping the high-type mean fixed. Increasing $\mu_L$ reduces the difference between the types. The second varies payoff volatility. Both claims concern the game's equilibrium conditions, rather than only a numerical inequality between closed-form expressions.

The milestone sequence begins with the CARA-normal expected-utility formula (38) and the interior range of $\alpha^*$. It then records the low type's indifference at $\alpha^*$ and the threshold form of condition (24). Proposition 5 characterizes the equilibrium under each security. The remaining milestones compare the financing thresholds and record the monotonicity of $\alpha^*$ with respect to $\mu_L$ and $\sigma$. These are the paper's stated results and intermediate claims in §4 and its appendix.

What the result establishes

The theorem isolates a case in which the form of the security changes what investors can infer. A token offering can permit the high type to sell enough to finance the investment while retaining a stake that the low type does not want to imitate. Equity may require a larger sale fraction, closing that opportunity. The window statement also says the advantage is limited: when types are too different or too similar, or when volatility is outside the relevant range, tokens do not uniquely enable separation under this model.

A machine-checked development would connect an explicit probabilistic payoff model, incentive comparisons over feasible actions, the equilibrium characterization, and comparative statics in one chain. The cited paper proves these results informally; the theorem files here are open proof targets. The CARA-normal calculation and the representation of threshold equilibria are reusable in other signaling models with normally distributed payoffs.

Where the mathematical work lies

The direct comparison of financing thresholds is insufficient for the goal. Separation also depends on whether a low-quality entrepreneur would imitate a high-quality one, and whether a high-quality entrepreneur prefers to reveal her type. These conditions optimize utility over different feasible sale fractions, including a strict boundary on the low-belief side of the threshold. The paper's closed form for $\alpha^*$ expresses the point at which the low type becomes indifferent, but the full result must also establish the high type's incentive and the uniqueness of the refined equilibrium.

The comparative statics require control of two moving parts: the threshold $\alpha^*$ changes with the low-type mean and volatility, while the high-type financing thresholds remain fixed in those comparisons. The interval endpoints in Proposition 6 are existential, so their placement must reflect the feasible parameter domain and the strict or weak inequalities at each boundary.

Formalization scope

Lean represents the normal approximation for $X_i=\xi_i^2$ directly with gaussianReal of mean $\mu_i$ and variance $\sigma^2$. This follows the paper's approximation even though a literal square is nonnegative and a nondegenerate normal variable is not. Revenue is $X_i/4$. Expected utility remains a Gaussian integral; equation (38) is a theorem target, not a definition of that utility. All payoffs and thresholds are real numbers.

The parameter domain has $\gamma>0$, $\sigma>0$, $\mu_L<\mu_H$, $C>0$, $I>0$, and $I\le\mu_L/4-C$. The last two substantive additions to the page's stated model are $C>0$, needed for the strict token-equity threshold comparison, and the low-type financing condition, needed for the paper's action $\alpha_L=1$ to be feasible. An equilibrium threshold satisfies $\bar\alpha_H^i\le t<1$. The least-cost refinement is represented by the paper's operational exclusion of Pareto-dominated separating equilibria, without claiming a general formalization of the Cho–Kreps intuitive criterion.

The high and low incentive conditions quantify only over feasible fractions. Equilibrium payoffs use real suprema on the corresponding action sets; within an equilibrium these sets are nonempty and the utility is bounded above. The goal defines signaling advantage through existence and nonexistence of separating equilibria, so it cannot be discharged by redefining the advantage as the closed-form inequality. Useful contributions include Gaussian expected-utility lemmas, optimization over the feasible intervals, equilibrium existence and uniqueness, and the real-analysis results needed for the parameter windows.

Selected references

• Jacob Chod and Evgeny Lyandres, A Theory of ICOs: Diversification, Agency, and Information Asymmetry, SSRN working paper 3159528, version of December 14, 2019, §4 and Appendix; published in Management Science. Working paper. Published article DOI.

Why this game matters

An optimal stopping game asks two players to choose when to stop a shared process. The first player receives one payoff if they stop first and another if the second player stops first. Such a game changes when one player knows a parameter that the other can only infer from observations. The informed player can reveal information through the timing of a stop, and can conceal it by randomising. De Angelis, Ekström and Glover study this interaction for a diffusion with one of two possible drifts. Their preprint gives a verification theorem for general payoffs and solves a linear geometric Brownian example explicitly. This mission targets the latter result, Theorem 6.10. The result is proved in the paper; the work here is to express its model, strategy classes, supporting results and conclusion in Lean.

The game and its information

The asset value starts at $x>0$ and evolves as a geometric Brownian motion $X_t=x\exp((\mu_\theta-\sigma^2/2)t+\sigma W_t)$, where $\sigma>0$, $\mu_0<0<\mu_1$, and the hidden type $\theta\in\{0,1\}$ selects the drift. Initially $\mathbb P(\theta=1)=\pi\in(0,1)$; write $\phi=\pi/(1-\pi)$ for the initial odds. Player 1 sees the history of $X$ and chooses an almost surely finite stopping time $\tau$ for its augmented observation filtration $\mathcal F^X$. Player 2 also knows $\theta$ and chooses an adapted, nondecreasing control $\Gamma$ for the augmented filtration $\mathcal F^{X,\theta}$. An independent uniform variable $U$ turns this control into the randomised stopping time $\gamma=\inf\{t\ge0:\Gamma_t>U\}$. The initial value $\Gamma_0$ may be positive, representing a jump at time zero.

If $\tau<\gamma$, Player 1 receives $f(X_\tau)$; if $\gamma\le\tau$, Player 1 receives $g(X_\gamma)$. Thus a finite tie pays $g$. The expected payoff is $J(\tau,\Gamma)$. Player 1 maximises it and Player 2 minimises it. A saddle point $(\tau^*,\Gamma^*)$ satisfies $J(\tau,\Gamma^*)\le J(\tau^*,\Gamma^*)\le J(\tau^*,\Gamma)$ for every admissible pair $(\tau,\Gamma)$. In the linear example $f(y)=y$ and $g(y)=(1+\varepsilon)y$, where $\varepsilon>0$.

The uninformed player's posterior probability $\Pi_t=\mathbb P(\theta=1\mid\mathcal F^X_t)$ is expressed through the posterior odds $\Phi_t=\Pi_t/(1-\Pi_t)$. The informed strategy is a pair $(\Gamma^0,\Gamma^1)$, one control for each type. Conditional laws $P^i=P(\cdot\mid\theta=i)$ define the interim payoffs $J^0,J^1$. The scaled ex-ante payoff is $\widehat J=(1+\phi)J$. These quantities permit both an ex-ante saddle-point statement and the agent-form equilibrium statement of Proposition 3.6.

Formalization targets

The supporting targets begin with the filtering and payoff identities of Section 3, the quasi-variational verification result of Theorem 5.1, and the reflected-likelihood and boundary-value facts of Section 6. They culminate in the explicit linear-game equilibrium. Two real numbers $0<A<B$ are determined by equations (90) and (93); piecewise power functions $V_1,V$ are defined by (89) and (91), extended by (94)–(97), and $V_0(\phi)=V(\phi)-\phi V_1(\phi)$. The type-one control $\Gamma^B$ keeps the adjusted odds $\Phi^B=\Phi(1-\Gamma^B)$ below $B$, while Player 1 stops at $\tau_A=\inf\{t:\Phi^B_t\le A\}$.

The goal is Theorem 6.10: $(\tau_A,(0,\Gamma^B))$ is a saddle point, and for every $x,\phi>0$,

$$\widehat J_{x,\phi}(\tau_A,(0,\Gamma^B))=xV(\phi),\qquad J^0_{x,\phi}(\tau_A,0)=xV_0(\phi),\qquad J^1_{x,\phi}(\tau_A,\Gamma^B)=xV_1(\phi).$$

The mission's milestone list follows the paper's stated results. It includes the payoff reductions, Theorem 5.1, reflection at $B$, the ODE bounds, the unique ratio $A/B$, and the verification of the explicit value functions.

What the result establishes

The theorem identifies actual strategies for both players, rather than only showing that the game's upper and lower values coincide. It specifies how the informed player's randomisation depends on the unobserved type and how the uninformed player responds to the adjusted odds. It also gives the ex-ante and both type-conditional payoffs. Without the saddle inequalities over the full strategy classes, the formulas would describe candidate strategies rather than an equilibrium.

A Lean development must capture the paper's information restrictions and time-zero behaviour before the analytical proof can be meaningful. Reusable components include a model-independent two-filtration randomised Dynkin frame, the augmented observation filtrations, randomised stopping times, nonnegative extended payoffs, conditional-law decomposition, and Stieltjes integration with an initial jump. The paper has a written proof; the statements here are open Lean goals, not machine-checked proofs.

Main difficulty

The verification theorem couples a partial differential inequality to a singular control and a stopping time. The adjusted odds can jump when the control jumps, so ordinary continuous-path differential conditions do not by themselves describe the admissible action. The support conditions and transversality limits in Theorem 5.1 are needed to connect the analytic candidate values to payoffs for strategies that can stop at any time. In the linear example, obtaining the power-function candidates is only one part of the target: their free boundaries must be valid, the reflected control must be admissible, and the saddle inequalities must hold against all admissible alternatives.

Formalization scope and conventions

The Lean model uses the explicit strong solution of the §6 GBM on a complete probability space carrying a Brownian motion and independent uniform devices $U,\Theta$. It sets $\theta^\pi=\mathbf1_{\{\Theta<\pi\}}$. Paths of the chosen Brownian modification are continuous. Player 1's filtration is generated by $X$ plus null sets; Player 2's also contains $\theta$; neither contains $U$. Stopping times live in $[0,\infty]$, with Player 1 required to stop almost surely. Payoffs are nonnegative extended integrals and equal zero if both stopping times are infinite. The Stieltjes convention counts $\Gamma_0$.

The posterior odds $\Phi$ use the GBM closed form. The running-maximum formula defines $\Gamma^B$ and permits its initial jump. The tilted law used in Lemma 6.5 is represented by an equivalent likelihood-path law. Theorem 5.1 is stated for the GBM instance with general continuous $0\le f\le g$ and relative closures inside $(0,\infty)^2$. Its localisation integral retains the factor printed in the preprint. The explicit boundaries, controls and values in the goal are definitions, never free variables or hypotheses; the saddle inequalities quantify over the full player strategy classes.

There is a normalization slip in the paper's (23): it prints $\Phi_t=dP^1/dP^0$ on $\mathcal F^X_t$, although $\Phi_0=\phi$ and a Radon–Nikodym derivative at time zero equals one. Equations (20)–(21) give $dP^1/dP^0=\Phi_t/\phi$. The formal filtering item uses that corrected identity. Equation (50) similarly identifies the ex-ante value with the scaled payoff; the formal target records $\widehat J=(1+\phi)J$ and states the payoff identities without confusing the two. The source's domain $\mathbb R_+^2$ in Theorem 6.10 is read as $x,\phi>0$, as required by the model. These readings are documented in the local moderation notes.

Selected references

• T. De Angelis, E. Ekström and K. Glover, Dynkin Games with Incomplete and Asymmetric Information, arXiv preprint 1810.07674v5, 2020. Preprint.

Why the business-model choice matters

Residential solar panels can reach customers through a purchase, a lease, or a power purchase agreement (PPA), under which the customer pays for the electricity the panels generate. These arrangements allocate panel ownership, subsidy receipts, and generation risk differently. A company choosing prices for all three therefore also chooses which customers adopt each arrangement. Agrawal, Toktay and Yücel study that choice in a model with net-metered electricity, investment and generation subsidies, and customers who differ in expected solar generation. Their main structural result identifies the company's optimal mix as panel cost and the investment subsidy change. The subsequent results about subsidy effects, renewable adoption, and restrictions on leasing use this mix as their starting point. Agrawal, Toktay and Yücel (2022).

Customers, prices and profit

One solar power company sets a normalized monthly sales price $s$, a monthly lease fee $l$, and a PPA price $p$ per unit of generation. A customer can choose sale $S$, lease $L$, PPA $P$, or continued electricity supply from the utility $U$. The customer has expected monthly solar generation $\eta$ and expected electricity demand $d$. The retail electricity price is $r$; $\alpha$ is the fraction of panel investment cost covered by an investment subsidy, $\beta$ is the generation subsidy per unit, $t$ is the company's PPA monitoring cost per unit, and $c$ is its normalized panel cost. Under net metering, the customer's utility bill is $r(q-n)$ when usage is $q$ and generation is $n$. The paper's expected monthly costs of the four choices are

$$C_S=(1-\alpha)s+r(d-\eta)-\beta\eta,\quad C_L=l+r(d-\eta),\quad C_P=p\eta+r(d-\eta),\quad C_U=rd.$$

The customer chooses a least-cost option. Expected generation is uniform on $[0,g]$ and independent of expected demand, whose distribution has positive support. Let $N^i(s,l,p)$ be the population share choosing option $i$ and $G^i(s,l,p)$ the total expected generation among those customers. An option is offered when its share is positive. The company's expected monthly profit, equation (1) of the source, is

$$\Pi(s,l,p)=(s-c)N^S+\bigl(l-(1-\alpha)c\bigr)N^L+\beta G^L +(p+\beta-t)G^P-(1-\alpha)cN^P.$$

These amounts come from actual customer choices, so their adoption shares are nonnegative by definition. The sales-only benchmark, in which customers choose between $S$ and $U$, yields the panel-cost bound $C_0=g(r+\beta)/(1-\alpha)$. The source restricts its main analysis to $c<C_0$. Agrawal, Toktay and Yücel (2022), §§3–4 and Online Appendix A.

Formalization targets

The goal is Proposition 1, the global choice of business models. Write $A_2=\beta/(\beta+r)$. When $\alpha<A_2$, there are panel-cost thresholds $C_1\le C_2$ such that every profit-maximizing price triple has the offer set

$$\{P,S\}\quad(c<C_1),\qquad \{P,L,S\}\quad(C_1<c<C_2),\qquad \{L,S\}\quad(C_2<c<C_0).$$

When $A_2\le\alpha$, a threshold $C_3$ separates $\{P,S\}$ for $c<C_3$ from $\{S\}$ for $C_3<c<C_0$. The same thresholds apply as $c$ and the admissible demand distribution vary, and a maximizing price triple exists for each admissible $c$. A zero-width middle regime is allowed when $C_1=C_2$. The equality points at $C_1,C_2,C_3$ are excluded because the appendix's candidate cases become degenerate or have tied global optima there, so the printed assignment at those points does not hold for every maximizer. Agrawal, Toktay and Yücel (2022), Proposition 1 and proof.

The milestones establish the common optimal electricity usage of Lemma 1, customer segmentation by $\eta$ in Lemma 2, and the sales-only profitability limit of Lemma A.1. They then identify the best profits in the regions $p\le r$ and $p>r$ and compare those profits across the investment-subsidy regimes. The mission follows the author's source indices and case names, including the appendix's closed-form candidate prices and values. Agrawal, Toktay and Yücel (2022), pp. 11, 14 and OA1–OA8.

What the result enables

The proposition states when a company can profitably maintain PPA, leasing, and sales side by side, and when it optimally drops one or both non-ownership models. This matters for the paper's later claims: a change in a subsidy or a legal restriction may alter not only prices within one model but which models serve customers at all. The paper's comparisons of total adoption, generation, and utility-firm profit therefore depend on the equilibrium classification. Agrawal, Toktay and Yücel (2022), Propositions 2–6.

The mathematical result is already proved in the source. This mission supplies compiled Lean statements for its model and central claims; the theorem proofs remain open. Completing them would provide a machine-checked route from individual cost comparisons and population integrals to the global pricing decision. The customer-choice and adoption definitions can also support formal work on the paper's later subsidy and restriction results. No machine-checked proof of these draft theorems is claimed here.

Main difficulty

Comparing customer costs at a fixed price triple gives generation intervals, but it does not by itself identify the company's best prices. The company optimizes three prices while the adopting population changes at interval boundaries. In the appendix, the resulting problem has distinct candidates when $p\le r$ and $p>r$, and its preferred candidate changes with both $c$ and $\alpha$. A direct comparison of two displayed candidate profits is therefore insufficient unless the candidate is optimal throughout its stated region and all boundary cases are accounted for. At a cost where two regional values agree, different maximizing price triples can have different offer sets. Agrawal, Toktay and Yücel (2022), proof of Proposition 1, OA4–OA8.

Formalization scope

Lean represents prices by three real coordinates and parameters by one structure. The standing conditions are $0<\alpha$, $0<\beta$, $0<t<r$, $\beta<r$, $0<g$, and $\alpha<A$, where $A=\sqrt{\beta(r+t)/(r(r+\beta)+\beta t)}$ is the paper's concavity threshold. Lemma 2 and Lemma A.1, which the paper states before introducing $\beta<r$ and $\alpha<A$ on p. 15, assume only the §3 conditions (and $\alpha<1$ for Lemma A.1). The goal also assumes $0<c<C_0$. Its demand distribution is an arbitrary probability measure concentrated on $(0,\infty)$, which generalizes the paper's density $h(d)$ without changing the claims, because the choice comparisons do not depend on $d$. Generation uses the uniform probability law on $[0,g]$ and integrates $\eta$ over the actual choice sets.

The four realized and expected costs are defined separately. Ties among $S,L,P$ use a fixed priority order; $U$ is selected only if strictly cheaper than all three solar options. This implements the appendix's allocation to PPA at $p=r$, where PPA and utility costs tie on a set of positive mass. The theorem ranges over all real price triples. Its offer set is calculated from positive adoption at a maximizer, and it asserts existence of that maximizer; neither the offer regime nor optimality is assigned by a case label. The cost thresholds are chosen before quantifying over the demand distribution and $c$. A milestone using $\eta_2=l/p$ requires $p>0$, and the closed-form denominators are used only under the stated parameter conditions. Population measures are finite, and the choice regions are measurable; these facts matter when converting adoption mass to a real number and integrating generation. The sales-only benchmark and the appendix formulas are separate definitions, not substitutes for equation (1).

Contributions are welcome on customer-choice measurability, integral identities for adoption and generation, the regional maximization claims, and the algebraic value comparisons. Propositions 2–6 and the Technical Appendix's alternative policy models are outside this mission.

Selected references

• V. V. Agrawal, L. B. Toktay and Ş. Yücel, Non-Ownership Business Models for Solar Energy, Manufacturing & Service Operations Management, 2022; authors' manuscript dated 18 September 2021 used for the page and theorem citations here. DOI: 10.1287/msom.2021.1049.

Motivation

Large manufacturers procure components by competitive bidding, and many of them also run cost-reduction investigations: the buyer's engineers visit a supplier's plant and look for process changes that lower the cost of the contracted part. The savings are passed to the buyer as a lower contract price. In practice such investigations usually happen after the contract is awarded, on the winner only. Chen, Beil and Duenyas (Operations Research 70(6), 2022) compare that convention with a mechanism in which the buyer investigates before the award, possibly several suppliers, and then awards the contract on the investigated prices.

Investigating before the award obviously helps the buyer for fixed bids: she sees more cost reductions before choosing. The question is whether suppliers lose. The buyer keeps every identified saving, and investigations of competitors make their prices more aggressive, so suppliers seem to have reason to resist. The paper shows that, when suppliers are ex ante symmetric, they do not: every supplier's ex ante expected profit is at least as high when investigations come before the award. This mission formalizes that result.

Setting

A buyer procures one contract from suppliers $\mathcal N=\{1,\dots,N\}$ and must transact with one of them. Supplier $i$ has a private cost $c_i=\Delta^c_i+\epsilon^c_i$, where $\Delta^c_i\ge0$ is public and $\epsilon^c_i$ has density $f$ on $[\underline c,\bar c]$ with mean $0$; so $c_i$ has density $f_i(c)=f(c-\Delta^c_i)$, c.d.f. $F_i$, and support $C_i=[\underline c_i,\bar c_i]$. Costs are independent.

An investigation of supplier $i$ costs the buyer $d\ge0$ and reveals a cost reduction $t_i=\Delta^t_i+\epsilon^t_i\ge0$, where $\epsilon^t_i$ has density $g$ on $[\underline t,\bar t]$ with mean $0$, independently of everything else. At most $\hat N\in\{1,\dots,N\}$ suppliers can be investigated, and costs always exceed reductions: $\Delta^t_i+\bar t<\Delta^c_i+\underline c$. Each supplier submits a sealed bid $b_i\in B_i=[0,\bar c_i]$. If an investigated supplier wins, he is paid his updated bid $b_i-t_i$ and his cost becomes $c_i-t_i$, so his margin is $b_i-c_i$ in every case.

• BAI (bid, award, investigate). The buyer awards the contract to the lowest $\lambda_i=b_i-r_i$, where $r_i=\max\{0,\Delta^t_i-d\}$ is the expected saving from investigating the winner afterwards. Ties are broken at random.
• BIA (bid, investigate, award). The buyer investigates sequentially. Each round she uses the bids and the reductions revealed so far to stop or to investigate one more supplier, and stopping is final. She then awards the contract to the lowest updated bid. Her policy minimizes the expected payment plus investigation cost, problem (1). Theorem 1 solves (1) by an index policy: with $\tau$ the root of $d=\int_\tau^\infty(\epsilon^t-\tau)\,dG(\epsilon^t)$, each supplier gets the index $\mu_i(b_i)=b_i-\max\{0,\tau+\Delta^t_i\}$. The buyer investigates in increasing order of index while the current lowest updated bid is at least the next index, up to a cap $\bar N\le\hat N$.

Supplier $i$'s winning probability at bids $b$ is $W_i(b)$, over $t$ and the tie-break. With the others bidding $\beta_{-i}(c_{-i})$, his expected profit from bidding $b$ at cost $c$ is $u_i(b;c)=(b-c)\,\mathbf E_{c_{-i}}[W_i(b,\beta_{-i}(c_{-i}))]$, equation (5). A Bayesian Nash equilibrium is a profile of strategies $\beta_i:C_i\to B_i$ that are best replies at every type. Supplier $i$'s ex ante expected profit is $\mathbf E_{c_i}[u_i(\beta_i(c_i);c_i)]$.

Formalization targets

Goal: Theorem 2 (weak form)

Suppose that suppliers are ex ante symmetric ($\Delta^c_i=\Delta^c$, $\Delta^t_i=\Delta^t$), that $F_i/f_i$ is nondecreasing (Assumption 1), and that $d<\max_i\Delta^t_i$ (Assumption 2). Let $\beta^{\mathrm{BIA}}$ be a symmetric equilibrium of BIA, and $\beta^{\mathrm{BAI}}$ a symmetric nondecreasing equilibrium of BAI. Then for every supplier $i$,

$$\mathbf E_{c_i}\big[u^{\mathrm{BAI}}_i(\beta^{\mathrm{BAI}}_i(c_i);c_i)\big]\;\le\;\mathbf E_{c_i}\big[u^{\mathrm{BIA}}_i(\beta^{\mathrm{BIA}}_i(c_i);c_i)\big].$$

Milestones

1. Proposition 1. There exists an equilibrium $\check\beta$ of the first-price auction with costs $c_i-r_i$ whose shifted strategy $\tilde\beta_i(c_i)=\check\beta_i(c_i-r_i)+r_i$ is a BAI equilibrium.
2. Theorem 1(a). The index policy (3) minimizes the buyer's expected cost (1) over all admissible sequential policies, for every bid vector.
3. Zero profit at the top. $U^{\mathcal M}_i(\bar c_i)=0$ for $\mathcal M\in\{\mathrm{BIA},\mathrm{BAI}\}$.
4. Envelope formula (A.2). $U^{\mathcal M}_i(c_i)=U^{\mathcal M}_i(\bar c_i)+\int_{c_i}^{\bar c_i}\phi^{\mathcal M}_i(y)\,dy$.
5. Ex ante identity. $\mathbf E_{c_i}[U^{\mathcal M}_i(c_i)]=U^{\mathcal M}_i(\bar c_i)+\mathbf E_{c}\big[A^{\mathcal M}_i(c)\,F_i(c_i)/f_i(c_i)\big]$.
6. Pointwise comparison. At cost vector $c$ and realized reduction vector $t$, $\sum_i A^{\mathrm{BAI}}_i(c) F_1(c_i)/f_1(c_i)=\min_i F_1(c_i)/f_1(c_i)\le\sum_i A^{\mathrm{BIA}}_i(c,t) F_1(c_i)/f_1(c_i)$ almost everywhere, with $\sum_iA^{\mathcal M}_i=1$.

Significance

The theorem identifies a win-win procurement design. With symmetric suppliers, a buyer who chooses the cheaper of BAI and BIA weakly lowers her own cost, and this choice never lowers any supplier's ex ante profit. The gain does not come from sharing savings, since the buyer keeps all identified savings. It comes from strategic bidding: under BIA a supplier need not submit the lowest initial bid to win, so price competition at the bid stage softens. The paper's Figure 1 shows the higher BIA bid curves. Theorem 1 is of independent interest: it is an index solution of a capped sequential search problem in which an uninvestigated bid may still win.

The paper proves the result on paper. To our knowledge none of it is machine-checked. A formalization adds three things. It makes the mechanisms precise, including the tie-breaking and the stopping rule that the text leaves partly implicit. It pins down the right inequality: the printed "higher" is not strict, and with a single supplier both mechanisms give the same profit. It also produces reusable components: an envelope-theorem layer for bidding games with an indirect mechanism, and a capped-search index theorem.

Difficulty

The proof of Theorem 2 needs the BIA winning probability only through its total, $\sum_i A^{\mathrm{BIA}}_i=1$. Everything else rests on three technical steps. The first is the envelope formula (A.2) for an indirect mechanism whose allocation $W_i$ has no closed form and need not be continuous in the bid. The usual argument assumes a differentiable direct mechanism and does not apply as stated. The second is the claim that in BAI the lowest-cost supplier wins almost surely. That needs a symmetric equilibrium that is not merely nondecreasing but free of pooling, and this must be derived from the equilibrium conditions. The third is the "by symmetry" step that equates each supplier's ex ante profit with the average over suppliers. It needs both the equilibria and the mechanisms to be invariant under relabelling the suppliers.

Theorem 1(a) is a dynamic program over adaptive policies with a cap and an outside option. A Weitzman-style argument must handle a cap $\bar N$ and suppliers whose index makes investigation worthless ($\tau_i=0$). It cannot simply be imported from Pandora's-box results.

Formalization scope

Suppliers are Fin N with $N\ge1$; all values are real numbers. A single definitions module PreAwardInvest.WinWin.Model contains the following.

• Parameters and assumptions. The parameters, and the standing assumptions of §3.1 (densities with mean zero, nonnegative costs and reductions, footnote 6, $1\le\hat N\le N$, $d\ge0$), with $f>0$ on $(\underline c,\bar c)$ added. Assumptions 1 and 2 are separate predicates.
• Laws. The cost and reduction laws are densities with respect to Lebesgue measure, and their vectors have product laws.
• Policies. A policy reads the bids, the investigated set and the revealed reductions. An admissible policy is nonanticipative and measurable in the reductions, and stopping is final.
• Index policy. It takes $\tau$ as any root of its equation. Ties in the ranking and in both awards are broken by one uniformly random priority order, so that BIA and BAI are symmetric under relabelling. Theorem 1(a) compares policies for bids in $B_i=[0,\bar c_i]$.
• Profits and equilibria. Profits follow (5), with the expectation over $c_{-i}$ taken over the whole cost vector with coordinate $i$ overwritten. Equilibria require measurable strategies into $B_i=[0,\bar c_i]$. Ex ante profit is the expectation of the equilibrium profit, not the Myerson virtual-cost expression.

Several conventions are disclosed hypotheses or corrections. The goal uses $\le$ in place of the printed "higher". The equilibria in the goal are assumed symmetric, and the BAI one nondecreasing (Lemma 1's class). Strict monotonicity is not assumed, because with one supplier the equilibrium bid is the constant $\bar c_1$.

The goal is not trivialized. BAI awards on bids through $\lambda_i=b_i-r_i$ and BIA runs the index policy on bids and revealed reductions. Neither mechanism has "lowest cost wins" built in, which is milestone 6. Ex ante profit is defined from (5), so milestones 4–5 are not definitional. A sorry-free check exhibits a one-supplier instance that satisfies every hypothesis of the goal. In it both ex ante profits equal $1/2$.

Not formalized: Theorem 1(b)–(c), Lemma 1 (existence via Athey 2001), the closed form (4) of $W_i$, the asymmetric results (Propositions 2–4), the buyer-cost comparison (Theorem 3), the optimal mechanism (Theorem 4), and the extensions of §9. Contributions welcome: the envelope theorem for monotone-selection bidding games, measurability of the winning probabilities, and the index policy's optimality.

Selected references

• Q. Chen, D. R. Beil, I. Duenyas, Procurement mechanisms with post-auction pre-award cost-reduction investigations, Operations Research 70(6):3054–3075, 2022. https://doi.org/10.1287/opre.2022.2349 (accepted manuscript: LBS Research Online eprint 2544).
• S. Athey, Single crossing properties and the existence of pure strategy equilibria in games of incomplete information, Econometrica 69(4):861–889, 2001. https://doi.org/10.1111/1468-0262.00223
• R. B. Myerson, Optimal auction design, Mathematics of Operations Research 6(1):58–73, 1981. https://doi.org/10.1287/moor.6.1.58
• P. Milgrom, I. Segal, Envelope theorems for arbitrary choice sets, Econometrica 70(2):583–601, 2002. https://doi.org/10.1111/1468-0262.00296
• M. L. Weitzman, Optimal search for the best alternative, Econometrica 47(3):641–654, 1979. https://doi.org/10.2307/1910412
• V. Krishna, Auction Theory, 2nd ed., Academic Press, 2009. https://doi.org/10.1016/C2009-0-22474-3

How often should a robo-advisor talk to its client?

A robo-advisor is an automated portfolio manager. It invests a client's wealth according to a model of the client's risk preferences, and it learns those preferences by interacting with the client: questionnaires, check-ins, requests to confirm or revise a risk profile. The design question of how often such a system should query its client is practical: each interaction updates the advisor's view of a preference that drifts over time, but each interaction is also exposed to the client's momentary reaction to recent market moves.

Capponi, Ólafsson and Zariphopoulou (Management Science 68(4), 2022; read here as arXiv:1911.01391v2) model this trade-off. Their Proposition 5.1 gives a closed-form approximation of how well the portfolio tracks the client's true risk aversion as a function of the time between interactions, and shows that this approximation has a unique optimal interaction time whose position responds monotonically to the model's parameters. This mission formalizes part (ii) of that proposition and the comparative statics (5.6).

Setting

Time is discrete. The client's true risk aversion $\gamma^C_n$ evolves over the investment horizon; in each period it receives, with probability $p_\epsilon \in [0,1]$, an idiosyncratic shock $\sigma_\epsilon W_n - \sigma_\epsilon^2/2$ with $W_n$ standard Gaussian and $\sigma_\epsilon > 0$, and no shock otherwise (p. 17). The robo-advisor and client interact every $\phi \ge 1$ periods. At an interaction the client communicates a risk-aversion parameter that is distorted by a behavioral bias: it is the true value multiplied by $e^{-\beta \cdot(\text{average excess market return since the last interaction})}$, where the coefficient $\beta \ge 0$ measures the strength of the bias (eq. (5.2), pp. 17–18). Between interactions the advisor keeps using the last communicated value. Market returns have volatility $\sigma(y) > 0$ in economic state $y$, and $\sigma_0 := \sigma(Y_0)$ is the volatility in the initial state.

The personalization measure (5.4) is the expected time-average relative error between the advisor's risk tolerance $1/\gamma_n$ and the client's $1/\gamma^C_n$,

$$\mathcal R(\phi,\beta) = \mathbb E\Big[\frac1T\sum_{n=0}^{T-1}\Big|\frac{1/\gamma_n - 1/\gamma^C_n}{1/\gamma^C_n}\Big|\Big].$$

Lower is better. Proposition 5.1(i) shows that $\mathcal R$ is, up to error terms, a multiple of the approximate personalization measure

$$\widetilde{\mathcal R}(\phi,\beta) = \sqrt{\frac{2}{\pi}}\left(\frac{\beta\sigma_0}{\sqrt{\phi}}\Big(1-\frac{\phi-1}{2}p_\epsilon\Big) + \sqrt{\frac{\beta^2\sigma_0^2}{\phi}+\sigma_\epsilon^2}\;\frac{\phi-1}{2}p_\epsilon\right).$$

The first term is the bias cost, which shrinks as interactions become rarer (the bias averages returns over a longer window); the second is the staleness cost, which grows with the number of shocks missed between interactions. The mission is about $\widetilde{\mathcal R}$, as Proposition 5.1(ii) is. In Lean the parameters are a structure Params with fields sig0 ($\sigma_0$), pe ($p_\epsilon$), se ($\sigma_\epsilon$), β, and $\widetilde{\mathcal R}$ is Rtilde P φ.

Formalization targets

Goal: Proposition 5.1(ii) and (5.6)

Assume $\sigma_0 > 0$, $\sigma_\epsilon > 0$, $p_\epsilon \in [0,1]$, $\beta \ge 0$ and $\beta + p_\epsilon > 0$. Then

$$\arg\min_{\phi\ge1}\widetilde{\mathcal R}(\phi,\beta) = \begin{cases} 1, & \beta = 0,\\ \phi_0\in[1,\infty), & \beta>0,\ p_\epsilon>0,\\ \infty, & p_\epsilon = 0,\end{cases}$$

and $\phi_0$ is increasing in $\beta$ and $\sigma_0$ and decreasing in $p_\epsilon$ and $\sigma_\epsilon$ (5.6). "$\arg\min = \infty$" means that no $\phi \ge 1$ is a minimizer, $\widetilde{\mathcal R}$ decreases strictly on $[1,\infty)$ and tends to its infimum $0$.

Milestones

The proof (Appendix C, p. 46) works with the bracket $f = \sqrt{\pi/2}\,\widetilde{\mathcal R}$ and an auxiliary function $g$ with $f'(\phi) = \tfrac12\beta\sigma_0p_\epsilon\phi^{-2}g(\phi)$. The milestones are its displayed claims, in order: $f \ge 0$; the two degenerate cases $p_\epsilon = 0$ and $\beta = 0$; the factorization of $f'$; the value of $f'(1)$ and the criterion $f'(1) \ge 0 \iff p_\epsilon\sigma_\epsilon^2/(\beta^2\sigma_0^2) \ge 2 + 1/p_\epsilon$; the sufficient condition $p_\epsilon\sigma_\epsilon/(\beta\sigma_0) < 1 \Rightarrow \partial_\phi\widetilde{\mathcal R}|_{\phi=1} < 0$ of p. 22; the lower bound $g'(\phi) \ge \tfrac12\phi^{-1/2}g(1)$, which settles the corner case $g(1)\ge 0$; and the interior case $g(1) < 0$, where $g$ is strictly convex, tends to $\infty$, and has a unique zero at which $f$ is minimized.

Significance

The result gives the model's two qualitative predictions in exact form. Without behavioral bias the advisor should interact at every period; without idiosyncratic shocks it should never interact; when both are present there is a single best interaction frequency, and it moves in the economically expected direction: more bias or more volatile markets call for rarer interaction, more frequent or larger preference shocks call for more frequent interaction. The p. 22 criterion gives a checkable condition, in terms of $p_\epsilon\sigma_\epsilon$ against $\beta\sigma_0$, under which interacting at every period is not optimal.

The proof in the paper is a sketch. The convexity of $g$ in the interior case is asserted ("it can be shown"), and the comparative statics (5.6) are stated as following from "the form of the function $f$". As printed, (5.6) asserts strict signs of partial derivatives of $\phi_0$, which fail on the open parameter region where the minimizer sits at the corner $\phi_0 = 1$ (there $\phi_0$ is locally constant). A machine-checked proof therefore supplies the missing convexity argument and the corrected comparative statics. No part of the proposition is known to be formalized.

Difficulty

The function $\widetilde{\mathcal R}$ mixes $\phi^{-1/2}$, $\phi^{1/2}$ and a square root of $\beta^2\sigma_0^2/\phi + \sigma_\epsilon^2$. The sign of its derivative is not visible from the formula, and the paper's sign analysis passes through $g$; the paper's claim that $g$ is strictly convex has no written proof. The comparative statics are not a differentiable implicit-function computation either: the minimizer switches between the corner $\phi = 1$ and an interior root of $g$, and the monotonicity must hold across that switch. The obvious move of differentiating the first-order condition $g(\phi_0) = 0$ in the parameters covers only the interior region and says nothing at the corner.

Formalization scope

All quantities are real. The time between interactions $\phi$ is a real variable on $[1,\infty)$: the model uses integer $\phi$, but Proposition 5.1 differentiates in $\phi$ and places $\phi_0$ in $[1,\infty)$. The standing ranges $\sigma_0 > 0$, $\sigma_\epsilon > 0$, $p_\epsilon \in [0,1]$, $\beta \ge 0$ are bundled in Params.Standing. "$\phi$ minimizes $\widetilde{\mathcal R}$" is the predicate IsOptInteraction P φ: $\phi \ge 1$ and $\widetilde{\mathcal R}(\phi) \le \widetilde{\mathcal R}(\psi)$ for all $\psi \ge 1$; there is no argmin function, so no junk value can satisfy the goal. Square roots are Real.sqrt, $\phi^{3/2}$ is $\phi\sqrt\phi$, and every statement restricts $\phi$ so that no radicand is negative and no denominator vanishes. Derivatives are stated with HasDerivAt and an explicit value. Rtilde P φ takes $\phi$ last, while the page writes both $\widetilde{\mathcal R}(\phi,\beta)$ and $\widetilde{\mathcal R}(\beta,\phi)$.

Two readings are fixed. The case "$\arg\min = \infty$" is: no minimizer exists, $\widetilde{\mathcal R}$ is strictly decreasing on $[1,\infty)$, and $\widetilde{\mathcal R}(\phi) \to 0$. The comparative statics (5.6) are stated as monotone comparative statics: if a parameter increases (keeping $p_\epsilon \le 1$), the minimizer moves weakly in the stated direction, and strictly whenever the original minimizer exceeds $1$. The monotonicity clauses quantify over minimizers for both parameter sets, and the existence clause of the goal ensures both exist, so they are not vacuous. Stating the goal about $f$ alone, or defining $\phi_0$ by sInf or by a formula, would trivialize the claim; the goal is about $\widetilde{\mathcal R}$ and its minimizers.

Part (i) of Proposition 5.1, which relates $\mathcal R$ to $\widetilde{\mathcal R}$ with unquantified $O(\cdot)$ error terms, is not formalized; neither is the optimal investment strategy of Proposition 4.1. The development needs one-variable real calculus from Mathlib, including square-root and quotient derivatives, monotonicity and convexity on intervals, and limits at infinity. Proofs of the milestones, of the convexity of $g$ on all of $[1,\infty)$ (which appears to hold without the hypothesis $g(1) < 0$), and of the derivative form of (5.6) on the interior region are all welcome.

Selected references

• A. Capponi, S. Ólafsson, T. Zariphopoulou, Personalized Robo-Advising: Enhancing Investment through Client Interaction, Management Science 68(4), 2022; preprint arXiv:1911.01391v2 (the version cited for all page and equation numbers). https://arxiv.org/abs/1911.01391

Motivation

On-demand service platforms (ride-hailing, delivery, home services) do not employ their workers. They set a price for customers and a wage per unit of work, and independent agents decide how much time to make themselves available. A recurring policy question, raised by regulators and labor advocates alike, is whether platforms should be allowed to recruit labor pools of unlimited size: a larger pool is often argued to depress what each worker earns. Benjaafar, Ding, Kong and Taylor (SSRN 3103447; published in Manufacturing & Service Operations Management, doi:10.1287/msom.2020.0964) study this question in a model where customers care about delay. Their central result, Theorem 2, is that the answer depends on delay sensitivity: in a standard market a larger pool lowers average labor welfare, but when customers are delay-sensitive, average labor welfare first rises and then falls in the pool size.

Setting

The model has two populations, both treated as continua.

Agents. A labor pool of mass $N>0$. An agent with opportunity-cost parameter $a$ who is available for time $x$ incurs cost $a x^2$; $a$ has distribution $F$ on $[\underline a,\bar a]$ with $0<\underline a$. Given the wage $w$, demand $D$ and labor supply $S$, work is shared in proportion to availability, so the agent's effective wage is $w_e=wD/S$ and his best response is $x^*(a)=wD/(2aS)$. Aggregation gives the labor supply equation

$$S=\sqrt{wDN\,E[1/a]/2}.$$

Customers. Needs arise at rate $\Lambda$ (the market size); a customer with valuation $v\sim\mathrm{Unif}[0,\bar v]$ seeks service if $v-p-hW\ge 0$, where $h\ge0$ is the delay sensitivity and

$$W=\frac{(D/S)^\beta}{S-D},\qquad \beta\ge1,$$

is the delay. Demand is $D=\Lambda[1-G(p+hW)]$ with $G$ the uniform cdf, and an equilibrium requires $D<S$. In the benchmark $h=0$ demand is $\Lambda[1-G(p)]$ and the capacity constraint is $D\le S$.

Platform. The platform chooses $p\ge0$, $w\ge0$ to maximize $(p-w)D$ subject to these equilibrium conditions; the optimum is $(p^*,w^*,D^*,S^*)$. The agent utilization is $\rho^*=D^*/S^*$, and average labor welfare is

$$\overline{LW}=\int\Big[\frac{w^*D^*}{S^*}x^*(a)-a\,x^*(a)^2\Big]dF(a).$$

The pool sizes for which a positive optimum exists are $N>\underline N$, with $\underline N=0$ for $\beta>1$ and $\underline N=8h/(\bar v^2E[1/a])$ for $\beta=1$.

Formalization targets

Goal: Theorem 2 (p. 11)

1. If $h=0$: $w^*$, $w^*_e$ and $\overline{LW}$ are strictly decreasing in $N$.
2. If $h>0$: $w^*$ is strictly decreasing in $N$ on $(\underline N,\infty)$, and for each $Q\in\{D^*/S^*,\ w^*_e,\ \overline{LW}\}$ there is $N_0>\max(0,\underline N)$ with

$$Q\ \text{strictly increasing on}\ (\underline N,N_0),\qquad Q\ \text{strictly decreasing on}\ (N_0,\infty).$$

The thresholds are not given in closed form; the goal asserts only their existence.

Milestones (in attack order)

• Lemma 11 (p. OA1): unique positive market equilibrium for each admissible $(p,w)$.
• (8)–(9) (p. OA1): price, wage and profit as functions of $(D,S)$; (10): $\overline{LW}=E[1/a]\,w_e^2/4$.
• Lemma 12 (p. OA2): the revenue-maximizing demand $\tilde D(S)$ increases in $S$ and $\Pi(\tilde D(S),S)$ is single-peaked at $S^*$.
• Lemma 1 (pp. 9–10): a unique optimum exists iff $\beta>1$ or $\beta=1$ and $N>8h/(\bar v^2E[1/a])$.
• (17)–(18) (p. OA7): first-order conditions at the optimum.
• Lemma 13 (p. OA4): $S^*$, $D^*$ increase in $N$; $S^*\to\infty$, $D^*\to\Lambda/2$; $S^*,D^*,\rho^*\to0$ as $N\downarrow\underline N$.
• Case $h=0$ of the proof (pp. OA4–OA5): $D^*=S^*=\bar v/(2(\bar v/\Lambda+2/(NE[1/a])))$, $w^*=\bar v\Lambda/(\bar vNE[1/a]+2\Lambda)$.
• Parts (i)–(iv) of the proof (pp. OA5–OA7): the threshold statements for $w^*_e$, $\rho^*$ and $\overline{LW}$, the identity $w^*=\tfrac12\bar v-\bar vD^*/\Lambda$, and the monotonicity of $w^*$.

Significance

The result. Theorem 2 separates two regimes. In a congestion regime (small pools, large delay cost $hW^*$) extra agents reduce delay, stimulate demand faster than supply grows, and raise utilization, the effective wage and average labor welfare: agents exert a positive externality on one another. In a cost regime (large pools) the demand effect is exhausted and extra agents only dilute work. The paper uses this to argue against blunt caps on platform labor pools and as the baseline for its analysis of nominal and effective wage floors (§5). Without delay sensitivity the classical conclusion, that a larger pool lowers welfare, is recovered exactly.

Formalizing it. The theorem is proved in the paper, with an online appendix of implicit-function and envelope arguments. None of it is formalized. This mission produces a machine-checked model of a platform with endogenous supply and congestion-dependent demand, the reduced $(D,S)$ problem, and the comparative statics in $N$. The paper's Lemma 11 needs a correction at $\beta=1$ (see below), which is the kind of gap a formal development exposes.

Difficulty

The optimum is defined implicitly by two nonlinear first-order conditions, and there is no closed form for $h>0$. The obvious route, differentiating $w^*_e=2S^*/(NE[1/a])$ in $N$, gives a quantity whose sign is the competition between the growth of $S^*$ and the factor $1/N$, and that sign changes with $N$. Monotonicity arguments of the usual kind (supermodularity in $(S,N)$, which does give that $S^*$ increases) say nothing about such ratios. The obstacle is single crossing of a quantity defined only implicitly through the optimum, not differentiability. The boundary behaviour at $N\downarrow\underline N$ and $N\to\infty$ (Lemma 13) is also needed and is itself nontrivial at $\beta=1$, where $\underline N>0$.

Formalization scope

Everything lives in the namespace LaborWelfare.PoolSize, with one definitions file Setting.

• Parameters. $\bar v>0$ (vbar), $\Lambda>0$ (Lam), $h\ge0$, real $\beta\ge1$ (beta), and $F$ a probability measure on $\mathbb R$ carried by $[\underline a,\bar a]$ with $0<\underline a\le\bar a$. The density of $F$ is not required: only $E[1/a]=\int a^{-1}dF$ enters any result. $(D/S)^\beta$ is a real power.
• $N$ is a real number; all results are about functions of $N$ on $(\underline N,\infty)$ (on $(0,\infty)$ for $h=0$, where $\underline N=0$).
• Equilibrium. $D>0$, $S>0$, (2), (3)–(4), and $D<S$ for $h>0$, $D\le S$ for $h=0$; the uniform cdf is clamped to $[0,1]$.
• The optimum is an outcome maximizing $(p-w)D$ over every price $p\ge0$ and wage $w\ge0$ subject to the market equilibrium. Statements quantify over a selection $N\mapsto$ optimal outcome, which Lemma 1 (and the $h=0$ milestone) show exists and is unique on the regime, so the monotonicity claims concern the platform's actual optimum and cannot be met by a degenerate outcome or a vacuous hypothesis.
• Labor welfare is the integral of the page, not its closed form; the closed form is milestone (10).
• Strictness. "Increasing" and "decreasing" are strict (StrictMonoOn, StrictAntiOn), as the paper fixes on p. 11; the thresholds are three separate numbers.
• Correction. For $w>0$ and $p<\bar v$, Lemma 11's positive equilibrium exists exactly when $\beta>1$ or $p+2h/(wNE[1/a])<\bar v$. At $\beta=1$, the delay stays bounded away from zero as utilization vanishes; the paper omits that condition.

A complete development needs real analysis on implicitly defined functions (implicit-function theorem in one variable, envelope arguments, monotone limits) and an argmax framework for the two-variable profit; these are reusable for other platform-pricing papers. Proofs of any milestone are welcome, as are alternative routes to the threshold statements.

Selected references

• S. Benjaafar, J.-Y. Ding, G. Kong, T. Taylor, Labor Welfare in On-Demand Service Platforms, Manufacturing & Service Operations Management, 2022 (online 2021). SSRN manuscript with online appendix: https://ssrn.com/abstract=3103447; https://doi.org/10.1287/msom.2020.0964
• J. Bai, K. C. So, C. S. Tang, X. Chen, H. Wang, Coordinating supply and demand on an on-demand service platform with impatient customers, Manufacturing & Service Operations Management 21(3), 2019. https://doi.org/10.1287/msom.2018.0707
• T. A. Taylor, On-demand service platforms, Manufacturing & Service Operations Management 20(4), 2018. https://doi.org/10.1287/msom.2017.0678