Operations Research

Motivation

A buyer may be liable for social responsibility violations among suppliers that remain in its production network. Auditing can prevent a later penalty, but the buyer must pay for each audit and then choose what to do with a supplier that fails. Dropping a supplier can also remove other firms that depend on it, changing the buyer's eventual production profit. Zhang, Aydin, and Parker study this decision in a three-tier supply network and establish a structural rule for an optimal auditing policy in Theorem 3. The rule tells the buyer how dropping and rectification can be ordered without specifying which supplier to audit first.

Setting

There is one buyer in tier 0 and two possible tier-1 firms, $a$ and $b$. The tier-2 suppliers are divided into three disjoint sets: $S_a$, whose members supply only $a$; $S_b$, whose members supply only $b$; and $S_{ab}$, whose members supply both. A network is $g=(S^{(1)},S_a,S_b,S_{ab})$, where $S^{(1)}\subseteq\{a,b\}$ is the set of tier-1 firms still present. Its supplier set $S_g$ contains those tier-1 firms and the members of the three tier-2 sets. The set $D_g(i)$ of dependents of supplier $i$ includes $i$ itself. For a tier-1 firm, it includes its exclusive tier-2 suppliers. For a tier-2 supplier, it also includes a tier-1 firm if that supplier is the firm's sole remaining tier-2 source.

An auditing state $\gamma=(g,U_\gamma)$ records the current network and its finite set of unaudited suppliers, $U_\gamma\subseteq S_g$. The state is terminal when $U_\gamma=\varnothing$. The operator $\gamma\oplus i$ vets an unaudited supplier without changing the network. The operator $\gamma\ominus i$ drops $i$ and $D_g(i)$. If a tier-1 firm is dropped, its formerly shared tier-2 suppliers become exclusive to the other tier-1 firm. These transitions are the paper's footnotes 3 and 4 on page 10.

At a state, the buyer can proceed to production ($pp$), audit and rectify an unaudited supplier ($ar(i)$), or audit and drop one if it fails ($ad(i)$). An auditing policy $\xi$ chooses an admissible action at every state. Let $a\geq0$ be the audit cost, $r\geq0$ the rectification cost, $u\in(0,1)$ the chance that a supplier is noncompliant, $w\in(0,1]$ the chance that an uncorrected violation is exposed, and $z\geq0$ the penalty for an exposed violation. If the buyer proceeds to production, it receives production profit $\pi(g)$ less the expected penalty $\zeta(\gamma)=|U_\gamma|uwz$.

The optimal value $V^*(\gamma)$ is the maximum of the values of the admissible actions at $\gamma$, using the finite recursion (1)–(5) of §3.2. An optimal policy chooses a maximizing action at every state. The appendix also defines the value $V(\xi,\gamma)$ of a fixed policy and the restricted value $V_{ar}(\gamma)$ when only $pp$ and $ar$ are available.

Formalization targets

The main target is Theorem 3, page 19: some optimal policy first audits and drops any number of suppliers, perhaps none, and then enters a second subphase. In that second subphase it either rectifies all remaining unaudited suppliers, in any order, or proceeds directly to production. The choice is governed by the comparison

$$a+ur\leq uwz\quad\text{(rectify all)},\qquad a+ur\geq uwz\quad\text{(proceed to production)}.$$

The inequalities are non-strict: both choices are permitted at equality. The statement applies at every state of the auditing process. Once the policy rectifies a supplier, it rectifies another at the successor state whenever unaudited suppliers remain; no later audit-and-drop action follows. Every available rectification action is optimal during this subphase.

Two appendix results are the milestones. Proposition D.1, OA-11 says that, for each starting state, a buyer can postpone rectification actions until after dropping actions without lowering its value at that state. Proposition D.2, OA-13 identifies the optimal value and actions in the restricted rectify-or-produce problem. With $c_{rp}=\min\{uwz,a+ur\}$, its value formula is

$$V_{ar}(\gamma)=\pi(g)-c_{rp}|U_\gamma|.$$

Significance

Theorem 3 reduces the form of policies that need consideration: rectification need not be interleaved with later dropping, and the final choice between rectification and accepting exposure risk depends on one comparison of per-supplier costs. It does not resolve which suppliers to audit and drop, or when to leave that first subphase. Those decisions can still depend on the network and audit outcomes, as §5.1 explains.

The paper proves the structural result and its two appendix propositions. This mission asks for machine-checked proofs of those known statements, together with a reusable finite representation of network dependents, transitions, and Bellman values. The present draft statements compile with proof placeholders; they are not machine-checked proofs of the claims. The definitions also permit later work on other auditing rules over the same state space.

Difficulty

An audit-and-drop action can change the network and therefore production profit. Comparing it with an audit-and-rectify action is more involved than comparing their immediate costs: a dropped supplier can remove its dependents, and those losses affect all later decisions. The obvious choice of rectifying whenever $a+ur\leq uwz$ ignores the possibility that a later drop removes the rectified supplier anyway. The structural theorem must account for both successor states of an audit and still produce one policy that is optimal at every state.

Formalization scope

Tier-2 suppliers carry labels in an arbitrary type, while every individual network and unaudited set is finite. The tier-2 components of a network are pairwise disjoint. The Lean parameters explicitly require $a,r,z\geq0$, $0<u<1$, and $0<w\leq1$. The paper derives $\zeta$ from independent supplier outcomes; the formalization uses that derived formula, and its Bellman recursions already take the audit outcomes' expectations. The profit $\pi$ is any real-valued function of the current network. This is a disclosed generalization of the Cournot profit used earlier in the paper: §6.1 says the two-subphase result does not depend on the mode of competition, and (D.27) uses only that vetting leaves the network unchanged.

The value functions are defined by recursion on the number of unaudited suppliers. Their maxima are taken over exactly the admissible finite action set, and optimality is checked at every state. Transition functions are total, but the theorems use them only for unaudited suppliers. The action-value functions return zero for inadmissible supplier actions; the fixed-policy recursion returns the production value there. These values have no role for admissible policies. The formulation excludes an unattained policy supremum, a policy that is optimal only at a chosen initial state, or a special production-profit function. Contributions that establish the appendix propositions, the main structural theorem, or useful lemmas about the finite transitions and recursions fit this scope.

Selected references

• H. Zhang, G. Aydin, and R. P. Parker, Social Responsibility Auditing in Supply Chain Networks, Management Science, 2021, authors' accepted manuscript dated 26 February 2021, pp. 8–11, 19, OA-11–OA-13. DOI: 10.1287/mnsc.2020.3950.

Motivation

A constrained optimization problem often has an objective of the form $\varphi(x)=\vartheta(f(x))$: a smooth map $f$ describes the model, while an extended-real function $\vartheta$ gives the cost and can assign $+\infty$ to infeasible outputs. Such a description covers polyhedral constraints, quadratic penalties on pieces, and many nonsmooth composite objectives. Solvers need to know how the local first and second order behavior of $\varphi$ depends on the two parts of the model. The usual chain rules in Rockafellar and Wets, Variational Analysis use qualification conditions stronger than an error bound at the point of interest. Mohammadi, Mordukhovich, and Sarabi develop chain rules under a metric subregularity qualification condition (MSQC), including the second order result targeted here.

The paper was circulated as arXiv:1905.08837v2 in 2019 and published in Mathematics of Operations Research in 2022. This mission follows the pinned arXiv version, whose theorem and page numbering is used throughout. The result is known in mathematics; the open task here is its formalization in Lean. The paper also derives optimality conditions and statements about KKT systems from its second order analysis, but those later applications are outside this mission's target. Source: §§1, 5, 6, 8.

