Operations Research

Motivation

Firms in a supply chain often hold equity in one another. A retailer may own a minority stake in a supplier without controlling it: the stake is passive, but it changes what the retailer cares about, because part of the supplier's profit now accrues to her. Avinadav and Shamir (Management Science, 2023) study how such partial vertical ownership (PVO) affects two classic frictions of decentralized supply chains: the supplier's under-investment in capacity, and the retailer's incentive to distort the demand information she shares. This mission formalizes the paper's benchmark result, Theorem 1, which settles the capacity question when both firms know the market state. It is the reference point against which the paper measures every asymmetric-information equilibrium, and a companion mission treats the paper's cheap-talk result (Theorem 2).

The question belongs to the literature on capacity investment with advance orders and on cross-ownership in vertical relations; the paper's Sections 1–2 survey it. The result itself is a threshold statement of a familiar newsvendor type, but in a model where the decision maker's objective mixes her own operating profit with a fraction of her supplier's.

Setting

A supplier builds a capacity $K$ at unit cost $c$ before the selling season. After demand $D$ is realized, the retailer orders $\min(K, \max(q^{adv}, D))$ at the wholesale price $w$ and sells at the retail price $r$, where $r > w > c$. Here $q^{adv} \ge 0$ is an advance order: a quantity the retailer commits to before the supplier builds capacity, and which the supplier must cover, $K \ge q^{adv}$. Unmet demand is lost and leftovers have no value.

Demand in market state $i \in \{L, H\}$ is $D_i = \mu_i + \varepsilon$ with $0 < \mu_L < \mu_H$, where the shock $\varepsilon$ has mean zero, cumulative distribution function $F$, a density, and support $(\underline\varepsilon, \bar\varepsilon)$ with $\mu_L + \underline\varepsilon \ge 0$. The expected profits are

$$\pi_s(K \mid \mu_i, q^{adv}) = \mathbb E\big[w\min(K, \max(\mu_i + \varepsilon, q^{adv})) - cK\big],$$ $$\pi_r(q^{adv}, K \mid \mu_i) = \mathbb E\big[(r - w)\min(\mu_i + \varepsilon, K) - w\max(q^{adv} - \mu_i - \varepsilon, 0)\big].$$

The retailer owns a share $\beta \in [0, 1]$ of the supplier and maximizes the accounting payoff

$$v_r(q^{adv}, K \mid \mu_i) = \pi_r(q^{adv}, K \mid \mu_i) + \beta\,\pi_s(K \mid \mu_i, q^{adv}).$$

The relevant critical fractiles are $z_s = 1 - c/w$ (supplier), $z_r = 1 - w/r$ (retailer without holdings) and

$$z_r(\beta) = 1 - (1 - z_r)(1 - \beta z_s) = z_r + \beta z_s (1 - z_r).$$

Under complete information both firms observe $i$. The supplier answers $q^{adv}$ with the capacity $K_i^{CI}(q^{adv})$, equal to $\mu_i + F^{-1}(z_s)$ if $q^{adv} \le \mu_i + F^{-1}(z_s)$ and to $q^{adv}$ otherwise (5). The retailer compares two options: order nothing and accept $\mu_i + F^{-1}(z_s)$, or order $q^* \in \arg\max_{q} v_r(q, q \mid \mu_i)$ and finance the whole capacity (6)–(7).

Formalization targets

Goal: Theorem 1

Let

$$\underline\beta = \min\Big\{\beta \in [0,1] : z_r(\beta)\big(F^{-1}(z_r(\beta)) - F^{-1}(z_s)\big) + \big(z_r + \beta(1 - z_r)\big)\int_{\underline\varepsilon}^{F^{-1}(z_s)} F - \int_{\underline\varepsilon}^{F^{-1}(z_r(\beta))} F \ge 0\Big\}.$$

Then the minimum exists, $\underline\beta < 1$, and for both market states

$$\big(q_i^{CI}, K_i^{CI}\big) = \begin{cases} \big(0,\ \mu_i + F^{-1}(z_s)\big) & \beta < \underline\beta,\\ \big(\mu_i + F^{-1}(z_r(\beta)),\ \mu_i + F^{-1}(z_r(\beta))\big) & \beta \ge \underline\beta. \end{cases}$$

The formal goal adds that the order chosen by (7) maximizes $q^{adv} \mapsto v_r(q^{adv}, K_i^{CI}(q^{adv}) \mid \mu_i)$ over $q^{adv} \ge 0$.

Milestones

In the order the proof uses them: the closed form (2) of $\pi_s$; the optimality of (5); the closed form (4) of $v_r$; the §4 observation that ordering a positive quantity up to $\mu_i + F^{-1}(z_s)$ is weakly dominated by ordering nothing; the closed form, concavity and unique maximizer $q^* = \mu_i + F^{-1}(z_r(\beta))$ of $q \mapsto v_r(q, q \mid \mu_i)$ (Appendix E, p. 43); the identity between the payoff gain $G(\beta) = \tfrac1r\big(v_r(q^*, q^* \mid \mu_i) - v_r(0, \mu_i + F^{-1}(z_s) \mid \mu_i)\big)$ and the expression in (9) (pp. 43–44); and Lemma E1, the existence of a unique threshold $\underline\beta \in [0,1)$ with $G(\beta) \ge 0 \iff \beta \ge \underline\beta$ (p. 44).

Significance

Theorem 1 says that a large enough passive stake always makes the retailer finance the entire capacity, and that full ownership is never needed: $\underline\beta < 1$ for every choice of prices, costs and demand law. The mechanism is visible in $z_r(\beta)$: each unit the retailer buys costs her effectively $w - \beta(w - c)$, so her preferred capacity grows with $\beta$, and from $\underline\beta$ on it is worth paying for. The theorem is also the benchmark for the rest of the paper: the cheap-talk, signaling and pooling equilibria of §§5–7 are compared with $(q_i^{CI}, K_i^{CI})$, and the thresholds $\underline\beta$ and $\underline{\underline\beta}$ jointly delimit the paper's regimes.

