All missions

Why transparency of a hiring algorithm is an economic question

Firms increasingly screen job applicants, borrowers and customers with algorithms built on observable features. Regulators and the public ask for these algorithms to be made transparent, and firms often resist, arguing that agents who know the algorithm will game it. Wang, Huang, Jasin and Singh (arXiv:2008.09283, 2020; published in Management Science, 2023) model this tension as a game between a firm and strategic agents. They separate causal features, which change an agent's productivity (education), from correlational features, which only predict it. Their first headline result, Theorem 1, says exactly when a profit-maximizing firm is better off disclosing its algorithm. The answer depends on the agents' education costs, region by region in the cost plane.

The model builds on the signaling literature, in which education is both a signal and a source of productivity (Spence, 1973; Weiss, 1983), and on strategic classification, where agents manipulate the features a classifier uses (Hardt et al., 2016).

Setting

A unit mass of agents contains a share $\theta\in(0,1)$ of high-talent agents (type H) and $1-\theta$ of low-talent agents (type L). A share $\lambda\in[\tfrac12,1]$ of H agents and a share $1-\lambda$ of L agents are high on a correlational feature. Every agent may acquire education at cost $C_H$ (type H) or $C_L$ (type L), with $0<C_H<C_L$. An agent's productivity is $W=\alpha\,\mathbf 1(T=H)+\beta\,\mathbf 1(\text{educated})$, and the firm pays every hired agent the wage $R$. The standing assumptions are $0<\beta<R<\alpha$ (Assumption 1) and two-sided bounds on $\alpha$ and $\beta$ (Assumptions 2 and 3) that exclude trivial equilibria.

In the opaque game the agents do not know the correlational feature. They choose education, ending in one of four states $A,B,C,D$ (education 0/1 times feature 1/0), and the firm hires state $S$ with probability $P_S$. In the transparent game every agent raises the disclosed feature, so only education matters (states $E$, $F$). Each type plays a common mixed strategy: it improves with probability $q_H$ or $q_L$. The firm's payoff is $\Pi=\sum_S P_S\,m_S$, where the margin $m_S=n^H_S(W^H_S-R)+n^L_S(W^L_S-R)$ is computed from the masses $n^T_S$ in state $S$. A Nash equilibrium requires each type to best-respond, and the firm to hire an occupied state surely when $m_S>0$ and never when $m_S<0$. In the opaque game the agents move first and coordinate on the payoff-dominant equilibrium (IsOpaqueOutcome), the one that is best for both types at once.

Formalization targets

Goal: Theorem 1, corrected

Let $\Pi_O$ be the firm's payoff at any selected opaque outcome and $\Pi_T$ its payoff at any transparent equilibrium. On seven open regions of the $(C_H,C_L)$ plane (InRegion):

$$\Pi_T\le\Pi_O \text{ on } N_1,N_2,N_3',C_3';\qquad \Pi_O<\Pi_T\iff\beta>\beta_1 \text{ on } C_1;\qquad \Pi_O<\Pi_T\iff\beta>\beta_2 \text{ on } C_2';\qquad \Pi_O<\Pi_T \text{ on } C_4,$$

with $\beta_1$, $\beta_2$ the explicit thresholds (13)–(14). The statement also asserts that the compared equilibria exist, so no clause holds vacuously.

Milestones

The milestones follow the paper's argument: the firm's thresholds (12); the opaque cases that cannot be equilibria; Lemma 1, the selected opaque outcome per region; the transparent cases that cannot be equilibria; Lemma 2, the transparent equilibrium; and the five payoff comparisons (N1–N3, (13), (14), (15), C4).

Significance