Setting

Fix finite dimensional Euclidean spaces $\mathbb R^n$ and $\mathbb R^m$. An extended-real function $\varphi:\mathbb R^n\to(-\infty,+\infty]$ has finite domain $\operatorname{dom}\varphi=\{x:\varphi(x)<+\infty\}$. Assigning $+\infty$ outside a feasible set lets an ordinary function and a constraint be treated together. A convex piecewise linear-quadratic function (PWLQ) $\vartheta$ has a finite collection of polyhedral convex pieces $\Omega_i$ whose union is its domain. On each piece its value is $\tfrac12\langle A_i y,y\rangle+\langle a_i,y\rangle+\alpha_i$, where $A_i$ is symmetric. The separate formulas must agree where pieces meet, because all describe the same function. Source: (2.9), p. 5.

A function $\varphi$ is fully subamenable at $\bar x$ when it agrees with $\vartheta\circ f$ on a neighborhood of $\bar x$, with $f$ twice differentiable at $\bar x$, $\vartheta$ convex PWLQ, and MSQC satisfied there. Write $\Omega=\{x:f(x)\in\operatorname{dom}\vartheta\}$. MSQC says that for some $\kappa\ge0$ and all $x$ near $\bar x$, $\operatorname{dist}(x,\Omega)\le\kappa\operatorname{dist}(f(x),\operatorname{dom}\vartheta)$. This controls how far a nearby point is from feasibility through its residual in the outer domain. It is the paper's condition (3.5), not metric regularity. Source: Definition 3.2 and (3.5), pp. 9–10; Definition 4.2, p. 16.

The subderivative $d\varphi(\bar x)(w)$ is a lower limit of first order difference quotients as positive time tends to zero and the direction tends to $w$. Given a limiting subgradient $\bar v\in\partial\varphi(\bar x)$, the second subderivative $d^2\varphi(\bar x,\bar v)(w)$ uses the quotient after subtracting the linear term $t\langle\bar v,w\rangle$ and dividing by $\tfrac12t^2$. Proper twice epi-differentiability means these quotients epi-converge to a second subderivative that never equals $-\infty$ and is finite somewhere. The paper gives an equivalent test using recovery directions for every positive null sequence; that test is used in Lean. Source: (2.11), (2.15), (2.16), pp. 6–7.

Formalization targets

Main theorem

For every $\bar v\in\partial\varphi(\bar x)$, a fully subamenable $\varphi$ is properly twice epi-differentiable at $\bar x$ for $\bar v$. With

$$\Lambda(\bar x,\bar v)=\{\lambda\in\partial\vartheta(f(\bar x)):\nabla f(\bar x)^*\lambda=\bar v\},$$

its second subderivative satisfies, for every $w\in\mathbb R^n$,

$$d^2\varphi(\bar x,\bar v)(w)=\max_{\lambda\in\Lambda(\bar x,\bar v)}\bigl\{d^2\vartheta(f(\bar x),\lambda)(\nabla f(\bar x)w)+\langle\lambda,\nabla^2f(\bar x)(w,w)\rangle\bigr\}.$$

The maximum is attained; a supremum alone is a weaker claim. This is Theorem 5.2 and (5.3), p. 22.

Supporting statements

The milestones are the paper's equality rules for first order subderivatives and subgradients (Theorems 3.4 and 3.6), its identification of critical directions with the finite domain of the second subderivative (Theorem 4.4), the PWLQ outer-function formula (4.8), the lower bound (4.10), and the parabolic limit formula (Lemma 5.1). Each names a separate mathematical claim needed to connect the composite model to the goal. Source: §§3–5.

Significance

Theorem 5.2 gives a data-level way to evaluate the second order behavior of a nonsmooth composite: the outer function contributes its own second subderivative, the inner map contributes its Hessian, and multipliers connect the two. Its properness and epi-differentiability clauses make the formula suitable for the paper's later no-gap second order optimality conditions and parametric analysis. Without those clauses, an equality of extended-real expressions alone would not establish the stability of the difference quotients. Source: Theorem 5.2 and §6.

A formal development of this result would add reusable definitions and lemmas for extended-real difference quotients, second-order tangent geometry, PWLQ functions, and local composite error bounds. The present draft contains statements and definitions that compile; it does not yet contain proofs of the open theorem items. The published limiting-subdifferential definition is reused, while the paper-specific local representation and multiplier set are defined here.

Difficulty

A first order expansion of $f$ does not settle the second order claim. Near a polyhedral boundary, the direction $w$ may be tangent while a fixed straight path $\bar x+tw$ leaves the domain; the second-order correction and the outer function's active piece matter. MSQC controls distance to feasibility but does not itself identify a feasible second-order path or a maximizing multiplier. The source therefore needs separate results about critical directions, PWLQ second subderivatives, parabolic limits, and dual attainment before the full formula can be stated with a maximum. Source: §§4–5, especially pp. 17–23.

Formalization scope

Lean uses EuclideanSpace ℝ (Fin n) and EReal. The paper's codomain excludes $-\infty$; the relevant hypotheses enforce that exclusion, while the subderivatives themselves may take either infinite value. The finite domain is defined by exclusion of $+\infty$. A PWLQ representation records finite closed half-space intersections, symmetric operators, and the exact $\tfrac12$ quadratic coefficient. Twice differentiability includes differentiability near the base point and differentiability of the derivative at the point. The composite identity holds on a neighborhood rather than globally. MSQC uses the paper's local distance estimate with $\kappa\ge0$. Positive null sequences represent $t\downarrow0$; a filter lower limit represents the varying direction. The second quotient retains the paper's $\tfrac12t^2$ denominator.

The subdifferentials are the published analytic regular and limiting subdifferentials. Their use matches the paper's geometric subdifferentials at the lower semicontinuous functions in these statements. The goal computes the second subderivative from the lower-limit definition, rather than defining it by (5.3). Full subamenability retains MSQC and a genuine PWLQ representation; it is neither an empty-domain case nor a stronger metric-regularity special case. Contributions toward proofs of the milestone theorems, their needed tangent-set geometry, and the goal are in scope.

Selected references

• A. Mohammadi, B. S. Mordukhovich, M. E. Sarabi, Variational Analysis of Composite Models with Applications to Continuous Optimization, arXiv:1905.08837v2, 2019; published in Mathematics of Operations Research, 2022. https://arxiv.org/abs/1905.08837v2
• R. T. Rockafellar and R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

Motivation