The result is proved in the paper (Appendix E, pp. 42–44). It has not been formalized. A formal proof adds two things beyond confirmation. First, it settles a step the paper asserts without argument: that $G(\beta) < 0$ whenever $z_r(\beta) \le z_s$, which is what forces $q^* > \mu_i + F^{-1}(z_s)$ in the second case of (8). Second, it produces reusable lemmas about newsvendor-type expectations under a general demand law with a density: the layer-cake identities behind (2)–(4) and the unique maximization of $q z - \int^{q} F$ at a quantile.

Difficulty

The identities (2)–(4) are integration-by-parts computations, but they must be done for an arbitrary law with a density, with oriented interval integrals and without assuming bounded support. The concavity and the maximizer at $F^{-1}(z_r(\beta))$ require that the quantile be a genuine inverse of $F$ on $(0,1)$.

The central difficulty is Lemma E1. The natural argument computes $G'(\beta)$ and observes it is positive when $z_r(\beta) > z_s$. That does not settle the sign of $G$ on the complementary region, where the paper argues informally that the supplier "builds a higher capacity for free". The comparison in $G$, however, uses capacity $q^*$ even when $q^* < \mu_i + F^{-1}(z_s)$, so that informal argument compares the wrong objects; a separate estimate is needed there. Differentiability of $\beta \mapsto F^{-1}(z_r(\beta))$ is also not given: the density need not be continuous or positive at the quantile, so the monotonicity of $G$ cannot simply be read off a derivative.

Formalization scope

The primitives $c, w, r, \mu_L, \mu_H$, the law $P$ of $\varepsilon$ and $\underline\varepsilon$ form a structure; $F$ is Mathlib's ProbabilityTheory.cdf P, and $F^{-1}(z) = \inf\{x : F(x) \ge z\}$, applied only at levels in $(0, 1)$. The payoffs $\pi_s, \pi_r, v_r$ are defined as Bochner integrals of the realized profits; the closed forms are milestones, not definitions. The expression of (9) is defined as printed, because Theorem 1 defines $\underline\beta$ by it, and a milestone ties it to the payoff gain $G$, which is defined with its factor $1/r$. The market state is quantified as $\mu \in \{\mu_L, \mu_H\}$ and the share as $\beta \in [0, 1]$.

The standing assumptions are those of §3: $P$ is a probability measure, $\varepsilon$ has mean zero and a density, $\underline\varepsilon < 0$ with $F(\underline\varepsilon) = 0$, $0 < \mu_L < \mu_H$, $\mu_L + \underline\varepsilon \ge 0$, and $c < w < r$. Three implicit assumptions are added and disclosed: $c > 0$ (otherwise $z_s = 1$ and $F^{-1}(z_s)$ is not defined), integrability of $\varepsilon$ (presupposed by "zero mean"), and strict increase of $F$ on the support $\{x \ge \underline\varepsilon : F(x) < 1\}$ (the paper uses $F^{-1}$ as an inverse). The advance order ranges over $q^{adv} \ge 0$, and $K \ge q^{adv}$ is a hypothesis of (2) and (4).

Two trivializations are ruled out. Defining the profits by their closed forms would make the payoff milestones true by definition, so they are expectations. Replacing the rule (7) by "an arg max of $q \mapsto v_r(q, K_i^{CI}(q) \mid \mu_i)$" would be ill-posed, because that maximizer is not unique (for $\beta < 1$ every order up to $\mu_i + \underline\varepsilon$ ties with $0$); $q^{CI}$ is the two-option rule as printed, and its optimality is a separate conclusion.

Proofs of any milestone are welcome, as are general lemmas on expectations of $\min/\max$ of a shifted random variable, on quantiles of continuous strictly increasing CDFs, and on the continuity of $\beta \mapsto F^{-1}(z_r(\beta))$. The source is the authors' manuscript of 2022-06-06; its proofs are in Appendix E.

Selected references