Theorem 1 overturns the common view that transparency always hurts the firm. Disclosure destroys the predictive value of the correlational feature, but it also intensifies competition on education. Where this makes the types separate ($C_4$), or where education is productive enough ($C_1$, $C_2'$), the firm gains. The thresholds $\beta_1,\beta_2$ are explicit, so the result gives testable conditions for the regulatory debate.

The printed theorem is false on part of its region map. The paper rules out equilibria in which both types mix ("case 9", p.18). At $\theta=\tfrac12$, $\lambda=\tfrac45$, $R=1$, $\alpha=\tfrac32$, $\beta=\tfrac{13}{20}$ and $(C_H,C_L)=(\tfrac1{10},\tfrac3{20})$, a point of the printed region $N_3$, a both-types-mixing equilibrium exists and dominates for both types. Its firm payoff is $\tfrac{161}{440}$, below the transparent payoff $\tfrac25$. The printed case-4 region of Lemma 1 also reverses an inequality. The mission states the corrected theorem: the boundary between $N_3/C_3$ and $C_2$ moves to the ray $\lambda C_H=(1-\lambda)C_L$, and the $C_2$ clause, with the same threshold $\beta_2$, holds on the enlarged region $C_2'$. No machine-checked proof of any part of the paper exists. A formal proof settles the corrected region map, which so far rests on exact-rational sampling.

Difficulty

The algebra is elementary; the difficulty is completeness. The paper's argument checks a list of nine strategy patterns, each with a guessed hiring vector. A proof of Theorem 1 must instead classify all equilibria: every sign pattern of the four margins, every tie, and every degenerate line inside a region, where continua of equilibria appear. It must then show that the payoff-dominant one exists and has the stated payoff. The obvious shortcut is to argue that L agents cannot need a higher hiring chance than H agents. It fails because the two types sit at different values of the correlational feature: both types are indifferent in a mixed equilibrium whenever $\lambda C_H>(1-\lambda)C_L$. The remaining steps are sign arguments for rational functions of $(\theta,\lambda,R,\alpha,\beta)$ under Assumptions 1–3. The hardest is the positivity of the denominator of the case-9 payoff $\Pi_{O9}$, whose minimum approaches zero as $\lambda\to\tfrac12$.

Formalization scope

All quantities are real numbers. Strategies are a common mixed strategy $q_T\in[0,1]$ per type, with expected masses. Firm optimality is stated through the signed margins, never through the ratios $\gamma^E_S=n^H_S/n_S$, which are $0/0$ at an unoccupied state. At an unoccupied state the firm hires an educated state with probability 1 and an uneducated state with probability 0. This off-path convention is used by every equilibrium in the paper's appendix, and without it the payoff-dominance selection has no solution in region $N_2$. Selection compares against every opaque equilibrium, not against the paper's list of cases. Regions are open sets read off Figure 4; boundaries are not claimed. $\lambda=1$ is kept: there the opaque game has no equilibrium on $C_2'$, so that clause is vacuous and existence is not claimed there.

The definitions are self-contained: parameters and assumptions (Params, Standing), the two games (masses, margins, payoffs, utilities), the two equilibrium predicates, the selection, the regions and the thresholds. Contributions are welcome on each milestone. The equilibrium classifications (Lemmas 1 and 2) are the core; the five payoff comparisons are independent ordered-field exercises.

Selected references

• Q. Wang, Y. Huang, S. Jasin, P. V. Singh, Algorithmic Transparency with Strategic Users, arXiv:2008.09283v1, 2020; published in Management Science, 2023. https://arxiv.org/abs/2008.09283
• M. Spence, Job Market Signaling, Quarterly Journal of Economics 87(3), 355–374, 1973. https://doi.org/10.2307/1882010
• A. Weiss, A Sorting-cum-Learning Model of Education, Journal of Political Economy 91(3), 420–442, 1983. https://doi.org/10.1086/261147
• M. Hardt, N. Megiddo, C. Papadimitriou, M. Wootters, Strategic Classification, ITCS 2016. https://doi.org/10.1145/2840728.2840730

Why a platform's investment depends on what its sellers can do

Marketplace platforms often sell their sellers a service that those sellers could otherwise buy or build. Order fulfillment is the standard example: Amazon, Walmart and Alibaba offer logistics and distribution services to third-party sellers, while other platforms have delayed or declined to offer them. Li, Pisano, Xu and Zhu (SSRN 3310484; published in Management Science, doi:10.1287/mnsc.2022.4522) ask how sellers' ability to supply such a service themselves changes the platform's decision to offer it, and the price it charges. Their finding (p.3) is that, in general, the scalability of sellers makes the platform less likely to offer the service. This mission formalizes the benchmark case with one type of seller, Proposition 1, which p.20 calls the paper's main result.

The model

A monopoly platform hosts a unit mass of identical sellers and charges a commission rate $\alpha$ on revenue. A seller who sells $q$ units earns revenue $R(q)$, with derived demand $D=R'$. Each sale needs an ancillary service. It costs $\bar c$ per unit from the market. A seller can instead invest $F-f$ and supply it at unit cost $\underline c<\bar c$; the scalable scenario is the one with this option, and the non-scalable scenario the one without it. The platform can pay a fixed $I$ to offer the service at unit cost $c\in(\underline c,\bar c)$ and price $p$.

The game has three stages: the platform decides whether to offer the service and at what price; sellers choose whether to enter and which service to use; sellers choose output. A seller using a service with marginal cost $\tilde c$ and fixed fee $\tilde F$ maximizes $(1-\alpha)R(x)-\tilde c x-\tilde F$, and its output $q(\tilde c)$ solves $(1-\alpha)D(q(\tilde c))=\tilde c$. Write $q_m=q(\bar c)$, $q_o=q(\underline c)$, $\pi_m=\alpha R(q_m)$ and $\pi_o=\alpha R(q_o)$. If sellers use the platform service at price $p$, the platform earns

$$\pi(p)=\alpha R(q(p))+(p-c)q(p).$$

In the non-scalable scenario sellers use it when $p\le\bar c$, which gives the profit function $\pi_N$. In the scalable scenario they use it when its payoff beats own service, which gives $\pi_S$. The investment levels at which the platform is indifferent are

$$I_N=\max_p\pi_N(p)-\pi_m,\qquad I_S=\max_p\pi_S(p)-\pi_o.$$

Formalization targets

The goal: Proposition 1

For every model,

$$I_S\le I_N,$$

and, at an optimum $p_S$ of $\pi_S$ where sellers use the service and an optimum $p_N$ of $\pi_N$,

$$p_S\le p_N,\qquad q(p_N)\le q(p_S),\qquad \pi(p_S)\le\pi(p_N).$$

The goal also asserts that the maxima are attained, that the optimal prices are unique, and that sellers use the service at the scalable optimum whenever $I_S>0$.

The milestones

The milestones follow the paper's proof: the sellers' stage (the first-order condition, the service choice, the cutoff price $p_s$ and eq. (6)), the jump in $\pi_N$ at $\bar c$, the calculus of $q$ and $\pi$ ending in the quasi-concavity of $\pi$, and the rewriting of $I_N$, $I_S$ with the two comparisons behind (a) and (b).

Significance

The result separates two channels. Without the service, a platform whose sellers can scale already earns more, since $\pi_o\ge\pi_m$. With the service, it must undercut a better outside option, so its price range shrinks from $(0,\bar c]$ to $(0,p_s]$. Both channels lower the gain from offering the service. Managerially, a platform should expect less from such an investment when its sellers are able to scale. The paper builds on this benchmark for its results with two seller types and with timing.

The result is proved on paper, and this mission does not change its conclusion. No machine-checked proof of it is known. Formalizing it adds a small platform model in which sellers' behaviour is derived from primitives, a repaired set of hypotheses, and explicit attention to attainment and uniqueness of optimal prices, which the paper leaves implicit.

Difficulty

The conclusion (a) is short once its inputs are available: it compares suprema over nested price sets and uses $\pi_o\ge\pi_m$. The work is in those inputs. The output $q$ is defined only implicitly, so its derivative needs an inverse-function argument, and the second derivative of $\pi$ needs $D''$ along that inverse. The source does not claim that $\pi$ is concave: the structure it uses is quasi-concavity, extracted from the sign of the derivative of $\pi'/q'$. The maxima run over half-open intervals, so attainment needs the behaviour of $\pi$ near price $0$. The cutoff $p_s$ has to be constructed by an intermediate-value argument from Assumption 1 and $f<F$.

Formalization scope

Data and conditions are separated: Params holds the data, and Model extends it with the conditions. All statements use the namespace MarketplaceScalability.

The paper's demand conditions on p.4, $D>0$, $D'<0$, $D''\le0$ and $D(0)=\infty$, are unsatisfiable, so the printed result would be vacuous. A positive concave function on $(0,\infty)$ cannot be strictly decreasing, and a concave function on $(0,b)$ cannot tend to $+\infty$ at $0$. Model keeps the signs on an interval $J=(0,\bar q)$ and replaces $D(0)=\infty$ by its only use: the first-order condition is solvable on $J$ for every price in $(0,\bar c]$. Linear demand on $(0,a/b)$ is an instance. Other conventions: $0\le\alpha<1$; prices are positive; $q$ is Function.invFunOn, and comparisons at a platform price test $p\le\bar c$ first; $I_N$ and $I_S$ use sSup, with attainment proved in the goal; indifferent sellers use the platform service; (b) is weak, since strict inequalities are false.

The cutoff $p_s$ appears in no definition: $\pi_S$ comes from the sellers' payoff comparison, and $\pi_o$, $\pi_m$ are computed from the primitives. A version with $p_s$ as a free number below $\bar c$ and $\pi_o\ge\pi_m$ assumed would make (a) a one-line comparison of suprema, and is ruled out.

Everything needed is one-variable calculus already in Mathlib. Proofs of the milestones are welcome in any order. The inverse-function lemma for $q$ is the natural starting point, since most later steps use it.

Selected references

• J. Li, G. Pisano, R. Xu, F. Zhu, Marketplace Scalability and Strategic Use of Platform Investment, SSRN working paper 3310484, 2022. https://ssrn.com/abstract=3310484
• The same paper in Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4522

Motivation

Learning curves are a standard fact of manufacturing: unit cost falls with cumulative output, so a buyer who orders more today buys cheaper tomorrow (Yelle 1979). Procurement contracts with an outside supplier then face a second problem: the supplier knows its own cost and learning ability better than the buyer does, and it also observes privately how learning went. Gao, Nikoofal and Zhang (MSOM 2023) characterize the buyer's optimal long-term contract when cost and learning rate are private ex ante and the learning outcome is private ex post. Their rent formula has a third term, driven by post-contract information, which is absent from the analysis of Baron and Besanko (1984), where, as the paper reads it, the rent depends on pre-contract information only.

Setting

One buyer procures from one supplier over two periods with discount factor $\delta\in(0,1)$. In period $t$ the buyer sells at price $a_t-q_t$. The supplier has a private type $\theta\in\{\ell,h\}$, with $\mathbb P\{\theta=\ell\}=\nu$, unit cost $c^\theta$ ($c^\ell<c^h$) and learning rate $r^\theta>0$. After producing $q_1$ it privately observes a learning outcome $\Lambda\sim\mathrm{Bernoulli}(\rho)$, and its period-2 unit cost is $L(\theta,\Lambda;q_1)=c^\theta-r^\theta q_1\Lambda$. Write $\Delta c_1=c^h-c^\ell$, $\Delta r=r^\ell-r^h$, $\kappa=\nu/(1-\nu)$.

The buyer commits to a contract $\phi$: payments and quantities $(p_1^\theta,q_1^\theta)$ and $(p_2^{\theta\Lambda},q_2^{\theta\Lambda})$ for each reported type and outcome. A supplier of type $\theta$ who picks the term of $\tilde\theta$ earns

$$\tilde U(\theta;\tilde\theta)=p_1^{\tilde\theta}-c^\theta q_1^{\tilde\theta}+\delta\,\mathbb E_\Lambda\Big[\max_{\tilde\Lambda}\big\{p_2^{\tilde\theta\tilde\Lambda}-(c^\theta-\Lambda r^\theta q_1^{\tilde\theta})q_2^{\tilde\theta\tilde\Lambda}\big\}\Big],$$

and $U(\theta)=\tilde U(\theta;\theta)$. The feasible set $\Phi$ requires nonnegative quantities, Condition (C) $q_1\le Q$, where $Q=\Delta c_1/(r^h-r^\ell)$ if $r^\ell<r^h$ and $Q=\infty$ otherwise, individual rationality $U(\theta)\ge0$, and incentive compatibility in both the type and the outcome. The buyer maximizes her expected payoff $\tilde V$ on $\Phi$. This is regime $\mathcal P^{\mathrm{AL}}$.

Formalization targets

Goal: Proposition 1, corrected

Let $(q^\ell,y^\ell,z^\ell)$ be type $\ell$'s first best, and let $(q,y,z)$ be the quantities of type $h$: $(y,z)=(\bar y(q),\bar z(q))$ when these separate, $y=z=\hat y(q)$ otherwise, with $q$ fixed by the first-order condition. Under second-order and interiority hypotheses, the contract $\phi^*$ with deferred payments is optimal, $U(h)=0$, and

$$U(\ell)=U^\ell=\begin{cases}\Delta c_1q+\delta\Delta c_1[\rho y+(1-\rho)z]+\delta\rho qy\,\Delta r,&c^h-r^hq\le c^\ell,\\ \Delta c_1q+\delta\Delta c_1y+\delta\rho qy\,\Delta r-\delta(1-\rho)r^hq(y-z),&c^h-r^hq>c^\ell,\end{cases}$$

with $U^\ell>0$. Every optimal contract has the quantities of $\phi^*$ and these rents. The printed payment to type $\ell$ is optimal exactly when it is feasible, and that is characterized by a rent inequality.

Milestones

Lemma 1(b), Claims 1–5, the deferred payment (19)–(20), the lowest rent, the two cases of Step 2, the concavity of the reduced function $F$ and the position of the optimum, and one lemma not in the paper, on the incentive compatibility of $\phi^*$.

Significance

The result gives the optimal transfers and output for a dynamic screening problem with two layers of private information. It shows a rent term that can have either sign, a transfer deferred to the second period, and two regimes according to whether a learned type $h$ can undercut an unlearned type $\ell$. Output of type $h$ can be distorted upward. The paper's later comparisons of regimes rest on this characterization.

The proposition is proved on paper only, and the printed statement needs correction. The proof never checks the incentive constraint of type $h$, and the printed payment to type $\ell$ can violate it: at $a_1=a_2=100$, $c^\ell=10$, $c^h=11$, $r^\ell=r^h=1$, $\delta=\rho=\nu=1/2$ one gets $\tilde U(h;\ell)=49/10>0=U(h)$. The quantities, rents and value survive. Replacing $q_2^{\ell0}$ by $q_2^{\ell1}$ in the two learning terms of type $\ell$'s payment restores feasibility. The mission therefore gives a corrected, machine-checkable form of a published result, with each departure from the page declared in its item, together with a counterexample.

Difficulty

The obvious route is to bind the incentive constraint of type $\ell$ and the participation constraint of type $h$, solve the relaxed problem, and stop. That route leaves a gap: nothing in the relaxed problem controls type $h$'s temptation to take type $\ell$'s term, which has to be derived from the optimality of the candidate quantities. The paper's Claim 4 (that a particular second-period constraint must bind) is false as printed, because a band of transfers gives the same rent.

The reduced objective is piecewise quadratic with up to three pieces, pooled, double-deviation separating and single-deviation separating. It has a concave kink at $q=\Delta c_1/r^h$ on which the optimum can sit for an open set of parameters. Concavity of each piece has to be read off Condition (A3), and the pooled piece needs its own bound.

Formalization scope

All objects are finite real arithmetic: Params with Params.Standing, Term and Contract, the payoffs, and Params.Feasible. The expectations $\mathbb E_\Lambda,\mathbb E_\theta$ are two-term weighted sums, and $\Lambda$ is a Bool. Optimality is Params.IsOptimal, membership in $\Phi$ plus a universal bound, because without second-order conditions the supremum can be $+\infty$. Quantities are nonnegative and (C) is written $(r^h-r^\ell)q_1\le\Delta c_1$. The second-order conditions are Params.SecondOrder: $\delta\rho(r^\ell)^2<4$, plus (A3) if $r^h>\nu r^\ell$ and $\delta\rho^2B^2<4$ otherwise. Params.FirstBestAdmissible and Params.Candidate hold the interiority and first-order conditions, with one-sided inequalities at the kink, so the goal does not cover corner optima. Under double deviation the separating quantities are those of App. p.7, not note 9. The slopes slopeRight, slopeGap and marginalRent are explicit formulas, not deriv, because the paper's partial derivatives hold second-period quantities fixed.

Trivializing encodings are ruled out: $\Phi$ keeps every constraint, including (IC$^h$), and is not defined by the binding constraints or by the deferred payment. The non-vacuity of the hypotheses is checked in all four regimes (pooled, double, kink, single) on the paper's Table 5 base case. The reduced function $F$ is defined by an explicit formula, and two milestones show it is the maximum.

Proofs of any milestone are welcome. A reusable byproduct is a treatment of two-type screening with a second round of private information, which no platform definition currently covers. The general objects here are specific to this model, so no platform definition was reused.

Selected references

• L. Gao, M. E. Nikoofal, W. Zhang, The Strategic Role of Supplier Learning, Manufacturing & Service Operations Management, 2023. https://doi.org/10.1287/msom.2021.0285
• D. P. Baron, D. Besanko, Regulation, asymmetric information, and auditing, The RAND Journal of Economics 15(4):447–470, 1984. https://doi.org/10.2307/2555518
• L. E. Yelle, The learning curve: historical review and comprehensive survey, Decision Sciences 10(2), 1979. https://doi.org/10.1111/j.1540-5915.1979.tb00026.x
• A. Pavan, I. Segal, J. Toikka, Dynamic mechanism design: a Myersonian approach, Econometrica 82(2), 2014. https://doi.org/10.3982/ECTA10269

Why manufacturers might keep demand information from a retailer

In many consumer-goods channels the party with the best demand information is the manufacturer, which controls promotion, product launches and brand planning, while the retailer places the order. Whether manufacturers should tell retailers what they know is a question of practice as well as theory, and the answer depends on how the manufacturers compete. This mission formalizes the main threshold result of Aditya Jain's Sharing Demand Information with Retailer under Upstream Competition (SSRN:3388957; journal version doi:10.1287/mnsc.2021.4116).

The paper belongs to a literature on vertical information sharing. Li (1985) gave the signal framework with linear conditional expectations used here. Gal-Or et al. (2008) showed signaling-driven distortions in the wholesale price of a single manufacturer selling through two retailers, and Shang, Ha and Tong (2016) studied two manufacturers with a retailer holding the information. Jain's setting reverses the direction of that last model: manufacturers hold the signals and sell through a common retailer.

Setting

Two manufacturers sell substitutable products through one retailer. The inverse demand is

$$p_i=a+\theta-\frac{1+\phi}{1+2\phi}q_i-\frac{\phi}{1+2\phi}q_{3-i},\qquad i\in\{1,2\},$$

where $\phi\ge0$ is the substitution level, $a$ the mean demand level, and $\theta$ a zero-mean demand uncertainty with variance $\sigma>0$. Marginal costs are zero.

Each manufacturer $i$ holds a private signal $Y_i$ with $E[Y_i\mid\theta]=\theta$, finite and nonzero precision $t_i=1/E[\mathbb V(Y_i\mid\theta)]$, and linear conditional expectations. Its accuracy is $s_i=t_i/(\sigma^{-1}+t_i)$.

Before seeing its signal, each manufacturer decides whether to share it ($\delta_i=1$) or not ($\delta_i=0$). This yields four cases: $F$ (both share), $N$ (neither), and $P_i$ (only $i$ shares). After signals arrive, manufacturers simultaneously set wholesale prices $w_i$, and the retailer chooses orders $q_1,q_2$ before demand is realized. The retailer knows a shared signal, and infers an unshared one from the price through the conjectured rule $w_i=\alpha_i+B_iY_i$. A linear separating equilibrium is a profile in which $B_i\neq0$ for each non-sharing manufacturer, the retailer maximizes its expected profit at every price, and no manufacturer gains by deviating to any other pricing function of its signal. The expected profit is $\Pi_i=E[w_iq_i]$.

Formalization targets

Goal: Proposition 5, corrected

Take $s_1=s_2=s$. Let

$$g_1=\Pi_i^{P_i}-\Pi_i^N,\qquad g_2=\Pi_i^F-\Pi_i^{P_{3-i}},\qquad g_3=\Pi_i^F-\Pi_i^N,\qquad \hat s=\frac{\sqrt{193}-9}{14}.$$

With $P(s)=14s^4+36s^3+50s^2+48s+32$, define

$$H_1:\ a^2(4-s^2)^2(2-s)P(s)>4\sigma s^2(5s+4)^2\bigl(4-s^2(s+2)^2\bigr),$$ $$H_2:\ a^2(4-s^2)^3(7s^2+9s-4)>\sigma s(4-s^4-3s^3-4s^2)(5s+4)^2,$$ $$H_3:\ a^2(2-s)^3(1+s)^2>2\sigma s^2(1-2s-s^2).$$

Under $H_1$, the gap $g_1$ is positive below a threshold $\hat\phi_1$, zero at it and negative above it; if $H_1$ fails, $g_1>0$ for all $\phi\ge0$. The same holds for $g_3$ with $H_3$ and $\hat\phi_3$, and for $g_2$ with $s>\hat s$ and $H_2$ and $\hat\phi_2$; for $s\le\hat s$ the gap $g_2$ is always positive. Thresholds that exist satisfy $\hat\phi_3<\hat\phi_1<\hat\phi_2$.

Milestones

The relations implied by Assumption 1; Proposition 1, the equilibrium in each sharing case as an if and only if; its reduction under full information; Proposition 6(a), for $\phi>0$; and clauses (a), (b), (c) of Proposition 5 separately.

Significance

The theorem says when substitutability turns the sharing preference around, and it locates the turning point exactly in $(a^2/\sigma,s)$. At low substitution, sharing removes a wholesale-price distortion that hurts each manufacturer. At high substitution, that distortion softens price competition, and withholding becomes attractive. Proposition 5 is the basis of the paper's analysis of equilibrium sharing patterns with equal accuracies.

The formalization adds a corrected statement. The printed clauses (a), (b) and (c) fail at some parameters, so the exact conditions $H_1,H_2,H_3$ state what is true: at $a=\sigma=1$, $s=2/5>\hat s$ no threshold $\hat\phi_2$ exists, and at $a^2=1/1000$, $\sigma=1$, $s=1/5$ neither $\hat\phi_1$ nor $\hat\phi_3$ exists. Printed Assumption 1(b) is also replaced, as it contradicts the relations derived from it. On status: the paper's proofs are in an Electronic Companion. The exact conditions $H_1,H_2,H_3$ were derived from the limits of the gaps and tested by exact root counts on rational grids; they are not proved for all parameters. No part of the result is known to have a machine-checked proof.

Difficulty

The equilibrium is the first obstacle: a non-sharing manufacturer's deviation moves both the retailer's response and its inference, so the best-response problem must be solved against all pricing functions, on and off the path, and uniqueness requires the full system of coefficients, with no assumption on the sign of $B_i$.

The second obstacle is the sign analysis. A natural first idea is to compare only the $a^2$ part of the profits, which produces $\hat s$ from $7s^2+9s-4$. This fails, because the $\sigma$ part of each gap has the same order $1/\phi$ as $\phi\to\infty$. The gaps are rational functions in $\phi$ with numerators of degree up to 11, and the claim is uniform in $(\phi,s,a^2/\sigma)$, in both directions of each condition. Clause (d) compares roots of different such polynomials.

Formalization scope

The probability space is general, with $\theta,Y_1,Y_2\in L^2$. Manufacturers are indexed by Fin 2, and 1 - i stands for $3-i$. $\sigma$ is a variance. $E[\mathbb V(Y_i\mid\theta)]$ is encoded as $E[(Y_i-\theta)^2]$. Assumption 1(b) reads $E[(Y_1-\theta)(Y_2-\theta)\mid\theta]=0$. The relation $E[Y_i\mid Y_{3-i}]=E[\theta\mid Y_{3-i}]$ is a hypothesis. Quantities are unconstrained in sign, as in problem (2). Manufacturer optimality is ex ante, over all measurable pricing functions in $L^2$. Profits are integrals along strategies, not closed forms, and they are taken along any family of equilibria. This rules out a trivial formalization: a closed-form $\Pi_i$ would detach the goal from the game, and a copy of the printed (b) would be unsatisfiable. The signal model is inhabited at every $\sigma>0$ and $s\in(0,1)$ by a finite example.

A complete development needs the moment identities of the signal model, a uniqueness argument for the quadratic game, closed-form profits, and an exact sign analysis of polynomials. The signal-model lemmas are reusable. Contributions of any of these parts are welcome, and so are alternative proofs of the conditions $H_1,H_2,H_3$.

Selected references

• A. Jain, Sharing Demand Information with Retailer under Upstream Competition, Management Science (submitted version, PDF of 2021-04-25). SSRN:3388957; doi:10.1287/mnsc.2021.4116
• L. Li, Cournot oligopoly with information sharing, RAND Journal of Economics 16(4), 1985. doi:10.2307/2555510
• E. Gal-Or, T. Geylani, A. J. Dukes, Information sharing in a channel with partially informed retailers, Marketing Science 27(4), 2008. doi:10.1287/mksc.1070.0316
• W. Shang, A. Y. Ha, S. Tong, Information sharing in a supply chain with a common retailer, Management Science 62(1), 2016. doi:10.1287/mnsc.2014.2127

Why acreage decisions under downward substitution matter

Specialty coffee roasters buy single-origin beans through direct trade: they contract acreage with a grower before harvest and take the crop that passes the quality specification. A single-origin label (SL) sells at a premium to a small connoisseur segment, while a blend label (BL) has a much larger market. Beans bought for SL can always be sold as BL, a flexibility called downward substitution. The contract is signed before two things are known: the harvest yield and the BL price.

Webster, Kazaz and Gheibi (2024) model this as a two-stage stochastic program with recourse and identify three optimal sourcing strategies: specialized (no downward substitution), diversified (consistent downward substitution) and mixed. The problem joins random-yield planning, surveyed in Yano and Lee (1995), with revenue management under the multinomial logit (MNL) choice model.

Setting

Fix a price sensitivity $b>0$, nominal qualities $v, v_B$ and a post-harvest cost $c$ per normalized pound. The pre-harvest cost $k(Q)$ of $Q\ge0$ normalized acres is continuous, nondecreasing and convex on $[0,\infty)$, and need not be differentiable. The pair $(\tilde\varphi,\tilde y)$ of blend price and yield has a joint law $F$ with support $\Omega=[\varphi_l,\varphi_h]\times[y_l,y_h]$, where $\varphi_l,y_l>0$ and $E[\tilde y]=1$.

Once $(\varphi,y)$ is realized, the harvest is $Qy$. Selling $q$ as SL clears the market at the MNL price

$$p(q)=\frac1b\left(v-\ln\frac{q\,(1+e^{v_B-b\varphi})}{1-q}\right),$$

and the rest sells as BL at $\varphi$, with profit $\pi(q)=(p(q)-c)q+(\varphi-c)(Qy-q)-k(Q)$. The second-stage value $\pi^*(Q,\varphi,y)$ is the maximum of $\pi$ over $0\le q\le1$, $q\le Qy$. The first-stage problem maximizes $\Pi(Q)=E[\pi^*(Q,\tilde\varphi,\tilde y)]$ over $Q\ge0$.

Let $W$ be the Lambert W function and $x(\varphi)=e^{v-1}/(e^{b\varphi}+e^{v_B})$. The unconstrained second-stage quantity is $q^\circ(\varphi)=W(x(\varphi))(1+W(x(\varphi)))^{-1}$, and the benchmarks are

$$Q_L=\frac{q^\circ(\varphi_h)}{y_h},\qquad Q_D=q^\circ(\mu_\varphi),\qquad Q_H=\frac{q^\circ(\varphi_l)}{y_l}.$$

An acreage is specialized if $Q\le Q_L$, diversified if $Q\ge Q_H$ and mixed if $Q_L<Q<Q_H$. With the markups $m_c(Q,\varphi,y)=\frac yb\ln[\frac{e^v}{e^{b\varphi}+e^{v_B}}\cdot\frac{1-Qy}{Qy}]$ and $m_u(Q,y)=\frac yb\cdot\frac1{1-Qy}$, put $\bar m_c=E[m_c]$, $\bar m_u=E[m_u]$, and define the expected shadow price $\lambda(Q)=E[(m_c-m_u)^+]$.

Formalization targets

Goal: Proposition 3

$$\exists\ \text{optimal } Q^*\le Q_L \iff \mu_\varphi+\rho\sigma_\varphi\sigma_y+\bar m_c(Q_L)-\bar m_u(Q_L)\le k'_+(Q_L)+c, \tag{11}$$ $$\exists\ \text{optimal } Q^*\ge Q_H \iff \mu_\varphi+\rho\sigma_\varphi\sigma_y\ge k'_-(Q_H)+c, \tag{12}$$

the second when an optimal acreage exists; some optimal acreage is mixed exactly when neither (11) nor (12) holds; and under uncertainty any two optimal acreages lie in the same class.

Milestones

1. Proposition 1: the unique second-stage solution $q^*=\min\{q^\circ(\varphi),Qy\}$, its price and its value.
2. Lemma 1: $\Pr(q^*<Q\tilde y)=0$ iff $Q\le Q_L$, and the matching condition at $Q_H$.
3. Lemma 2: $Q_L<Q_D<Q_H$ under uncertainty.
4. Proposition A1: concavity of $\Pi$, strict on $[0,Q_H]$.
5. The marginal expected profit from the proof of Proposition 2: $(\Pi+k)'(Q)=\mu_\varphi+\rho\sigma_\varphi\sigma_y+\lambda(Q)-c$ for $Q>0$.
6. The shadow price at the benchmarks: $\lambda(Q)=0$ iff $Q\ge Q_H$, and $\lambda=\bar m_c-\bar m_u$ iff $Q\le Q_L$.

Significance

The result gives an exact test, in terms of marginal revenue and marginal cost at two explicit acreages, for which strategy a roaster should adopt, for every joint law of price and yield and every convex cost, including the piecewise linear costs the paper calls typical. It is the basis of the paper's later comparative statics.

The theorems are proved in the paper, and to our knowledge none has a machine-checked proof. Formalizing them adds a capacity-constrained MNL pricing problem, a two-stage program with recourse and random yield, and one-sided optimality conditions for a concave objective with a kinked cost. Three printed statements need corrections, each with a counterexample satisfying all of the paper's assumptions:

• in (12), $k'(Q_H)$ must be the left derivative, because the paper's right-derivative convention fails when $k$ kinks at $Q_H$;
• Proposition A1's strict concavity on $[0,\infty)$ fails for affine $k$ beyond $Q_H$, so strictness is stated on $[0,Q_H]$;
• Lemma 1's "$=1$ iff $Q\ge Q_H$" fails with an atom at $(\varphi_l,y_l)$.

The phrase "is optimal" is read existentially, and a clause is added that all optimal acreages share one class under uncertainty.

Difficulty

The first-order condition at a benchmark does not follow from a pointwise derivative. The second-stage value has a different formula on the constrained and unconstrained realizations, and the boundary between them moves with $Q$. Differentiating under the integral therefore requires seeing that the two pieces meet with equal derivative on $Qy=q^\circ(\varphi)$. The naive argument "Proposition 2 gives the optimum" also fails, because $k$ may have kinks, so that the set in Proposition 2 need not have a maximum: the conditions must be one-sided and rest on concavity. Strictness on $[0,Q_H]$ needs mass near the corner $(\varphi_l,y_l)$, which is the role of the support hypothesis.

Formalization scope

The joint law is a probability measure on $\mathbb R\times\mathbb R$. Support $\Omega$ is encoded as $F(\Omega^c)=0$ with positive mass of every ball around a point of $\Omega$; no density, independence or atomlessness is assumed, and the rectangle may degenerate to a point. The feasible set uses $q<1$, since no finite price clears the market at $q=1$. $k'_\pm$ are derivWithin on Ioi and Iio. $\rho\sigma_\varphi\sigma_y$ is the covariance, since $\rho$ is undefined for zero variance. $\lambda$'s integrand is explicitly $0$ where $Qy\ge1$. The order of $v$ and $v_B$ is not assumed.

$\pi^*$ and $\Pi$ are defined as optimal values. Defining them by Proposition 1's formula would trivialize the mission and is ruled out. The strategy classes are thresholds on $Q$, not Lemma 1's probabilities.

A complete development needs elementary facts on $W$, the analysis of the concave second-stage objective, and differentiation under the integral on the compact support. The Lambert W definition is reusable beyond this mission. Contributions of any milestone or of auxiliary lemmas are welcome.

Selected references

• S. Webster, B. Kazaz, S. Gheibi, Direct Trade Sourcing Strategies for Specialty Coffee, Manufacturing & Service Operations Management, 2024. https://doi.org/10.1287/msom.2021.0586
• C. A. Yano, H. L. Lee, Lot sizing with random yields: a review, Operations Research 43(2):311–334, 1995. https://doi.org/10.1287/opre.43.2.311
• R. M. Corless, G. H. Gonnet, D. E. G. Hare, D. J. Jeffrey, D. E. Knuth, On the Lambert W function, Advances in Computational Mathematics 5:329–359, 1996. https://doi.org/10.1007/BF02124750

Motivation

A bank funds its assets with two kinds of debt that a nonbank firm does not mix in the same way: insured deposits, which earn the bank a service profit but cost a risk-based insurance premium, and nondeposit debt (bonds), which carries a credit spread. Regulators close a bank whose total capital falls below a fixed fraction of its assets, and the deposit insurer charges a premium that grows with the deposits it protects. How a value-maximizing bank should split its funding between the two, given these rules, is a question about bank regulation as much as about corporate finance: the split determines how much capital stands between the bank's assets and the insurer's loss.

Sundaresan and Wang (Management Science, 2023) extend the structural capital-structure model of Leland (1994) to banks with deposit profitability, risk-based deposit insurance and a total capital requirement, and solve the bank's liability choice in closed form. Their Proposition 2 is the paper's main result: the value-maximizing bank uses nondeposit debt to place its own default boundary exactly at the regulator's closure boundary. With no deposit profit and no insurance subsidy the formula reduces to Leland's optimal leverage for a nonbank firm.

Setting

The parameters (Table 1 of the paper) are the asset volatility $\sigma>0$, the asset cash-flow rate $\delta\ge0$, the risk-free rate $r>0$, the deposit profitability $\eta\in(0,r)$, the debt advantage (tax rate) $\tau\in(0,1)$, the liquidation cost $\alpha\in(0,1)$, the capital requirement $\beta\in[0,\alpha)$ and the insurance subsidy $\omega\in[0,1]$. The exponent $\lambda$ (lam) is the positive root of $\sigma^2\lambda(1+\lambda)/2-(r-\delta)\lambda-r=0$; the state price of the asset value falling from $V$ to a boundary $L\le V$ is $(L/V)^\lambda$.

For an asset value $V>0$, a liability structure is a pair $(D,C_B)$: deposits $D\ge0$ and a nondeposit coupon $C_B\ge0$. It determines:

• the regulatory total capital boundary $V_b=D/(1-\beta)$, at which the regulator closes the bank;
• the fair assessment rate of deposit insurance, equation (2), $g^\circ=\frac{r[\alpha-\beta]^+}{1-\beta}\,\frac{x^\lambda}{1-x^\lambda}$ with $x=V_b/V$; the charged rate $g=(1-\omega)g^\circ$, the premium $I=gD$ and the net deposit cost $C_D=(r-\eta)D$;
• the endogenous default boundary $V_d=(1-\tau)\frac{\lambda}{1+\lambda}\frac{I+C_D+C_B}{r}$, equation (3), at which equity holders default, and the liquidation boundary $V_l=\max\{V_b,V_d\}$;
• with $p=(V_l/V)^\lambda$, the nondeposit debt value $B=\frac{C_B}{r}(1-p)+[(1-\alpha)V_l-D]^+p$, the equity value $E=V-(1-\tau)\frac{I+C_D+C_B}{r}(1-p)-V_lp$, and the total bank value $F=D+B+E$;
• the credit spread $s$, defined by $C_B=(r+s)B$.

A structure is feasible if $0\le D<(1-\beta)V$, $C_B\ge0$ and $V_d\le V$, and strategic (IsStrategic) if it is feasible and maximizes $F$ over all feasible structures.

Formalization targets

Goal: Proposition 2

Assume the regularity assumption (4), read as $g^*<\eta/(1+\lambda)$ with $g^*$ below. Let

$$\pi=\frac{1}{1+\lambda}\cdot\frac{\eta(1-\tau)\lambda(1-\beta)+r\tau(1+\lambda)}{\eta(1-\tau)\lambda(1-\beta)+r\tau(1+\lambda)+r(1-\tau)\lambda[(1-\omega)\alpha+\omega\beta]}. \tag{5}$$

Then for every $V>0$ there is exactly one strategic structure, and at it $(V_b/V)^\lambda=\pi$,

$$\frac{V_b}{V}=\frac{V_d}{V}=\pi^{1/\lambda},\qquad \frac DV=(1-\beta)\pi^{1/\lambda},\qquad \frac BV=\Big(\frac{\tau}{1-\tau}+\beta+(1-\beta)\frac\eta r\frac{\lambda}{1+\lambda}+\frac{1-\pi}{\lambda}\Big)\pi^{1/\lambda},$$ $$s=\frac{r\pi}{1-\pi},\qquad g=g^*=(1-\omega)\frac{\alpha-\beta}{1-\beta}\cdot\frac{r\pi}{1-\pi}.$$

Milestones

1. $\lambda$ (§2.2, p.5): $\lambda>0$ is the only positive root of its quadratic, and $\lambda=2r/\sigma^2$ when $\delta=0$.
2. Equation (2) (p.5): $g^\circ$ makes the insurance contract worth zero, is the only such rate when $D>0$, and is strictly increasing in $D$.
3. Equation (3) (p.6): $V_d$ is the strict maximizer of the equity value over default boundaries in $(0,V]$, equity is zero at $V=V_d$, and $V_d$ increases in each of $I$, $C_D$, $C_B$.
4. Proposition 1 (p.6): a feasible structure with $V_d<V_b$ is improved by a larger coupon, which raises both the nondeposit debt value and $F$; hence every strategic structure has $V_b\le V_d$.

Significance

The proposition gives the bank's leverage, the split between deposits and bonds, the credit spread and the insurance assessment rate as explicit functions of eight parameters. Its qualitative content is that at the optimum the bank's capital is exactly the regulatory minimum at the moment its shareholders choose to default, so the strategic structure leaves no extra capital to protect the deposit insurer. The paper's comparative statics in the capital requirement, the deposit profitability and the insurance subsidy (Propositions 5–7) and its comparison of banks with nonbank firms (Proposition 4) are read off these closed forms.

The paper's proofs are in an Online Appendix that is not part of the source artifact. The result is proved on paper but has no machine-checked proof; this mission asks for one, including the global optimality and uniqueness that the paper asserts as a "complete characterization". The model's closed forms were checked numerically before formalization: maximizing $F$ reproduces the paper's Table 2 and the closed forms (5)–(7) at random parameter vectors satisfying (4).

Difficulty

$F$ is not concave and not smooth: it has kinks where $V_d=V_b$ (the maximum in $V_l$) and where $(1-\alpha)V_l=D$ (the positive part in $B$), and the fair rate $g^\circ$ blows up as $D/V\to1-\beta$. A first-order condition in the region $V_d>V_b$ alone does not find the optimum, which sits on the kink $V_d=V_b$, and global optimality over the whole two-dimensional feasible set has to be argued separately. The regularity assumption (4) cannot be dropped: for $\sigma=0.4$, $\alpha=0.9$, $\beta=\omega=0$, $\tau=0.15$, $\delta=0.08$, $r=0.05$, $\eta=0.005$ the assumption fails and the maximizer of $F$ has a deposit ratio of about $0.041$, not the $0.049$ of (6).

Formalization scope

The model is stated at the closed-form state-price level: the state price is the explicit expression $(L/V)^\lambda$ (Real.rpow), not an expectation under a geometric Brownian motion. The total bank value is taken from the paper's displayed pricing equations (15)–(17) of §4.1 with no restructuring, which match the §2 description; the paper's own closed form of $F$ is in the Online Appendix. As in (2), $g^\circ$ is evaluated at $V_b$ even when $V_d>V_b$. Assumption (4), which the paper writes for the structure-dependent rate $g$, is read as the parameter condition $g^*<\eta/(1+\lambda)$; required at every feasible $D$ it would be unsatisfiable. The insurance subsidy ranges over Table 1's $[0,1]$ (the running text says $\omega<1$). The point $D=(1-\beta)V$ is excluded from the feasible set because (2) is undefined there. All ratios are stated for an arbitrary $V>0$, not normalized.

The strategic structure is defined as a maximizer of $F$, never by the closed forms (6); the goal asserts existence and uniqueness, so it cannot hold vacuously. The credit spread is $C_B/B-r$, and the goal does not assume $B>0$.

The definitions use Mathlib's real powers, square root and max only. Proofs of the milestones, and lemmas on the shape of $F$ in the regions $V_d<V_b$ and $V_d\ge V_b$, are welcome.

Selected references

• S. Sundaresan, Z. Wang, Strategic Bank Liability Structure Under Capital Requirements, Management Science (2023), Articles in Advance pp. 1–20. https://doi.org/10.1287/mnsc.2022.4570
• H. E. Leland, Corporate Debt Value, Bond Covenants, and Optimal Capital Structure, Journal of Finance 49(4), 1994. https://doi.org/10.1111/j.1540-6261.1994.tb04760.x
• R. C. Merton, On the Pricing of Corporate Debt: The Risk Structure of Interest Rates, Journal of Finance 29(2), 1974. https://doi.org/10.1111/j.1540-6261.1974.tb03058.x

Motivation

Since Naor's 1969 model of queue joining, the literature on pricing congestible services has assumed that a customer judges a time-consuming service by its full price: the money price $r$ plus a constant multiple $\eta$ of the time commitment $\delta$, $r+\eta\delta$. Revenue-maximizing and welfare-maximizing prices for queues, priority schemes and capacity choices (Afèche and Mendelson 2004; Allon and Federgruen 2007; Nazerzadeh and Randhawa 2018; Gurvich et al. 2019) are all derived under this assumption, usually with $\eta$ identified with a customer type such as a wage. Allon and Federgruen describe it as "tantamount to assuming that all consumers assign a specific cost value to their waiting time and that the cost of waiting is simply proportional to the total waiting time."

Li, Lariviere and Bassamboo ask when this assumption is actually implied by a consumer's own optimization. They embed the purchase decision in a Becker (1965) style allocation of time and money, and show that the full-price model is exact for consumers who choose freely how long to work at a constant wage (gig workers), while it fails for shift workers. The result gives the full-price model a microfoundation and identifies the waiting cost $\eta$ with the wage $\theta$.

Setting

A consumer has $T$ units of time per day. She chooses a plan $(t_l,c_l,t_w,c_O)$: leisure time $t_l$, leisure consumption $c_l$, work time $t_w$ and overhead expenditure $c_O$, and a purchase decision $y\in\{0,1\}$ for a discrete service with value $V$, price $r$ and time commitment $\delta$. Her problem (PC) is

$$\max\ U(t_l,c_l)+Vy\quad\text{s.t.}\quad t_w+O(c_O)+t_l+\delta y\le T,\quad c_O+c_l+ry\le \Pi_\theta(t_w),\quad t_l,c_l,t_w,c_O\ge 0 .$$

Here $U$ (StandingAssumptions) is continuous, non-decreasing and concave in each argument on the closed quadrant with $U(0,c_l),U(t_l,0)\ge0$; $O(c_O)$, the time spent on chores when $c_O$ is spent to reduce them, is decreasing and strictly convex; $\Pi_\theta$ is the compensation function. For gig workers it is linear, $\Pi_\theta(t_w)=\theta t_w$ (linearCompensation), with wage $\theta>0$.

A pair $(r,\delta)$ is feasible (IsFeasiblePair) when the buyer's problem ($y=1$) has a feasible plan (IsFeasiblePlan). The buyer's leisure utility $u^B(\theta,r,\delta)$ (buyerUtility) is the supremum of $U(t_l,c_l)$ over the buyer's feasible plans. The consumer is a full-price decision-maker (Definition 1, IsFullPriceDecisionMaker) if there is $\eta>0$ with $u^B(\theta,r,\delta)=u^B(\theta,\hat r,\hat\delta)$ whenever $(\hat r,\hat\delta)$ is feasible and $r+\eta\delta=\hat r+\eta\hat\delta$. An optimal plan (IsOptimalPlan) of the buyer ($j=B$, $y=1$) or the non-buyer ($j=NB$, $y=0$) maximizes $U(t_l,c_l)$ over the feasible plans of that problem. The marginal rate of substitution of time for money (mrs) is

$$\chi(t_l,c_l)=\frac{\partial U/\partial t_l}{\partial U/\partial c_l}.$$

Formalization targets

Goal: Proposition 1 (p.8)

For $\theta>0$ and $\Pi_\theta(t_w)=\theta t_w$:

1. the consumer is a full-price decision-maker;
2. with $\eta=\theta$: for all $r,\delta,\hat r,\hat\delta\ge0$ with $(\hat r,\hat\delta)$ feasible,

$$r+\theta\delta=\hat r+\theta\hat\delta\ \Longrightarrow\ u^B(\theta,r,\delta)=u^B(\theta,\hat r,\hat\delta);$$

3. at every optimal plan of the buyer (any $r,\delta\ge0$) and of the non-buyer with $t_l>0$, $c_l>0$, at which $U$ is differentiable with $\partial U/\partial c_l\ne0$,

$$\chi(t^j_l,c^j_l)=\theta,\qquad j\in\{NB,B\}.$$

Milestones: Lemma 4 (p.32)

Part 1 (buyer) and part 2 (non-buyer): at an optimal plan where $U$ is differentiable with $\partial U/\partial c_l\ne0$, both constraints bind; if moreover $t_l>0$ and $c_l>0$, then $\chi=\theta$ at the paper's point $(T-t^j_w-O(c^j_O)-\delta y,\ \theta t^j_w-c^j_O-ry)$; and $O'(c^j_O)=-1/\theta$ whenever $c^j_O>0$ and $O$ is differentiable there.

Significance

The proposition says that, for gig workers, the purchase decision depends on $(r,\delta)$ only through $r+\theta\delta$: the iso-utility curves in the $(r,\delta)$ plane are parallel lines of slope $\theta$. This is exactly the structure that the queueing-pricing literature assumes, with waiting cost per unit of time equal to the wage (Remark 1 of the paper recovers the standard model $v(\theta)-r-\theta\delta$ from it). The paper's later results (Lemma 2, Proposition 2, §4) show that shift workers are not full-price decision-makers and that pricing them as if they were loses revenue; Proposition 1 is the benchmark those comparisons are measured against.

The result is proved in the paper, not formalized anywhere. The mission adds a machine-checked version of the model and of the proposition, with a corrected first-order clause: the paper states $\chi=\theta$ at every optimum, but at corner optima ($t_l=0$ or $c_l=0$) it is false, and $O'(c_O)=-1/\theta$ also needs $c_O>0$. The formal statement carries exactly these interiority hypotheses, each only on the equation that needs it.

Difficulty

The full-price part is an exact change of variables, but the obvious one fails: substituting $t_w$ from the time constraint gives a set that seems to depend on $r$ and $\delta$ separately, and the sign constraint $t_w\ge0$ must be shown never to bind for non-negative prices (with negative prices it does bind, and the property fails). The supremum has to be compared as a supremum: attainment is not available, since $O$ is not assumed continuous.

The first-order part requires care that the paper skips. An optimum of (PC) is a maximizer of a constrained problem, not of the paper's reduced unconstrained function; one must first show that both constraints bind at an interior optimum where $\partial U/\partial c_l\ne0$, then perturb along feasible curves on which the reduced objective is differentiable, which uses only differentiability of $U$ at one point and of $O$ at one point.

Formalization scope

All quantities are real numbers. $U$ is a function on $\mathbb R\times\mathbb R$ with all assumptions imposed on the closed quadrant; "concave in both arguments" is read as concave in each argument separately (the weaker reading). The purchase decision is a real $y$ entering (PC) as $\delta y$ and $ry$, with $y\in\{0,1\}$ imposed where used. Feasibility of $(r,\delta)$ refers to the buyer's problem. $u^B$ is a supremum in EReal, so infeasible pairs give $-\infty$ rather than a junk value. Prices and time commitments are non-negative throughout. An optimal plan is a maximizer of $U$ over all four variables with $y$ fixed; binding constraints are a conclusion, never part of the definition. $\chi$ is computed from the Fréchet derivative of $U$, and every statement about it assumes differentiability and $\partial U/\partial c_l\ne0$ at the point, so neither fderiv's junk value nor division by zero can make a conclusion true.

A trivializing formalization would define $u^B$ or feasibility through the full price $r+\theta\delta$, or define an optimal plan as one satisfying the first-order conditions; neither is done here: $u^B$ is the supremum over plans satisfying the two constraints of (PC) literally.

A complete development needs elementary real analysis only: supremum manipulation in EReal, one-variable derivatives of compositions along curves, and the vanishing derivative at a local maximum. The time-allocation model is new to the platform and is reusable for the paper's shift-pay results (Lemma 2, Proposition 2). Proofs of Lemma 4 and of Proposition 1 are welcome, as are formal versions of the paper's shift-pay results.

Selected references

• S. Li, M. A. Lariviere, A. Bassamboo, Is Full Price the Full Story When Consumers Have Time and Budget Constraints?, SSRN 4223388 (2022); Manufacturing & Service Operations Management (2023). https://ssrn.com/abstract=4223388, https://doi.org/10.1287/msom.2022.0357
• P. Naor, The Regulation of Queue Size by Levying Tolls, Econometrica 37(1), 1969. https://doi.org/10.2307/1909200
• G. S. Becker, A Theory of the Allocation of Time, The Economic Journal 75(299), 1965. https://doi.org/10.2307/2228949
• G. Allon, A. Federgruen, Competition in Service Industries, Operations Research 55(1), 2007. https://doi.org/10.1287/opre.1060.0335
• P. Afèche, H. Mendelson, Pricing and Priority Auctions in Queueing Systems with a Generalized Delay Cost Structure, Management Science 50(7), 2004. https://doi.org/10.1287/mnsc.1040.0230