Online and omni-channel retailers promise delivery within a fixed number of days, and carriers charge less for slower service. A retailer that receives orders over time can therefore wait, collect several orders into one package, and send it by a slower and cheaper service, as long as no order misses its promised date. Waiting saves the fixed cost of a shipment but uses up the slack of the orders already waiting. This trade-off between shipment consolidation and expedited delivery is the subject of L. Wei, R. Kapuscinski and S. Jasin, Shipping Consolidation across Two Warehouses with Delivery Deadline and Expedited Options for E-commerce and Omni-channel Retailers (Manufacturing & Service Operations Management, 2020; author's manuscript SSRN 2920899).

The paper treats one and two warehouses, with fixed and with volume-dependent shipping costs. Its first structural result concerns the simplest case, one warehouse and a fixed cost per package: the optimal policy waits while the most urgent order has enough slack and ships everything once the slack falls to a period-dependent threshold. This mission formalizes that result and the lemmas its proof rests on.

Setting

Time is discrete and counted backward: $t$ is the number of periods to go and period $1$ is the last. Each order must be delivered at most $d \ge 1$ periods after it arrives. The slack time of a pending order is the number of periods left until its deadline; slack $1$ means the order must leave now.

Shipping a package that must arrive within $p$ periods costs $F(p)$, the fixed shipping cost, which does not depend on the number of orders in the package. The paper assumes $F$ is non-increasing and convex (slower delivery is cheaper, with diminishing savings), and specifies it on $[1,\infty)$. In each period new orders arrive with probability $\alpha \in [0,1]$.

With one warehouse and fixed costs, the paper's Lemma 1 shows that it is optimal either to ship all pending orders together in one package or to ship none, at a cost depending only on the smallest slack $z$ among pending orders. The state is therefore $z \in \{1,\dots,d\}$, or $\infty$ when nothing is pending. The cost-to-go functions $V_t(z)$ and $V_t(\infty)$ satisfy the recursion (2)–(3): for $t > 1$ and $1 \le z \le d$,

$$V_t(z) = \min\{\,F(z) + V_t(\infty)\ \text{(ship)},\ \ V_{t-1}(z-1)\ \text{(do not ship)}\,\},$$ $$V_t(\infty) = \alpha V_{t-1}(d) + (1-\alpha) V_{t-1}(\infty),$$

with $V_1(z) = F(z)$ and $V_1(\infty) = 0$. Holding is infeasible at $z = 1$. Shipping is optimal at $(t,z)$ when the ship branch attains the minimum; holding is optimal when it is feasible and the do-not-ship branch attains the minimum. With ties both are optimal.

Formalization targets

Goal: Theorem 1 (p. 13)

For every period $t \ge 1$ there is an integer $\tau_t$ such that, for every slack $1 \le z \le d$,

$$z \le \tau_t \implies \text{shipping all pending orders is optimal}, \qquad z > \tau_t \implies \text{holding all pending orders is optimal}.$$

The threshold may depend on $t$, and no formula for it is asserted.

Milestones

1. Lemma E1 (Online Appendix, p. 1). For reals $a_1,\dots,a_n$ and $b_1 \ge \dots \ge b_n$,

$$\min_i (a_i + b_i) - \min_i a_i \ \ge\ b_n.$$

2. Unrolled cost-to-go (proof of Lemma 2, Online Appendix, p. 1). For $t \ge 1$ and $1 \le z \le d$,

$$V_t(z) = \min_{0 \le j \le k} \{F(z-j) + V_{t-j}(\infty)\}, \qquad k = \min\{t,z\} - 1.$$

3. Lemma 2 (p. 13). For $t \ge 1$ and $2 \le z \le d$,

$$V_t(z-1) - V_t(z) \ \ge\ F(z-1) - F(z).$$

4. The downward step (proof of Theorem 1, p. 13). For $t \ge 2$ and $3 \le z \le d$, if shipping is optimal at slack $z$, it is optimal at slack $z-1$.

Significance

Theorem 1 reduces the policy of a $T$-period stochastic control problem to one integer per period. The paper builds on it: Theorem 2 computes the long-run average cost of a constant threshold, Proposition 2 and Lemma 3 describe the best constant threshold, and the two-warehouse analysis of §5 and the heuristics of §7 start from this one-warehouse structure. Lemma 2 states that the cost-to-go reacts to a loss of slack at least as strongly as the current shipping cost does, which the paper calls counter-intuitive (p. 13); it is the property that makes the threshold exist.

The results are proved in the paper, with one gap: the proof of Lemma 2 is written out only for $t \ge d$, and the case $t < d$ is described as similar and omitted. A formal proof closes that case. To the best of our knowledge none of these results has a machine-checked proof.

Difficulty

The natural first idea is to argue that the cost-to-go $V_t(z)$ inherits convexity in $z$ from $F$ and then read off a threshold. That is not what is needed: the threshold needs a comparison between the slope of $V_t$ and the slope of $F$ (Lemma 2), and the paper notes (p. 13) that, without further structure, the difference $V_t(z-1) - V_t(z)$ can a priori be larger or smaller than $F(z-1) - F(z)$, because the optimal shipping periods for slacks $z-1$ and $z$ may differ. The recursion couples two indices, period and slack, through the no-order value $V_t(\infty)$, and its boundary cases ($z = 1$, where shipping is forced, and $t = 1$, the last period) behave differently from the interior. The paper's own argument covers only $t \ge d$; the regime $t < d$, in which the horizon ends before the most urgent order's deadline, is left to the reader.

Formalization scope

• Model. The model is the reduced recursion (2)–(3) itself, encoded as a recursive definition valuePair F α d t returning $(z \mapsto V_t(z), V_t(\infty))$. The reduction from the general dynamic program (1) over all slack vectors to (2)–(3) (Lemma 1) is not formalized; $z$ stands for the smallest slack among pending orders. All objects are deterministic; $\alpha$ enters only through (3).
• Conventions. Periods are counted down, $t \ge 1$. $V_1(\infty) = 0$ (from (1): nothing pending costs nothing in the last period). The boundary condition $V_{t-1}(0) = \infty$ is encoded as a forced shipment at $z = 1$. Every statement is restricted to $1 \le z \le d$, the domain of (2); values outside it, and at $t = 0$, are placeholders. $F : \mathbb R \to \mathbb R$ is real-valued, assumed convex and non-increasing on $[1,\infty)$, and evaluated only at integers $z \ge 1$; the paper's $F(0) = \infty$ is never read and is not encoded.
• Optimality. A decision is optimal when its branch of (2) attains the minimum; ties make both decisions optimal. Holding is optimal only if it is feasible ($t \ge 2$, $z \ge 2$).
• Ruling out a trivial goal. Shipping is always optimal at $z = 1$, so "there is a threshold below which shipping is optimal" holds with $\tau = 1$ for free; the goal also requires holding to be optimal at every slack above the threshold.
• Not formalized. Lemma 1, Proposition 1, Theorem 2 and the results that rest on it (Proposition 2, Lemma 3), the two-warehouse results of §5, the variable-cost model of §6, and the heuristic bounds of §7.
• Infrastructure. Only Finset.inf', ConvexOn and natural-number arithmetic are needed. Lemma E1 is a self-contained fact about finite minima and may be reusable. Alternative proofs of Lemma 2 that avoid the unrolled form are welcome.

Selected references

• L. Wei, R. Kapuscinski, S. Jasin, Shipping Consolidation across Two Warehouses with Delivery Deadline and Expedited Options for E-commerce and Omni-channel Retailers, Manufacturing & Service Operations Management, 2020. https://doi.org/10.1287/msom.2020.0903 — author's manuscript: https://ssrn.com/abstract=2920899

Motivation

Autonomous vehicles (AVs) can drive closer to one another than human drivers, because they react faster and can coordinate in platoons. Transport agencies and industry groups have therefore proposed reserving a designated lane for AVs on highways, so that AVs can exploit short headways without mixing with human-driven vehicles (HVs). Whether such a lane helps depends on a trade-off that is familiar from queueing theory: splitting a highway into two separate lanes loses the efficiency of pooled capacity, while a lane reserved for AVs moves faster when it is busy.

Mirzaeian, Cho and Scheller-Wolf (Management Science, 2021; manuscript SSRN 3278330) model a highway segment as a state-dependent loss queue and compare a no-AV benchmark with the designated-lane policy (the D policy). Their headline finding is that the D policy reduces mean travel time only when the highway is heavily loaded and AVs make up a large enough share of traffic. This mission formalizes that finding.

The queueing model is the state-dependent $M/G_n/c/c$ queue of Cheah and Smith (1994), developed for pedestrian flows, which Jain and Smith (1997) applied to vehicular traffic; its stationary law, display (12) below, is due to Cheah and Smith.

Setting

A highway segment has length $L > 0$ and $N \ge 2$ lanes, each holding at most $c \ge 1$ vehicles. Vehicles arrive as a Poisson process of rate $\lambda$; a vehicle that finds the segment full is turned away. When $n$ vehicles are on a segment of capacity $\kappa$, each travels at mean speed $V_n$, for $1 \le n \le \kappa$, with $V_1 \ge V_2 \ge \dots \ge V_\kappa > 0$. This is the $M/G_n/\kappa/\kappa$ queue. Its stationary law is (display (12) of the paper)

$$\pi_n = \frac{(\lambda L)^n}{n!\,V_n\cdots V_1}\,\pi_0, \qquad \pi_0 = \Bigl(1 + \sum_{n=1}^{\kappa} \frac{(\lambda L)^n}{n!\,V_n\cdots V_1}\Bigr)^{-1},$$

its throughput is $\theta = \lambda(1-\pi_\kappa)$, and its mean travel time is, by Little's law, $W = \bigl(\sum_{n=1}^{\kappa} n\pi_n\bigr)/\theta$ (display (13)).

The benchmark pools all lanes into one queue of capacity $Nc$ with speeds $V^B_n$; its mean travel time is $W^B(\lambda)$. Under the D policy, a fraction $p \in [0,1]$ of arrivals are AVs and must use the designated lane, so there are two independent queues: the AV queue (capacity $c$, speeds $V^{DA}_n$, arrival rate $p\lambda$) and the HV queue (capacity $(N-1)c$, speeds $V^{DH}_n$, arrival rate $(1-p)\lambda$). The overall mean travel time is

$$W^D(p,\lambda) = p\,W^{DA} + (1-p)\,W^{DH}.$$

The jam speeds $V^B_{Nc}$, $V^{DA}_c$, $V^{DH}_{(N-1)c}$ are the speeds of full queues. The paper assumes $V^{DH}_{(N-1)c} < V^B_{Nc}$ throughout, and the AV lane is faster when full than the HV lanes, $V^{DH}_{(N-1)c} < V^{DA}_c$. The threshold is

$$p^{(D,W)} = \frac{V^{DA}_c V^B_{Nc} - V^{DA}_c V^{DH}_{(N-1)c}}{V^{DA}_c V^B_{Nc} - V^B_{Nc} V^{DH}_{(N-1)c}}.$$

Formalization targets

Goal: Proposition 1(a), heavy-load clause (corrected)

For every $p \in [0,1]$ with $p \ne p^{(D,W)}$ there is $\bar\lambda^{(D,W)}(p) > 0$ such that

$$\lambda \ge \bar\lambda^{(D,W)}(p) \implies \bigl(W^D(p,\lambda) \le W^B(\lambda) \iff p \ge p^{(D,W)}\bigr).$$

Milestones

1. The closed form (16): $W = L\sum_{n=0}^{c-1}\frac{(L\lambda)^n}{n!V_{n+1}\cdots V_1} \Big/ \bigl(1 + \sum_{n=1}^{c-1}\frac{(L\lambda)^n}{n!V_n\cdots V_1}\bigr)$ for $\lambda > 0$.
2. Lemma 1: $W$ is increasing in $\lambda$.
3. Display (20): $\lim_{\lambda\to\infty} W = L/V_c$.
4. The policy limits: $W^B_\infty = L/V^B_{Nc}$ and $W^D_\infty(p) = \frac{pL}{V^{DA}_c} + \frac{(1-p)L}{V^{DH}_{(N-1)c}}$.
5. $W^D_\infty(p) \le W^B_\infty$ if and only if $p \ge p^{(D,W)}$.

Significance

The goal makes precise the paper's main policy conclusion: under heavy load a designated AV lane lowers mean travel time relative to the benchmark exactly when the AV share exceeds a threshold that depends only on the three jam speeds. Below the threshold, the loss of pooling dominates. This is the basis for the paper's caution against designating lanes for AVs while AV penetration is low, and the same heavy-traffic argument underlies its comparisons with the integrated policy (Propositions 2 and 3).

The printed Proposition 1(a) is not correct as stated, and the formal statement records the repair. Its heavy-load clause asserts a single $\bar\lambda^{(D,W)}$ valid for every $p$; the travel-time gap behaves like $G(p) + K/\lambda$ with $G$ affine and vanishing at $p^{(D,W)}$, so no single threshold works for AV shares arbitrarily close to $p^{(D,W)}$, and at $p = p^{(D,W)}$ the equivalence can fail for all $\lambda$. Its light-load clause ("$W^D(p) \ge W^B$ for $p\in[0,1]$ when $\lambda$ is small") fails at $p = 1$ whenever the AV lane is as fast as the benchmark at low occupancy and faster at higher occupancy, which includes the paper's calibrated model. The mission therefore poses the heavy-load clause pointwise in $p$, excluding $p = p^{(D,W)}$, which is what the paper's proof establishes. None of these results has a machine-checked proof; the queueing layer (the $M/G_n/c/c$ stationary law, travel time and their heavy-traffic limits) is new on the platform.

Difficulty

The heavy-traffic limits are the core. The obvious route, letting $\lambda \to \infty$ in the definition $W = \sum n\pi_n/(\lambda(1-\pi_c))$, gives the indeterminate form $c/(\lambda\cdot 0)$: the blocking probability $\pi_c \to 1$ and $\lambda(1-\pi_c)$ tends to the jam throughput. The limit has to be read off a rearranged expression, the closed form (16), whose leading terms in $\lambda$ cancel to $L/V_c$. Lemma 1 is a genuine monotonicity statement about a ratio of polynomials in $\lambda$ whose coefficients depend on an arbitrary nonincreasing speed sequence; it cannot be checked degree by degree. The goal then needs strict separation of the two limits away from $p^{(D,W)}$, together with an eventually-in-$\lambda$ argument, and care at $p \in \{0,1\}$, where one of the two D-policy queues receives no traffic.

Formalization scope

The queue is represented by its closed-form stationary law (12), exactly as in the paper; no continuous-time Markov chain is constructed. Speeds are arbitrary real sequences $V : \mathbb N \to \mathbb R$, read at $n = 1,\dots,\kappa$; the platooning model of §3.1.2 (a Markovian arrival process that generates the speeds) is out of scope, and Proposition 1 is stated in terms of the speeds only. "Decreasing" speeds are read as nonincreasing (AntitoneOn on $\{1,\dots,\kappa\}$), and "increasing" in Lemma 1 as weakly increasing. Capacity $c$ is per lane. The arrival rate is real, and the limit is $\lambda \to +\infty$ in $\mathbb R$. Lean's $x/0 = 0$ assigns $W = 0$ at $\lambda = 0$, where the throughput vanishes; Lemma 1 and (16) are therefore stated for $\lambda > 0$, and the goal's $\bar\lambda$ is positive. At $p = 0$ or $p = 1$ the idle queue's junk value carries weight zero. The strict inequality $V^{DH}_{(N-1)c} < V^{DA}_c$ (the proof writes $\le 0$) keeps the threshold's denominator nonzero, and it is necessary for the equivalence. The goal is not trivialized by vacuous hypotheses: the instance $N = 2$, $c = 1$, $V^B \equiv 2$, $V^{DH} \equiv 1$, $V^{DA} \equiv 4$ satisfies all of them, with $p^{(D,W)} = 2/3$ strictly inside $(0,1)$. A statement that drops the exclusion $p \ne p^{(D,W)}$, uses one $\bar\lambda$ for all $p$, or feeds the full rate $\lambda$ to both D-policy queues would not be this result.

A complete development needs finite sums and products, factorials, polynomial-ratio limits at infinity, and a monotonicity argument for ratios of power series truncations. The loss-queue layer (stationary law, throughput, travel time, its closed form, monotonicity and heavy-traffic limit) is reusable for any $M/G_n/c/c$ model, including the paper's integrated policy. Contributions to any milestone, and alternative proofs of Lemma 1, are welcome.

Selected references

• N. Mirzaeian, S.-H. Cho, A. Scheller-Wolf, A Queueing Model and Analysis for Autonomous Vehicles on Highways, Management Science, 2021. https://doi.org/10.1287/mnsc.2020.3692 (manuscript: https://ssrn.com/abstract=3278330)
• J. Y. Cheah, J. MacGregor Smith, Generalized M/G/C/C state dependent queueing models and pedestrian traffic flows, Queueing Systems 15(1):365–386, 1994.
• R. Jain, J. MacGregor Smith, Modeling vehicular traffic flow using M/G/C/C state dependent queueing models, Transportation Science 31(4):324–336, 1997. https://doi.org/10.1287/trsc.31.4.324

Motivation

Many shared assets deteriorate unless someone pays to maintain them: a public infrastructure stock, a jointly used ecosystem, a joint venture's capital, a common research base. When several parties benefit from the same stock and each pays for its own contributions, every party is tempted to wait for the others to pay. Kwon (arXiv:1904.00500, published in Operations Research, 2022) models this as a two-player stochastic differential game in continuous time, in which each player may raise the stock at any rate, and studies the Markov perfect equilibria of the game.

The single-player version is a classical monotone follower problem of singular stochastic control (Alvarez 2001; Øksendal and Sulem 2005; Lon and Zervos 2011): the optimal policy reflects the stock upward at a threshold. In the game, a natural first guess is that free riding lowers that threshold, or that the players take turns reflecting. The paper shows instead that, in the symmetric game, there is an equilibrium in which both players contribute gradually, at a finite rate, below the same threshold as the single decision maker. The equilibrium is a continuous-state analogue of the mixed-strategy delay equilibrium of the war of attrition.

Setting

The stock $Z_t$ lives in an interval $I=(a,b)\subseteq\mathbb R$ ($a=-\infty$ or $b=\infty$ allowed) and satisfies

$$dZ_t=\mu(Z_t)\,dt+\sigma(Z_t)\,dW_t+d\xi_{1t}+d\xi_{2t},$$

on a filtered probability space satisfying the usual conditions, where $W$ is a Wiener process, $\mu<0$ (the stock deteriorates) and $\sigma>0$. Player $i$'s control $\xi_i$ is any adapted, nondecreasing, right-continuous process: its cumulative contribution. A control may jump, including at time $0$. Player $i$'s payoff from the initial stock $x$ is

$$V_i(x;\xi)=\mathbb E^x\Big[\int_0^\infty e^{-rt}\pi(Z_t)\,dt-\int_0^\infty e^{-rt}k\,d\xi_{it}\Big],$$

where $\pi$ is an increasing, bounded-above flow profit, $k>0$ the unit cost and $r>0$ the discount rate. In the symmetric game both players have the same $\pi$ and $k$.

The analysis uses:

1. the uncontrolled process $X^x$, solving $dX=\mu(X)dt+\sigma(X)dW$, $X_0=x$;
2. the resolvent $(Rg)(x)=\mathbb E[\int_0^\infty e^{-rt}g(X^x_t)\,dt]$;
3. the generator $\mathcal A=\tfrac12\sigma(x)^2\partial_x^2+\mu(x)\partial_x-r$;
4. the increasing and decreasing fundamental solutions $\psi,\varphi$ of $\mathcal A\psi=\mathcal A\varphi=0$;
5. the function $q(x)=\pi(x)+[\mu(x)-rx]k$.

Assumptions 1–3 of the paper require Lipschitz coefficients with linear growth, a uniform integrability condition on $e^{-r\tau}(X_\tau)^-$, integrability of $e^{-rt}\pi(X_t)$, and boundary behaviour of $R\pi$ and $q$ at $a$ and $b$; in particular $q$ increases below a point $x^*$ and decreases above it.

The single decision maker's value is

$$V(x)=\begin{cases}k(x-\theta)+V(\theta) & x<\theta,\\ (R\pi)(x)+A\varphi(x) & x\ge\theta,\end{cases}\tag{4}$$

for a threshold $\theta\in I$ and a coefficient $A$ that make $V$ twice continuously differentiable (Lemma 1). The candidate equilibrium rate is

$$u(x)=\begin{cases}-\tfrac1k\big(\mathcal AV(x)+\pi(x)\big) & x<\theta,\\ 0 & x\ge\theta.\end{cases}\tag{6}$$

Formalization targets

Goal: Theorem 2 (pp. 15–16)

If $u$ of (6) is Lipschitz on $I$ with linear growth, then the profile in which both players contribute at the regular rate $d\xi_{it}=u(Z_t)\,dt$ is a Markov perfect equilibrium, and

$$V_1(x;\xi)=V_2(x;\xi)=V(x)\qquad\text{for all }x\in I.$$

The equilibrium is against all adapted deviations, from every initial state, with the opponent keeping its feedback rule $u$.

Milestones

1. Proof of Lemma 1, part (i) (pp. 33–34): for $V$ of (4) in $C^2(I)$, $\mathcal AV+\pi=0$ on $[\theta,b)$, $\mathcal AV+\pi<0$ on $(a,\theta)$, $V'=k$ on $(a,\theta]$ and $V'<k$ on $(\theta,b)$.
2. Lemma 1 (p. 10): such $\theta$ and $A$ exist, and $V$ is the single decision maker's optimal value, attained by reflection at $\theta$.
3. Theorem 1 (pp. 14–15), in the instance where both the opponent and the candidate contribute at regular feedback rates: a $C^2$, nondecreasing, bounded-above $U$ satisfying conditions (iii)–(iv) is the candidate's payoff and dominates every deviation in the class $\Sigma_i$.
4. The optimality condition of §2.2 (p. 10), for $V$ of the form (4) and the operator $\mathcal A^{\xi_j}=\tfrac12\sigma^2\partial_x^2+[\mu+u_j]\partial_x-r$ of an opponent playing a regular rate $u_j$ (as applied on p. 38): conditions (i)–(ii) make $V$ the optimal value over all controls.

Significance

Theorem 2 says that the free-rider problem in this game does not shift the threshold below which the stock is maintained; it changes how the stock is maintained, from instantaneous reflection by one party to gradual, rate-limited contribution by both. The equilibrium value equals the single decision maker's value, so the players lose nothing relative to a single owner who pays for everything, although each pays only part. This contrasts with the asymmetric case, where the paper's Theorem 3 rules out a regular-control equilibrium with smooth payoffs. The result is one of the few explicit equilibria of a nonzero-sum singular-control game with linear costs.

The paper's proofs are on paper only. A formalization requires machine-checked versions of a verification theorem for one-dimensional singular control (the optimality condition), of the analysis of the free-boundary point $\theta$ through the fundamental solutions, and of the passage from best response within a restricted class $\Sigma_i$ to best response among all adapted controls. The verification steps for a controlled diffusion with jumps, Itô's formula for semimartingales with a nondecreasing part, and the comparison $Z\ge X$ with the uncontrolled process are reusable for other singular-control and monotone-follower problems on the platform.

Difficulty

The obvious route, Itô's formula applied to $e^{-rt}V(Z_t)$ along an arbitrary deviation, requires the transversality limit $\mathbb E[e^{-rt}V(Z_t)]\to0$ and uniform integrability of the localised terms. $V$ is unbounded below when $a=-\infty$, and the deviation is arbitrary, so this needs the comparison of every controlled state with the uncontrolled process and Assumption 1(ii). The proof also passes through a best-response theorem for the restricted class $\Sigma_i$ (Theorem 1), whose conclusion is weaker than a Nash equilibrium; the upgrade to all of $\Xi_i$ is a separate argument. Finally, the identification of $\theta$ uses the boundary behaviour of $\psi$, $\varphi$ and the scale density at the ends of $I$, which Mathlib does not provide for general diffusions.

Formalization scope

Time is $[0,\infty)$. The probabilistic data (measure, filtration, Wiener process, the uncontrolled family $X^x$, $\psi$, $\varphi$) form one structure, and the standing assumptions of §2.1 together with Assumptions 1–3 form one predicate, a hypothesis of every theorem. The Itô integral of the state equation is the published relation EthierKurtz.HasBrownianItoIntegral; Mathlib supplies Brownian motion, stopping times, uniform integrability and Stieltjes measures.

Conventions the formalization commits to:

1. The initial value $x$ is the pre-jump value $Z_{0-}$; the discounted cost is a Lebesgue–Stieltjes integral that counts the jump at time $0$.
2. Statements hold for every solution of the relevant state equation; existence and uniqueness of strong solutions (the paper's appeal to SDE theory) is not posed.
3. Payoffs are compared only for admissible controls: finite expected discounted cost and integrable discounted running profit. Since $\pi$ is bounded above, every other control has payoff $-\infty$, so no deviation is lost.
4. Markov perfection is the best-response property from every initial state against the opponent's feedback rule, among all adapted controls.
5. The fundamental solutions are pinned by the Laplace transforms of hitting times, $\mathbb E[e^{-r\tau_y}]=\psi(x)/\psi(y)$ for $x\le y$ and $\varphi(x)/\varphi(y)$ for $y\le x$ (Borodin and Salminen).
6. The scale density of Assumption 3(iii) uses a base point $x_0\in I$ in place of the printed $0$, and the limits of Assumption 3 that may be infinite are limits in the extended reals.
7. Added, and disclosed: $e^{-rt}q(X^x_t)$ is integrable, so that $(Rq)$ of (3) exists, as the paper presupposes.
8. The optimality condition is stated for $V$ of the form (4) only: for an arbitrary $C^2$ function it is false (an affine $V=kx+c$ with large $c$ satisfies its conditions on $I=\mathbb R$ but is unbounded).
9. The class $\mathcal U$ in Theorem 2 is its state-only version (Lipschitz on $I$ with linear growth).

The threshold $\theta$ and coefficient $A$ are not chosen by the formalization: the goal holds for every pair making $V$ twice continuously differentiable on $I$, and smoothness at $\theta$ determines the pair. The rate $u$ is computed from $V$ through the generator, not supplied as a free function, and its nonnegativity is part of the conclusion. A payoff is never a Bochner integral of a non-integrable function, so no junk value can enter an equilibrium comparison.

Contributions welcome: proofs of the milestones, and reusable infrastructure for Itô's formula with nondecreasing càdlàg integrators, comparison theorems for one-dimensional SDEs, and the boundary classification of one-dimensional diffusions.

Selected references

• H. Dharma Kwon, Game of Variable Contributions to the Common Good under Uncertainty, arXiv preprint, 2019 (published in Operations Research, 2022). https://arxiv.org/abs/1904.00500v1
• A. N. Borodin and P. Salminen, Handbook of Brownian Motion — Facts and Formulae, Birkhäuser, 1996. https://doi.org/10.1007/978-3-0348-7652-0
• L. H. R. Alvarez, Singular stochastic control, linear diffusions, and optimal stopping: A class of solvable problems, SIAM Journal on Control and Optimization 39(6), 1697–1710, 2001. https://doi.org/10.1137/S0363012900367825
• L. H. R. Alvarez, On the properties of r-excessive mappings for a class of diffusions, Annals of Applied Probability 13, 1517–1533, 2003. https://doi.org/10.1214/aoap/1069786505
• B. Øksendal and A. Sulem, Applied Stochastic Control of Jump Diffusions, 2nd ed., Springer (cited by the paper as 2005). https://doi.org/10.1007/978-3-540-69826-5
• P. C. Lon and M. Zervos, A model for optimally advertising and launching a product, Mathematics of Operations Research 36(2), 363–376, 2011. https://doi.org/10.1287/moor.1110.0493

Motivation

The apparel industry is a large source of carbon emissions, water use and landfill waste, and much of that footprint comes from garments being discarded early. Fast-fashion retailers such as Zara and H&M combine two operational choices: they offer a very large number of styles each season, and they replenish the styles that turn out to be popular through quick response, i.e. production during the selling season at a higher unit cost. Their garments are also widely reported to be of low quality, which shortens their useful life and reduces the chance of reuse.

X. Long and J. Nasiry, Sustainability in the Fast Fashion Industry (SSRN 3486502; Manufacturing & Service Operations Management, 2022, doi:10.1287/msom.2021.1054), give an operational explanation of low quality: it is driven by the firm's incentive to offer variety. The paper's headline (abstract, and the first sentence of its conclusion) is that when variety is chosen by the firm, quality falls as consumers become more sensitive to fashion or as introducing new styles gets cheaper. This mission formalizes that result and the chain of propositions leading to it.

Setting

A firm sells one season of a fashion product. Before the season it chooses a number of styles $m\ge 1$ (design cost $\beta m$), a common quality $u\ge 0$, and an inventory $q$ per style produced at unit cost $\tfrac k2u^2$. Styles are points on a circle of unit circumference (Salop's circular city). During the season, a trend $x$ uniform on the circle and a market size $n\sim U(0,\bar n)$ are realised. All $n$ consumers buy the style $t^*$ closest to the trend at their valuation

$$p=a+\theta u+\gamma\Big(\tfrac12-|t^*-x|\Big),$$

where $|t^*-x|$ is the arc distance, $a$ is a base value, and $\theta$ and $\gamma$ measure the sensitivity to quality and to fashion. Demand above $q$ is met by quick response at unit cost $\tfrac{k'}2u^2$ with $k'>k$; unsold units of the other styles are wasted.

The paper shows that equally spaced styles are optimal (Lemma 1), computes the expected price $a+\theta u+\gamma/2-\gamma/(4m)$ and the expected quick-response volume $(\bar n-q)^2/(2\bar n)$, and arrives at the firm's problem (1):

$$\max_{m\ge1,\ u\ge0,\ 0\le q\le\bar n}\ \mathbb E\Pi(m,u,q)=\Big(a+\theta u+\frac\gamma2-\frac{\gamma}{4m}\Big)\frac{\bar n}{2}-m\frac k2u^2q-\frac{k'}2u^2\frac{(\bar n-q)^2}{2\bar n}-\beta m .$$

An optimal solution $(m^*,u^*,q^*)$ is a feasible triple with the largest expected profit. The parameters satisfy $0<k<k'$ and $\theta,\gamma,\beta,\bar n>0$; $a$ is any real number.

Formalization targets

Goal: Proposition 4(ii)

For admissible parameters, problem (1) has an optimal solution, and

$$u^*\ \text{decreases in }\gamma,\qquad u^*\ \text{increases in }\beta,\qquad u^*\ \text{decreases in }\bar n,$$

where each comparison changes one parameter, keeps the others fixed, and holds between every optimal solution before the change and every optimal solution after it. Monotonicity is weak: on part of the parameter space the optimal quality does not move.

Milestones

In attack order:

1. the stochastic model reduces to (1): Lemma 1, the expected price, and the two uniform expectations (p. 10–11);
2. for fixed $m$: the optimal inventory $\hat q$ (p. 14), and Proposition 2, which gives the optimal quality $\hat u(m)$, the optimal inventory and the value of (1). For $m>k'/k$ these are $\hat u=\theta/k'$ and $\hat q=0$; for $m\le k'/k$ they are $\hat u=\theta k'/(mk(2k'-mk))$ and $\hat q=\bar n(1-mk/k')$. Proposition 2(iii) adds that $\hat u$ decreases in $m$ and $k'$;
3. the optimal variety: Proposition 3 locates $m^*$ in three ranges of $\gamma$. It is $1$, $\sqrt{\bar n\gamma/(8\beta)}$, or an interior root $m_E\in[1,k'/k]$, with explicit thresholds in $\gamma$ and $\beta$;
4. Proposition 4(i): $m^*$ increases in $\gamma$ and $\bar n$ and decreases in $\beta$ and $k'$.

Significance

The result separates two channels by which fashion sensitivity could affect quality. For a fixed number of styles, the optimal quality does not depend on $\gamma$, $\beta$ or $\bar n$ at all (p. 17). All of the effect therefore runs through variety: more styles mean more leftover inventory or more reliance on expensive quick response, and the firm cuts quality to lower the unit cost. Policy conclusions in the paper rest on this mechanism. The disposal-cost and production-tax analyses of §5 ask whether a regulator can reverse the quality decline, and the environmental-impact comparison (Corollary 3) compares fast fashion with a single-style firm.

The paper proves the result with Karush–Kuhn–Tucker conditions on a non-concave reduced problem, split into four regions of $\gamma$ and several cases in $\beta$. No machine-checked proof of any of its statements exists. A formal development would certify the region analysis, which the paper itself states with thresholds that are easy to mistype. It would also supply a reusable treatment of monotone comparative statics for every selection of a non-unique optimum. Two printed slips are already corrected in the statements: the expectation "$\mathbb E[(\bar n-q)^+]$" on p. 11 should read $\mathbb E[(n-q)^+]$, and the optimal-inventory display on p. 14 needs $u>0$.

Difficulty

The reduced profit $F(m)=\max_{u,q}\mathbb E\Pi$ is not concave in $m$: on $[1,k'/k]$ its second derivative changes sign, and the optimum can jump between $m=1$, an interior critical point $m_E$, and the region-III value $\sqrt{\bar n\gamma/(8\beta)}$. Differentiating an optimality condition, the implicit-function argument the paper uses for $m_E$, says nothing about these jumps or about ties. The goal is stated for every optimal solution, including the parameter values where two values of $m$ are optimal, so a proof needs an argument valid across jumps.

Formalization scope

Everything is real-valued. Parameters form a record with an admissibility predicate. Problem (1) is one explicit real function, and the feasible set is $m\ge1$, $u\ge0$, $0\le q\le\bar n$, with the number of styles $m$ a real number as in the paper's analysis. "Optimal" means a feasible maximiser over this set. "The optimal $x^*$" is read as the $x$-component of every optimal solution; "increases/decreases" are weak; parameter changes are strict and vary one record field ({ P with γ := γ₂ }). Ties at the thresholds of Proposition 3 are handled by asserting uniqueness of $m^*$ only off the thresholds. The circle is AddCircle (1 : ℝ), whose metric is the arc distance and whose Haar measure is the uniform probability; the uniform market size is an interval integral divided by $\bar n$. Lemma 1 is stated in the reduced form its proof uses: equal spacing minimises the expected nearest-style distance. The paper's standing assumption that the base value $a$ is high enough to make quick response always worth using does not enter (1) and is not a hypothesis.

The goal is a statement about every joint maximiser $(m,u,q)$ of the expected profit (1) over $m\ge1$, $u\ge0$, $0\le q\le\bar n$. It compares parameter values that differ in one coordinate only, and it asserts that an optimum exists. For a fixed number of styles the optimal quality does not depend on $\gamma$, $\beta$ or $\bar n$, so a formalization about the per-$m$ optimum would be trivially true; the content lies entirely in how the optimal variety responds.

A proof needs only real analysis: one-variable optimisation of quadratics, existence of a maximiser of a continuous coercive function, and an increasing-differences (Topkis-type) monotonicity argument. A proved abstract version of the latter is on the platform, Supermodularity.Monotonicity.argmax_mono_of_strictly_increasing_differences. Lemma 1 needs integration on AddCircle and a convexity inequality over arc lengths. Contributions of alternative proofs of Proposition 3, and of reusable lemmas on comparative statics of argmax sets, are welcome.

Selected references

• X. Long, J. Nasiry, Sustainability in the Fast Fashion Industry, Manufacturing & Service Operations Management 24(3), 2022; author's manuscript SSRN 3486502 (2021). https://ssrn.com/abstract=3486502, https://doi.org/10.1287/msom.2021.1054
• S. C. Salop, Monopolistic Competition with Outside Goods, Bell Journal of Economics 10(1), 141–156, 1979. https://doi.org/10.2307/3003323
• G. P. Cachon, R. Swinney, Purchasing, Pricing, and Quick Response in the Presence of Strategic Consumers, Management Science 55(3), 497–511, 2009. https://doi.org/10.1287/mnsc.1080.0948
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539

Motivation

A two-sided platform (a ride-hailing service, a marketplace, a payment network) earns money only when its two sides transact, so its value depends on the stock of participants on both sides. A young platform has to decide not only how fast to grow but also which side to grow, and it does so through the prices it sets on each side. Whether to subsidize drivers or riders, sellers or buyers, is a recurring operational decision, and the economics literature on two-sided markets (Rochet and Tirole, 2003; Armstrong, 2006) studies it mostly in static models.

Lian and van Ryzin (SSRN 3310559, later published in Management Science, 2021, doi:10.1287/mnsc.2020.3832) pose the question dynamically: supply and demand stocks grow with the surplus each side receives and decay at their own attrition rates, and the platform chooses prices over time to maximize discounted profit. Their first main result, Theorem 1, says that the optimal mix of the two sides at any moment depends only on the current size of the market, and it describes exactly how that mix moves as the market grows. This mission formalizes Theorem 1 and the lemmas its proof rests on.

Setting

A supply stock $s$ and a demand stock $d$ generate $g(s,d)$ transactions per unit time, where the output function $g$ is homogeneous of degree $\alpha>0$: $g(ks,kd)=k^{\alpha}g(s,d)$ for $k>0$. The returns to scale are decreasing if $\alpha<1$ and increasing if $\alpha>1$. Buyers value a transaction at $v$, sellers incur cost $c<v$. Supply and demand decay at attrition rates $\beta^s_0,\beta^d_0>0$ and grow with adoption coefficients $\beta^s_1,\beta^d_1>0$; the platform discounts at rate $\rho>0$.

When prices are unconstrained, the two stocks reduce to one market size $x$ and a balance $\gamma\in[0,1]$, the share of the size held by supply. With $h(\gamma)=g(\beta^s_1\gamma,\beta^d_1(1-\gamma))$ the output is $g(\gamma,x)=x^{\alpha}h(\gamma)$, and the size evolves by

$$\dot x=-\bigl(\beta^s_0\gamma+\beta^d_0(1-\gamma)\bigr)x+(v-c-\pi)\,g(\gamma,x),$$

where $\pi$ is the platform's per-transaction margin. The platform maximizes $\int_0^\infty e^{-\rho t}\pi\,g(\gamma,x)\,dt$ over balance and margin paths (problem (13)). The net welfare rate is

$$G(\gamma,x)=(v-c)\,g(\gamma,x)-\bigl(\rho+\beta^s_0\gamma+\beta^d_0(1-\gamma)\bigr)x .$$

The paper assumes (Assumptions 1–4) that $h$ is twice differentiable and positive on $(0,1)$, nonnegative at $0$ and $1$, strictly concave ($h''<0$), that $h'$ has a unique zero $\gamma_o\in(0,1)$, the output-maximizing balance, and, when $\alpha<1$, that $(1-\alpha)h'^2<-\alpha h h''$.

In Lean the primitives are the fields of TwoSidedGrowth.Balance.Model (with ASCII names bs0 bd0 bs1 bd1 for the four $\beta$'s), the assumptions are the structure Model.Standing, and h, out, G, kappa, IsBalance, Admissible, profit are the objects above.

Formalization targets

Goal: Theorem 1 (p. 19)

Write $\kappa(x)=(\beta^s_0-\beta^d_0)x^{1-\alpha}/(v-c)$. For every market size $x>0$ the optimal balance is

$$\gamma^*(x)=\max\Bigl\{\min\bigl\{(h')^{-1}(\kappa(x)),1\bigr\},0\Bigr\},\tag{14}$$

in the sense that exactly one balance satisfies (14); it is the unique maximizer of $G(\cdot,x)$ on $[0,1]$; and along any size path the balance path $\gamma^*(x(t))$ yields at least the discounted profit of every other admissible balance path on every finite horizon. Moreover, as $x$ grows from $0$ to $\infty$, $\gamma^*(x)$ moves monotonically:

	$\alpha>1$	$\alpha<1$
$\beta^s_0>\beta^d_0$	$0\to\gamma_o$	$\gamma_o\to 0$
$\beta^s_0<\beta^d_0$	$1\to\gamma_o$	$\gamma_o\to 1$

The balances $0$ and $1$ are the durability-maximizing balances: all of the market on the side that attrites more slowly.

Milestones

1. Lemma 5 (p. 41): along an admissible path, $\int_0^T e^{-\rho t}\pi g\,dt=\int_0^T e^{-\rho t}G\,dt-e^{-\rho T}x(T)+x(0)$.
2. Lemma 6, first sentence (p. 42): $G(\cdot,x)$ is strictly concave on $[0,1]$.
3. (33) (p. 43): the clamp formula is well defined and is exactly the argmax of $G(\cdot,x)$ on $[0,1]$.
4. (34) (p. 43): where $\gamma^*(x)$ is interior,

$$\frac{d\gamma^*}{dx}=\frac{(\beta^s_0-\beta^d_0)(1-\alpha)}{(v-c)h''(\gamma^*(x))x^{\alpha}},\qquad \operatorname{sgn}\frac{d\gamma^*}{dx}=\operatorname{sgn}\bigl((\alpha-1)(\beta^s_0-\beta^d_0)\bigr).$$

Significance

Theorem 1 separates the two controls of the growth problem: the balance is chosen myopically from the current size, and only the margin, which determines how fast the size moves, remains a dynamic decision. Every later result of the paper (the stationary size of Theorem 2, the subsidy and growth policies of §4) analyses a one-dimensional problem in $x$ because of this reduction. The table also has a direct managerial reading: a small market with decreasing returns should be balanced for output, a large one for durability, and with increasing returns the order is reversed.

The result is proved in the paper, partly in prose ("the other three cases can be checked similarly"). No machine-checked version of it is known. The formal development adds a precise reading of (14) when $h'$ is unbounded at the ends (as it is for the paper's own Cobb–Douglas example, where the printed claim that $h'$ is bounded by $h'(0)$ and $h'(1)$ fails), explicit monotonicity and limit statements for all four cases, and a machine-checked version of the profit identity that underlies the reduction.

Difficulty

The identity of Lemma 5 is an integration by parts, and the argmax of a strictly concave function is unique. The work lies elsewhere. The first obstacle is that $h'$ need not be bounded on $(0,1)$, so $(h')^{-1}$ has to be read as an extended inverse with three regimes, and the argmax characterization must handle the boundary cases where $G(\cdot,x)$ is monotone on $(0,1)$ and its maximum sits at an endpoint where $h$ has no derivative. The second is the monotonicity: the naive argument differentiates $\gamma^*$ everywhere, but $\gamma^*$ is constant at $0$ or $1$ on whole intervals of sizes when $h'$ is bounded at an end, and it is not differentiable where it reaches the boundary; monotonicity has to be proved for the clamped function directly, and the derivative formula (34) only on the open set of interior balances, through the inverse function theorem. The limits require continuity of the extended inverse at $\kappa=0$ and the divergence of $\kappa$ at the other end of the size range.

Formalization scope

• Everything lives in the namespace TwoSidedGrowth.Balance; the single definition file Setting holds the model and all derived objects.
• Added, disclosed standing assumptions: $\alpha>0$; $c<v$; continuity of $h$ on $[0,1]$. Positivity of the $\beta$'s and of $\rho$ is printed. Homogeneity is posed for $k>0$ and $s,d\ge 0$. Assumption 3, printed "on [0,1]", is posed as a unique zero of $h'$ in $(0,1)$; derivatives of $h$ are never evaluated at $0$ or $1$.
• (14) is the predicate IsBalance: an interior root of $h'(\gamma)=\kappa(x)$, or $0$ when $h'\le\kappa(x)$ on $(0,1)$, or $1$ when $\kappa(x)\le h'$ on $(0,1)$. It is not defined as an argmax of $G$, and the profit of (13) is the integral of $e^{-\rho t}\pi g$, not the right-hand side of Lemma 5; either shortcut would make the main conjuncts definitional and is ruled out.
• Problem (13) is posed on every finite horizon $[0,T]$, over admissible triples: $x>0$ continuously differentiable and obeying the state equation, $\gamma\in[0,1]$ and $\pi$ continuous. The comparison holds the size path fixed, following §3.5. The impulse (Dirac) controls of §3.6 are outside the mission.
• "Decreasing/increasing" is monotone on $(0,\infty)$ and strict on the set of interior balances; "from $a$ to $b$" are the limits at $0^+$ and $+\infty$. The case $\alpha=1$ is not claimed.
• The source is the SSRN working-paper version of 2020-01-16; labels and pages refer to it. Not in scope: Lemma 1 (CES examples), Proposition 1, Theorem 2, the growth-policy results (Theorems 3–6, Propositions 2–16), and the second sentence of Lemma 6.
• Contributions welcome: proofs of the milestones, and reusable facts about extended inverses of strictly monotone continuous functions and the interval-integral integration by parts with exponential discounting.

Selected references

• Z. Lian, G. van Ryzin, Optimal Growth in Two-Sided Markets, SSRN working paper 3310559, version of 2020-01-16. https://ssrn.com/abstract=3310559 — published in Management Science, 2021. https://doi.org/10.1287/mnsc.2020.3832
• J.-C. Rochet, J. Tirole, Platform Competition in Two-Sided Markets, Journal of the European Economic Association 1(4), 2003. https://doi.org/10.1162/154247603322493212
• M. Armstrong, Competition in Two-Sided Markets, RAND Journal of Economics 37(3), 2006. https://doi.org/10.1111/j.1756-2171.2006.tb00037.x