• T. Avinadav and N. Shamir, Partial Vertical Ownership, Capacity Investment, and Information Exchange in a Supply Chain, Management Science, 2023 (read as the authors' manuscript of 2022-06-06; Theorem 1 on p. 11, proof on pp. 42–44). https://doi.org/10.1287/mnsc.2023.4673
• G. P. Cachon, Supply Chain Coordination with Contracts, Handbooks in Operations Research and Management Science 11, 2003 (the newsvendor and wholesale-price contract background). https://doi.org/10.1016/S0927-0507(03)11006-7

Motivation

In 2018 New York City's Taxi and Limousine Commission adopted a minimum earnings rule for ride-hailing drivers: each platform must pay drivers, per hour spent with a passenger, at least a target hourly earnings level divided by the platform's measured driver utilization in the previous period. The rule ties next period's wage floor to this period's idle time, so a platform that over-recruits drivers must raise wages. Asadpour, Lobel and van Ryzin (SSRN 3502607, published in Manufacturing & Service Operations Management, 2022) model this rule as a dynamical system and ask when the regulated marketplace can stay stable, meaning wages stay bounded while the platform does not lose money.

Their main result (Theorem 1, a separate mission of this series) characterizes stability in a deterministic market. Real markets are hit by demand shocks: a sudden drop in ride requests lowers utilization in one period, and the rule then forces a high wage in the next. This mission formalizes the paper's answer (Theorem 2, §4.1) to whether a platform that may not subsidize rides can absorb such a one-time shock.

Setting

Time is discrete. In each period $t$ the platform chooses a price $p_t \ge 0$ per ride hour and a wage $w_t \ge 0$ per ride hour. The demand $D(p)$ is the number of ride hours requested at price $p$; the supply $S(z)$ is the number of driver hours offered when drivers earn $z$ per hour. Rides served are $Q(p,z) = \min\{D(p), S(z)\}$, the utilization is $u(p,z) = Q(p,z)/S(z)$, and drivers' hourly earnings $z_t$ solve the equilibrium condition

$$z_t = w_t \, u(p_t, z_t).$$

A price, wage and earnings sequence satisfying this in every period is an equilibrium-augmented policy. The platform's profit is $\pi(p,w,z) = (p-w)\,Q(p,z)$. With target $M > 0$, the minimum earnings rule requires

$$w_{t+1} \ge \frac{M}{u(p_t, z_t)} \quad \text{in every period.}$$

The revenue and cost functions are $R(p) = p\,D(p)$ and $C(z) = z\,S(z)$. The paper assumes $D$ positive, strictly decreasing and continuous; $S$ strictly increasing, continuous, and positive and differentiable away from $0$; $R$ unimodal with maximum at $p^*$; and demand and supply crossing at $w^*$, $D(w^*) = S(w^*)$. $H$ is the inverse of $C$, and $J$ is the inverse of $R$ on its decreasing branch: $J(r) = p$ iff $p \ge p^*$ and $R(p) = r$.

A shock lowers utilization to $u_0$ in one period. A marketplace absorbs a $u_0$ utilization shock (Definition 3) if some feasible equilibrium-augmented policy obeying the rule, with first post-shock wage $w_1 \ge M/u_0$, has bounded wages and non-negative profit in every period.

Formalization targets

Goal: Theorem 2

$$\text{the marketplace absorbs a } u_0 \text{ utilization shock} \iff u_0 \ge \frac{M}{J(C(M))}.$$

The threshold is explicit in the model primitives; no constant is chosen by the formalization.

Milestones (the steps of the published proof, Online Appendix p. 5)

1. If $u_0 < M/J(C(M))$ and $w_1 \ge M/u_0$, then $M/H(R(w_1)) \ge \phi(M,u_0) > 1$, where $\phi(M,u_0) = M/H(R(M/u_0))$.
2. Along a policy with $p = w$ after such a shock, $w_{t+1} \ge \phi(M,u_0)\,w_t$, hence $w_t \ge \phi(M,u_0)^{t-1} w_1$.
3. If $u_0 \ge M/J(C(M))$, then at $p = w = J(C(M))$ and $z = M$: $z/w = D(p)/S(z) = u(p,z)$, so $z = M$ is an equilibrium.

Significance

The result. Theorem 2 quantifies the fragility of a regulated marketplace whose platform cannot cross-subsidize: there is a sharp utilization level below which a single shock sends wages into unbounded growth, and above which the platform recovers immediately with a zero-profit stationary policy. Its threshold depends on the market only through the decreasing branch of revenue and the cost of paying $M$, which makes it a concrete design criterion for the target $M$: a regulator choosing $M$ also chooses how deep a utilization drop the market can survive. The remark after the theorem (p. 14) relates it to the stability threshold of Theorem 1.

Formalizing it. The result is proved in the paper; no machine-checked version exists. A formal proof must close points the published argument leaves implicit: the reduction to $p = w$ policies (the paper's Lemma 3, posed in mission I) must hold in the all-periods form used here; the wage recursion of Lemma 4 needs wages above $w^*$, which the proof does not check; and the sufficiency policy needs $J(C(M)) \ge M$, which holds only because utilizations are at most one. The mission also gives the platform a second, independent use of the shared marketplace model.

Difficulty

The sufficiency direction is a direct check of one stationary policy. The necessity direction is where the work lies. The natural attempt, to argue that a high first wage simply cannot be paid without loss, fails: profit only requires $p_t \ge w_t$, and a platform may raise its price along with the wage. The obstruction is dynamic. Raising the price above $J(C(M))$ lowers revenue below the cost of supplying earnings $M$, so equilibrium earnings fall below $M$, utilization falls, and the rule raises the next wage by a factor bounded away from one. Turning this into a proof requires controlling arbitrary policies with $p_t \ge w_t$, not just the convenient $p = w$, and carrying an induction hypothesis (wages stay above $M/u_0$) that the paper does not state.

Formalization scope

The Lean development lives in namespace MinEarnings.Shock. Demand and supply are functions D S : ℝ → ℝ; all regularity is required on $[0,\infty)$, and "differentiable" is read as differentiable on $(0,\infty)$, which is all the argument uses. "$R$ unimodal with maximum at $p^*$" is strict increase on $[0,p^*]$ and strict decrease on $[p^*,\infty)$. The points $p^*$, $w^*$ and the inverse cost $H$ are parameters carrying their defining properties. Time is 0-based: Lean's period $0$ is the paper's period $1$, so the shock constraint $w_1 \ge M/u_0$ is a bound on Lean's first wage and the rule constrains every later wage. Bounded wages means $\exists B\ \forall t,\ w_t \le B$, and profit is non-negative in every period.

Three conventions are pinned and disclosed in every statement:

• $J(C(M))$ is not defined as a function. It is passed as a price $q$ with $q \ge p^*$ and $R(q) = C(M)$, which determines it uniquely. The paper's $J$ is defined on $(0, R(p^*)]$, which presumes $R(p) \to 0$, an assumption the paper does not make.
• The shock utilization satisfies $0 < u_0 \le 1$. Without $u_0 \le 1$, which Definition 3 leaves implicit, the sufficiency direction fails when $p^* \le w^* < M$.
• Equilibrium earnings are positive, $z_t > 0$. Lean defines $0/0 = 0$, so a zero-earnings "equilibrium" with $S(0) = 0$ would have utilization $0$ and turn the rule into $M/0 = 0 \le w_{t+1}$; the positivity requirement rules out this trivializing reading, and the requirement that wages be bounded uniformly rules out a vacuous reading of stability.

The development needs only Mathlib's real analysis: monotonicity on intervals, inverse functions on $(0,\infty)$, and geometric growth of sequences. The setting file is shared, up to namespace, with the other two missions of the series. Contributions welcome: proofs of the milestones, a proof of the all-periods reduction to $p = w$ policies, and a general lemma that a sequence with $w_{t+1} \ge \phi w_t$, $\phi > 1$, $w_0 > 0$ is unbounded.

Selected references

• A. Asadpour, I. Lobel, G. van Ryzin, Minimum Earnings Regulation and the Stability of Marketplaces, SSRN 3502607 (version of August 24, 2022); Manufacturing & Service Operations Management, 2022. https://ssrn.com/abstract=3502607 · https://doi.org/10.1287/msom.2022.1150

Utilization-based minimum earnings rules

In 2018 New York City's Taxi and Limousine Commission (TLC) imposed a minimum pay formula on the largest ride-hailing platforms, following a proposal by Parrott and Reich (2018): the pay per minute and per mile driven is divided by the platform's utilization rate, the fraction of drivers' working time spent carrying passengers. Seattle adopted a similar rule in 2020. The rule targets drivers' hourly earnings while leaving them free to choose when and how much to work. Because utilization is only observed after the fact, the regulation computes the floor for the next measurement period (six months in New York) from the utilization of the current one.

Asadpour, Lobel and van Ryzin (2022) model this rule as a dynamic system and ask when a platform can comply with it while keeping wages bounded and profits non-negative. This mission formalizes their Theorem 3: the lag in the rule does not matter for stability, because the dynamic system is stable exactly when a single static system of equations has a solution. Two companion missions of the series formalize Theorem 1 (the threshold $z^*$ on stable earnings targets) and Theorem 2 (absorption of a utilization shock).

Setting

Time is discrete. In period $t$ the platform charges riders a price $p_t \ge 0$ per hour of driving and pays drivers a wage $w_t \ge 0$ per hour of driving riders. A demand function $D$ gives the ride hours demanded at price $p$, and a supply function $S$ gives the driver hours offered at expected hourly earnings $z$. The regularity assumptions are that $D$ is positive, strictly decreasing and continuous, and $S$ is strictly increasing, continuous, and positive and differentiable away from zero. The ride hours produced, the utilization and the platform's profit are

$$Q(p,z)=\min\{D(p),S(z)\},\qquad u(p,z)=\frac{Q(p,z)}{S(z)},\qquad \pi(p,w,z)=(p-w)\,Q(p,z).$$

Drivers earn $w_t$ only while busy, so earnings satisfy the equilibrium condition $z_t = w_t\,u(p_t,z_t)$. The minimum earnings rule with target $M>0$ is

$$w_{t+1}\ \ge\ \frac{M}{u(p_t,z_t)}\qquad\text{for every period } t.$$

The $M$-minimum-earnings marketplace is stable if some policy $(p_t,w_t,z_t)$ that is feasible, satisfies the equilibrium condition and obeys the rule has a bounded wage sequence and $\pi(p_t,w_t,z_t)\ge 0$ in all but finitely many periods. It is statically stable if there are $p,w,z\ge 0$ and $u\in(0,1]$ with

$$u=\frac{Q(p,z)}{S(z)},\qquad z=w\,u,\qquad w\ge\frac{M}{u},\qquad p\ge w. \tag{8}$$

Formalization targets

Goal: Theorem 3

$$\text{the } M\text{-minimum-earnings marketplace is stable}\iff\text{it is statically stable}.$$

The statement carries only the regularity assumptions on $D$ and $S$ and $M>0$.

Milestones

The milestones follow the proof in the Online Appendix.

1. A statically stable marketplace is stable.
2. Along a policy with $p_t = w_t$ that satisfies the equilibrium condition and the rule, if $u_{t+1}\ge u_t$ for some $t$, the marketplace is statically stable.
3. Along the same kind of policy, if $w_t\ge M/u_t$ for some $t$, the marketplace is statically stable.
4. If neither case occurs and wages are bounded, then $w_t\to w$ and $u_t\to u$, and the limits satisfy $0<u\le 1$, $w\ge M/u$ and $u = Q(w,wu)/S(wu)$.

Significance

Theorem 3 reduces a question about infinite sequences to a question about one system of four relations in four unknowns. The paper uses it to give a second proof of its threshold theorem, and it shows that the lag in the regulation cannot be blamed for instability: every earnings target that a real-time rule could sustain can also be sustained under the lagged rule, and conversely. This gives regulators and platforms a criterion that can be checked by solving equations rather than by simulating policies.

The result is proved in the paper. No machine-checked version of it or of the paper's other results exists. Formalizing it checks the passage to the limit in the dynamic-to-static direction, where the paper leaves one step implicit (the positivity of the limiting utilization), and it provides a Lean model of the regulated marketplace that the other two missions of the series share.

Difficulty

The static-to-dynamic direction is immediate. In the other direction, a stable policy is a sequence, and a solution of (8) is a single point. Fixing one period of a stable policy does not give such a point: the rule compares $w_{t+1}$ with $u_t$, while (8) compares $w$ with the utilization of the same point. A solution has to be extracted either from a period where the comparison happens to go the right way or from a limit. The limit is delicate because the utilization $Q(p,z)/S(z)$ is a ratio, and a limit with $u = 0$ would not solve (8). The positivity of the limiting utilization has to come from the rule and the bound on wages together. The reduction to policies with $p_t = w_t$ (Lemma 3 of the paper) also has to be carried out on the policy before the case analysis can start; that lemma is posed as a milestone of the first mission of this series and is not repeated here.

Formalization scope

Prices, wages and earnings are real numbers, and $D, S : \mathbb{R}\to\mathbb{R}$ are constrained on $[0,\infty)$. A policy is a triple of sequences indexed by $\mathbb{N}$ starting at $0$, so Lean's period $t$ is the paper's period $t+1$, and the rule constrains every wage except the first. "Bounded" is an upper bound on the wages, which are non-negative; "all but finitely many periods" is an eventually-along-atTop statement. "Differentiable" is read as differentiability on $(0,\infty)$ together with continuity on $[0,\infty)$.

The equilibrium condition requires $z_t>0$. Without it the encoding is trivial: if $S(0)=0$, which the assumptions allow, Lean evaluates $u(p,0)=0/0$ as $0$, the rule becomes $0\le w_{t+1}$, and every target $M$ would count as stable. For the same reason Definition 4's $u\in(0,1]$ is kept with its strict lower bound. The paper's standing assumptions that the revenue $pD(p)$ is unimodal and that $D$ and $S$ cross are not used by Theorem 3 or its proof and are not assumed, so the formal statements are slightly more general than the paper's.

A complete development needs basic real analysis from Mathlib (monotone convergence, continuity of $D$, $S$ and $\min$, limits of quotients) and the equilibrium construction behind Lemma 3, which uses the inverse of the cost function $C(z)=zS(z)$. That construction is reusable across the series. Proofs of the milestones, of the $p=w$ reduction, and of the goal are all welcome.

Selected references

• A. Asadpour, I. Lobel, G. van Ryzin, Minimum Earnings Regulation and the Stability of Marketplaces, SSRN 3502607 (version of August 24, 2022); Theorem 3 on p. 15, proof in Online Appendix pp. 5–6. https://ssrn.com/abstract=3502607
• A. Asadpour, I. Lobel, G. van Ryzin, Minimum Earnings Regulation and the Stability of Marketplaces, Manufacturing & Service Operations Management, 2022. https://doi.org/10.1287/msom.2022.1150
• J. A. Parrott, M. Reich, An Earnings Standard for New York City's App-based Drivers: Economic Analysis and Policy Assessment, report for the New York City Taxi and Limousine Commission, 2018 (cited in the paper as Parrott and Reich [2018]).

Motivation

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

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

Setting

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

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

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

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

Its convex conjugate is

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

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

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

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

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

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

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

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

Formalization targets

Goal: Proposition 3 (p. 25)

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

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

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

Milestones

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

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

Centralized markets such as kidney exchanges, ride-sharing platforms and online labor markets match agents who arrive over time. Kerimov, Ashlagi and Gurvich (SSRN 3824407; Management Science, 2023, doi:10.1287/mnsc.2021.01215) study such a market with $n$ agent types and $d$ feasible multi-way matches. Their main result is that, when a fluid linear program called the static-planning problem (SPP) has a unique non-degenerate solution, a periodic resolving policy keeps the regret against the hindsight optimum bounded by a constant of order $1/\epsilon$ at all times, where the general position gap $\epsilon$ is the smallest positive basic variable of (SPP).

The constant $1/\epsilon$ is only informative if one can say what $\epsilon$ is. Section 5 of the paper does this for a class of networks it calls (SPP)-acyclic: there the optimal solution of (SPP) is an explicit signed sum of arrival rates, so $\epsilon$ is an imbalance between sums of arrival probabilities. This mission formalizes that structural result and the lemmas it rests on. It needs no probability: only the combinatorics of the network and linear programming.

Setting

A matching network has agent types $\mathcal A = \{1,\dots,n\}$ and matches $\mathcal M = \{1,\dots,d\}$. Match $m$ uses one agent of each type in a set $\mathcal A(m)$ with $|\mathcal A(m)| \ge 2$, every type belongs to some match, and the matching matrix $M \in \{0,1\}^{n\times d}$ has $M_{im} = 1$ iff $i \in \mathcal A(m)$. Arrival probabilities $\lambda$ satisfy $\lambda_i > 0$, $\sum_i \lambda_i = 1$, and match values satisfy $r_m > 0$.

The matching network graph $\mathcal G$ is the bipartite graph whose vertices are the types and the matches, with an edge between type $i$ and match $m$ iff $i \in \mathcal A(m)$.

For a right-hand side $b \in \mathbb R^n$, the static-planning problem is

$$\max\ r\cdot z\quad\text{s.t.}\quad Mz + s = b,\quad z \in \mathbb R^d_{\ge 0},\ s \in \mathbb R^n_{\ge 0},$$

and (SPP) is the case $b = \lambda$. For a solution $(z^*, s^*)$ write $\mathcal M_+ = \{m : z^*_m > 0\}$ (active matches), $\mathcal M_0 = \mathcal M \setminus \mathcal M_+$ (redundant matches), $\mathcal Q_+ = \{j : s^*_j > 0\}$ and $\mathcal Q_0 = \mathcal A \setminus \mathcal Q_+$.

The network satisfies the general position condition (GP) if (SPP) has a unique optimal solution $(z^*, s^*)$ and it is non-degenerate: $|\mathcal M_+| + |\mathcal Q_+| = n$. The optimal basis matrix $\mathcal B$ is formed by the columns of $M$ indexed by $\mathcal M_+$ and the unit vectors $e_j$, $j \in \mathcal Q_+$.

The (SPP)-residual graph is $\mathcal G$ with the redundant matches removed, and the network is (SPP)-acyclic if it satisfies GP and its (SPP)-residual graph has no cycle.

Formalization targets

Goal: Theorem 5.1 (p. 25)

Assume GP and (SPP)-acyclicity. Then there are vectors $y^l \in \{-1,0,1\}^n$, $l \in \mathcal M_+ \cup \mathcal Q_+$, with

$$z^*_m = y^m\lambda > 0\ (m \in \mathcal M_+),\qquad s^*_j = y^j\lambda > 0\ (j \in \mathcal Q_+),$$

and every right-hand side $\tilde\lambda > 0$ with $y^l\tilde\lambda > 0$ for all $l$ has, as its unique optimal solution, $z_m = y^m\tilde\lambda$ on $\mathcal M_+$, $s_j = y^j\tilde\lambda$ on $\mathcal Q_+$, and zero elsewhere.

Milestones

1. (4), p. 20. Under GP, $\mathcal B$ is invertible and $(z^*_{\mathcal M_+}, s^*_{\mathcal Q_+}) = \mathcal B^{-1}\lambda > 0$.
2. §4.2, p. 20. Under GP the same basis remains optimal for every $\tilde\lambda > 0$ with $\|\tilde\lambda - \lambda\|_\infty \le \zeta_0$, for some $\zeta_0 > 0$.
3. Lemma C.1, p. 44. A connected acyclic matching network graph has at least $n - d + 1$ leaves; under GP with $\mathcal M_0 = \emptyset$ and a connected acyclic residual graph, $|\mathcal Q_+| = n - d$ and some over-demanded queue takes part in exactly one match.

A further theorem item, Lemma 5.1 (p. 24), states that under GP a network with only two-way matches, in which every cycle contains an even number of matches, is (SPP)-acyclic.

Significance

Theorem 5.1 turns the regret constant of the paper's main theorem into a quantity one can read off the data: every positive basic variable, and therefore $\epsilon$, is $\sum_i y_i\lambda_i$ with coefficients in $\{-1,0,1\}$. Its second sentence describes the whole region of right-hand sides on which the same basis stays optimal, an open polyhedral cone cut out by the inequalities $y^l\tilde\lambda > 0$, which is how the paper relates GP to the arrival rates in §5.1.

On the formal side, the mission builds a reusable model of the matching network, its bipartite incidence graph and the static-planning linear program with a variable right-hand side. Prove2Me does not yet contain the structural theory of optimal bases of such programs. Theorem 5.1 and its milestones are proved in the paper (Appendix C and §4.2); none of them is machine-checked yet.

Difficulty

The representation $z^* = \mathcal B^{-1}\lambda$ holds for every network in general position, so the content of the theorem lies in two places.

• The entries of $\mathcal B^{-1}$. Inverses of $0/1$ matrices have arbitrary rational entries in general: the triangle network (three types, matches $\{1,2\},\{2,3\},\{1,3\}$) has an optimal basis whose inverse has entries $\pm\tfrac12$. The claim needs the acyclic structure of the residual graph in an essential way.
• The second sentence. Exhibiting numbers $y^l$ with $y^l\lambda = z^*_l$ is trivial and says nothing. The statement requires the same vectors to produce the unique optimal solution for a whole open set of right-hand sides, which forces them to be the rows of $\mathcal B^{-1}$. This step therefore also involves the optimality conditions of (SPP) and the uniqueness part of GP.

Formalization scope

Types are Fin n, matches Fin d, both 0-based. The topology is the structure MatchingNetwork with the fields $|\mathcal A(m)| \ge 2$ and "every type is in a match"; $\lambda$ and $r$ are separate vectors with the standing predicates $\lambda_i > 0$, $\sum_i\lambda_i = 1$ and $r_m > 0$, which are hypotheses of every theorem. The optimal solution $(z^*, s^*)$ is an argument together with the GP hypothesis, never a default or a choice. The graph is a SimpleGraph on Fin n ⊕ Fin d; the residual graph keeps redundant matches as isolated vertices, which affects neither acyclicity nor the degrees of type vertices. The column index type of $\mathcal B$ is $\mathcal M_+ \sqcup \mathcal Q_+$, and the inverse is a two-sided inverse over these index types, not Matrix.inv, which is $0$ on singular matrices.

Conventions the statements commit to:

• in Theorem 5.1, "induces the optimal solution" is read as the unique optimal solution, and $\tilde\lambda$ is any positive vector, not necessarily summing to one;
• "for all sufficiently small $\zeta_0$" in milestone 2 is the existence of one $\zeta_0 > 0$;
• Lemma C.1's count of $n - d + 1$ leaves is stated without natural-number subtraction;
• Lemma C.1's second half carries the standing reduction of Appendix C ($\mathcal M_0 = \emptyset$, one connected component) as hypotheses;
• "every cycle contains an even number of matches" in Lemma 5.1 is stated as "every cycle of the bipartite graph has length divisible by 4".

The paper's own text says "all entries of $Y$ are either $-1$, $0$, or $-1$" (p. 25); this is read as $-1$, $0$ or $1$, as in the theorem's statement.

A formalization that keeps only the first sentence of Theorem 5.1, or that lets the vectors $y^l$ be unrelated to the basis, is trivially satisfiable and is not the theorem.

Needed infrastructure: optimality conditions for linear programs in equality form (reduced costs, uniqueness of a non-degenerate optimum), Mathlib's acyclic graphs and trees (SimpleGraph.IsAcyclic, IsTree.card_edgeFinset), and degree counting on bipartite graphs. The paper proves Theorem 5.1 in Appendix C by an explicit construction along paths of the residual graph; any correct argument is welcome. Lemmas on the inverse of a basis matrix whose bipartite row–column graph is a forest would be reusable well beyond this mission.

Selected references

• S. Kerimov, I. Ashlagi, I. Gurvich, Dynamic Matching: Characterizing and Achieving Constant Regret, SSRN 3824407 (version of September 14, 2022); Management Science (2023). https://ssrn.com/abstract=3824407, https://doi.org/10.1287/mnsc.2021.01215
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, §5.1 (sensitivity analysis of an optimal basis).

Motivation

Many problems in optimization reduce to a subgradient inclusion $0\in\partial\varphi(x)$: for a smooth $\varphi$ this is the gradient equation $\nabla\varphi(x)=0$, and for an extended-real-valued $\varphi=f+g$ (a smooth loss plus an indicator or a nonsmooth regularizer) it is the first-order optimality condition of a composite problem. Newton's method is the classical way to solve such equations with a superlinear rate, but its textbook form needs $\varphi\in C^2$ and a nonsingular Hessian. Khanh, Mordukhovich and Phat (arXiv:2009.10551v2, 2022; Mathematics of Operations Research, 2023) design a Newton-type method in which the Hessian is replaced by Mordukhovich's second-order subdifferential $\partial^2\varphi$, and prove local superlinear convergence under two assumptions that are weaker than the usual ones: metric regularity (instead of strong metric regularity or tilt stability) and the semismooth* property of Gfrerer and Outrata.

Timeline of the ingredients:

• 1996: Poliquin and Rockafellar introduce prox-regular functions and show that, for small parameters, their Moreau envelopes are $C^{1,1}$ near the reference point and their proximal mappings are single-valued and Lipschitz there (Trans. AMS 348).
• 2002: Klatte and Kummer develop Newton methods for Lipschitzian equations through generalized derivatives (Nonsmooth Equations in Optimization, Kluwer).
• 2021: Gfrerer and Outrata define semismooth* set-valued maps and a semismooth* Newton method (SIAM J. Optim. 31).
• 2021: Mordukhovich and Sarabi give a generalized Newton method for tilt-stable minimizers of prox-regular functions (SIAM J. Optim. 31).
• 2020/2022: Khanh, Mordukhovich and Phat replace tilt stability and strong metric regularity by metric regularity of $\partial\varphi$.

Setting

Let $\varphi:\mathbb R^n\to(-\infty,\infty]$ be proper. Its limiting subdifferential $\partial\varphi(x)$ collects the limits of Fréchet subgradients at points $x_k\to x$ with $\varphi(x_k)\to\varphi(x)$. For a set $\Omega$, the regular normal cone $\widehat N_\Omega(z)$ contains the vectors $a$ with $\langle a,w-z\rangle\le o(\|w-z\|)$ for $w\in\Omega$; the limiting normal cone $N_\Omega(z)$ contains the limits of regular normals at nearby points. For a set-valued $G$, the coderivative is $D^*G(x,y)(w)=\{u:(u,-w)\in N_{\operatorname{gph}G}(x,y)\}$, and the second-order subdifferential is $\partial^2\varphi(x,v)=D^*\partial\varphi(x,v)$.

The function $\varphi$ is prox-regular at $\bar x$ for $\bar v\in\partial\varphi(\bar x)$ with modulus $r>0$ if it is l.s.c. around $\bar x$ and, for some $\varepsilon>0$, $\varphi(x)\ge\varphi(u)+\langle v,x-u\rangle-\tfrac r2\|x-u\|^2$ whenever $x,u$ lie within $\varepsilon$ of $\bar x$, $|\varphi(u)-\varphi(\bar x)|<\varepsilon$ and $v\in\partial\varphi(u)$ lies within $\varepsilon$ of $\bar v$. It is continuously prox-regular if, in addition, $\varphi(x_k)\to\varphi(\bar x)$ along every $(x_k,v_k)\to(\bar x,\bar v)$ with $v_k\in\partial\varphi(x_k)$. It is prox-bounded if it is bounded below by a quadratic function.

For $\lambda>0$, the Moreau envelope and proximal mapping are

$$e_\lambda\varphi(x)=\inf_y\Big\{\varphi(y)+\tfrac1{2\lambda}\|y-x\|^2\Big\},\qquad \operatorname{Prox}_\lambda\varphi(x)=\operatorname*{argmin}_y\Big\{\varphi(y)+\tfrac1{2\lambda}\|y-x\|^2\Big\}.$$

Algorithm 6.2 starts at $x^0\in U_\lambda=\operatorname{rge}(I+\lambda\partial\varphi)$. While $0\notin\partial\varphi(x^k)$ it sets $v^k=\lambda^{-1}(x^k-\operatorname{Prox}_\lambda\varphi(x^k))$, picks any $d^k$ with $-v^k\in\partial^2\varphi(x^k-\lambda v^k,v^k)(\lambda v^k+d^k)$, and moves to $x^{k+1}=x^k+d^k$.

The standing assumptions at a solution $\bar x$ are:

• (H1) the inclusion $-v\in\partial^2\varphi(x,v)(d)$ is solvable for every $(x,v)\in\operatorname{gph}\partial\varphi$ near $(\bar x,0)$;
• (H2) $\partial\varphi$ is metrically regular around $(\bar x,0)$;
• (H3) $\partial\varphi$ is semismooth* at $(\bar x,0)$.

Formalization targets

Goal: Theorem 6.6 (corrected parameter range)

If $\varphi$ is proper, prox-bounded, continuously prox-regular at $\bar x$ for $0\in\partial\varphi(\bar x)$ with constants $r,\varepsilon$, and (H1)–(H3) hold, then

$$\exists\,\lambda_0\in(0,r^{-1}]\ \ \forall\lambda\in(0,\lambda_0)\ \ \exists\,U\in\mathcal N(\bar x),\ U\subseteq U_\lambda:\ \text{Algorithm 6.2 is well-defined from }U\text{ and every run from }U\text{ converges Q-superlinearly to }\bar x.$$

Milestones

• Lemma 5.4: for continuous $F$, metric regularity around $\bar x$ holds iff $\|v\|\ge c\|u\|$ for all $v\in D^*F(x)(u)$, $x$ near $\bar x$.
• Lemma 5.6: $D^*F(\bar x)(u_1+u_2)\subseteq D^*F(\bar x)(u_1)+D^*F(\bar x)(u_2)$ for locally Lipschitz $F$.
• Lemma 5.5: for $C^{1,1}$ $\varphi$, $\nabla\varphi$ is semismooth* at $\bar x$ iff $\nabla\varphi(x)-\nabla\varphi(\bar x)-\partial^2\varphi(x)(x-\bar x)\subseteq o(\|x-\bar x\|)$.
• Theorem 5.7: the $C^{1,1}$ Newton method (Algorithm 5.3) converges locally Q-superlinearly under (H1)–(H3) for $\nabla\varphi$.
• Lemma 6.3 (i)–(iii), corrected: near $\bar x+\lambda\bar v$, and for $\lambda$ small, $e_\lambda\varphi$ is $C^{1,1}$, $\operatorname{Prox}_\lambda\varphi$ is single-valued, monotone and Lipschitz, and $\nabla e_\lambda\varphi(x)=\lambda^{-1}(x-\operatorname{Prox}_\lambda\varphi(x))$.
• Lemma 6.4, corrected: $x^*\in D^*\nabla e_\lambda\varphi(x,v)(v^*)\iff x^*\in\partial^2\varphi(x-\lambda v,v)(v^*-\lambda x^*)$.
• Remark 6.5, corrected: the steps of Algorithm 6.2 are the steps of Algorithm 5.3 for $e_\lambda\varphi$.

Significance

The result gives a Newton method for nonsmooth, nonconvex subgradient inclusions whose convergence does not require strong metric regularity. Example 5.2 of the paper exhibits a $C^{1,1}$ function whose gradient is metrically regular and semismooth* but not strongly metrically regular, so the theorem covers solutions that earlier generalized Newton theories exclude. Through the Moreau envelope, the method reduces to a $C^{1,1}$ gradient equation; the same reduction, with the forward–backward envelope, drives the paper's composite algorithm (the companion mission) and its applications to Lasso-type problems.

The paper's results are proved on paper; none of them, nor the underlying theory of coderivatives, second-order subdifferentials or semismooth* maps, is formalized in Mathlib. This mission produces a machine-checked development of that layer and of the convergence theorem. It also fixes a defect: as printed, Lemma 6.3 and Theorem 6.6 claim their conclusions for every $\lambda\in(0,r^{-1})$, which is false (see Formalization scope); the formal statements are the corrected ones.

Difficulty

The obvious argument says "Algorithm 6.2 is Algorithm 5.3 for $e_\lambda\varphi$, so apply Theorem 5.7". Each step of that sentence carries the difficulty. Transferring (H1)–(H3) from $\partial\varphi$ to $\nabla e_\lambda\varphi$ requires the coderivative of the inverse $(\lambda I+\partial\varphi^{-1})^{-1}$, which needs a local graphical calculus for limiting normals that Mathlib does not have. The $C^{1,1}$ property of the envelope and single-valuedness of the proximal map hold only for small $\lambda$ and near $\bar x+\lambda\bar v$: prox-regularity is local while $\operatorname{Prox}_\lambda\varphi$ minimizes globally, so a far-away deep well can capture the proximal point. Theorem 5.7 itself rests on a uniform coderivative bound from metric regularity (Lemma 5.4, a pointwise-to-uniform form of the Mordukhovich coderivative criterion) and on the semismooth* estimate (Lemma 5.5), which combines directional normal cones with the symmetry of generalized Hessians.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n); definitions are stated on real inner product spaces, and $E\times F$ carries the sup norm (the cones are norm-independent).
• $\partial$ is the published analytic limiting subdifferential NonconvexSplitting.Shared.LimitingSubdiff. It agrees with the paper's geometric (2.9) for functions l.s.c. around the point, which covers every function $\partial$ is applied to here.
• $\varphi$ takes values in EReal and is assumed proper; the envelope is EReal-valued, and finiteness is asserted wherever it is differentiated.
• $\operatorname{Prox}_\lambda\varphi(x)$ is the argmin set. A run of an algorithm selects any proximal point and any direction solving the Newton inclusion. The stop of Step 1 is a constant tail. Well-definedness means every partial run from $U$ can be continued.
• Metric regularity uses $\operatorname{dist}(\cdot;\emptyset)=+\infty$. Q-superlinear convergence is stated in $\varepsilon$-form, avoiding $0/0$. $C^{1,1}$ is local to a neighbourhood.
• Correction. Lemma 6.3, Lemma 6.4, Remark 6.5 and Theorem 6.6 are posed as "there is $\lambda_0\in(0,r^{-1}]$ such that for every $\lambda\in(0,\lambda_0)$", on neighbourhoods instead of $U_\lambda$. As printed they fail for $\varphi(y)=\tfrac12y^2$ on $[-5,5]$, $-1000-|y-10|$ on $[9,11]$, $+\infty$ elsewhere, with $\bar x=0$, $r=1$, $\lambda=\tfrac12$: there $\operatorname{Prox}_\lambda\varphi(x)=\{9\}$ near $0$, and Algorithm 6.2 jumps to the stationary point $9$. Lemmas 5.4–5.6 and Theorem 5.7 are posed as printed.
• Trivializing formalizations are ruled out: $\lambda_0>0$ is part of the conclusion, so the $\forall\lambda$ is never vacuous; conclusions hold for every run rather than for a run chosen by Classical.choose; and $\varphi$ is not specialized (no convexity, which would make $U_\lambda=\mathbb R^n$; no $C^2$; no strong metric regularity; no assumption that $\bar x$ is a minimizer).
• Reusable infrastructure: normal cones to graphs, limiting and directional coderivatives, metric regularity, semismooth*, prox-regularity, Moreau envelopes. Formalizations of Mordukhovich's coderivative criterion, of the scalarization formula $D^*F(\bar x)(u)=\partial\langle u,F\rangle(\bar x)$ for Lipschitz $F$, and of Poliquin–Rockafellar's Theorem 4.4 are especially welcome.

Selected references

• P. D. Khanh, B. S. Mordukhovich, V. T. Phat, A Generalized Newton Method for Subgradient Systems, arXiv:2009.10551v2, 2022; Math. Oper. Res., 2023. https://arxiv.org/abs/2009.10551
• R. A. Poliquin, R. T. Rockafellar, Prox-regular functions in variational analysis, Trans. Amer. Math. Soc. 348, 1996. https://doi.org/10.1090/S0002-9947-96-01544-9
• H. Gfrerer, J. V. Outrata, On a semismooth Newton method for solving generalized equations*, SIAM J. Optim. 31, 2021. https://doi.org/10.1137/19M1257408
• B. S. Mordukhovich, M. E. Sarabi, Generalized Newton algorithms for tilt-stable minimizers in nonsmooth optimization, SIAM J. Optim. 31, 2021. https://doi.org/10.1137/20M1329937
• B. S. Mordukhovich, Variational Analysis and Generalized Differentiation I, Springer, 2006. https://doi.org/10.1007/3-540-31247-1
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3