Missions · Prove2Me

Completed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

Guarantees in Fair Division: General or Monotone Preferences 2: For Monotone Preferences the Moving Knife Guarantee Lies Between minMax and Maxmin and the Bid & Choose Guarantee Is at Most MaxminResearch Paper

Motivation

Fair division asks how to split a divisible resource among $n$ agents whose preferences differ. In the non-atomic ("cake-cutting") model the resource is a region of Euclidean space and an agent values each measurable piece. Bogomolnaia and Moulin (arXiv:1911.10009, Mathematics of Operations Research, 2023) study fair guarantees: utility levels that a division rule lets every agent secure for herself, whatever the other agents' preferences and behaviour. Two numbers bracket every such guarantee. Maxmin is an upper bound on any fair guarantee, and minMax is what Kuhn's Divide & Choose rule secures for arbitrary continuous preferences (Theorem 1 of the paper; a companion mission formalizes it).

For utilities that are monotone in the share (the manna is unanimously good), the authors ask whether rules of a different shape improve on minMax. They consider the classical Moving Knife rules, where a knife sweeps the manna and agents shout "stop", and introduce Bid & Choose rules, where a clock runs and the agent who stops it picks any share of a prescribed size. Each rule comes with a computable guarantee, $\Gamma^\kappa$ for the knife and $\Gamma^\theta$ for Bid & Choose. The question this mission formalizes is where these guarantees sit relative to the two benchmarks.

Setting

The manna $\Omega$ is a bounded measurable subset of $\mathbb R^d$ , $d\ge1$ , with Lebesgue measure $|\cdot|$ and $|\Omega|>0$ . A share is a measurable $S\subseteq\Omega$ . Shares are compared by the pseudo-metric $\delta(S,T)=|S\,\triangle\,T|$ . A utility $u\in\mathcal D(\Omega)$ is a bounded, $\delta$ -continuous function on shares with $u(\emptyset)=0$ ; it lies in $\mathcal M^+(\Omega)$ if $S\subseteq T$ implies $u(S)\le u(T)$ .

An $n$ -partition of $\Omega$ is a tuple of shares $(S_i)_{i=1}^n$ with union $\Omega$ and pairwise null overlaps; it is an equipartition for $u$ if all $u(S_i)$ are equal. The benchmarks are

\mathit{minMax}(u;n)=\inf_{\Pi}\max_i u(S_i),\qquad \mathit{Maxmin}(u;n)=\sup_{\Pi}\min_i u(S_i),

over all $n$ -partitions $\Pi$ .

A moving knife $\kappa$ is a $\delta$ -continuous path $t\mapsto K(t)$ of shares on $[0,1]$ from $K(0)=\emptyset$ to $K(1)=\Omega$ with $|K(t')\setminus K(t)|>0$ whenever $t<t'$ . A benchmark measure $\theta$ is a probability measure on $\Omega$ , mutually absolutely continuous with Lebesgue measure on $\Omega$ . Write $\Upsilon(n)$ for the sequences $0=t^0\le t^1\le\dots\le t^n=1$ , and

u^\kappa(t^1,t^2)=u\big(K(t^2)\setminus K(t^1)\big),\qquad u^\theta(t^1,t^2)=\inf_{T:\,\theta(T)=t^1}\ \sup_{S:\,S\cap T=\emptyset,\ \theta(S)=t^2-t^1}u(S).

For $\alpha\in\{\kappa,\theta\}$ the guarantees are

\Gamma^\alpha(u;n)=\sup_{\tau\in\Upsilon(n)}\ \min_{0\le k\le n-1}u^\alpha(t^k,t^{k+1}).

Formalization targets

Goal: Theorem 2 iii), the provable part

For $n\ge1$ , $u\in\mathcal D(\Omega)\cap\mathcal M^+(\Omega)$ , every moving knife $\kappa$ and every benchmark measure $\theta$ :

\mathit{minMax}(u;n)\le\Gamma^\kappa(u;n)\le\mathit{Maxmin}(u;n),\qquad \Gamma^\theta(u;n)\le\mathit{Maxmin}(u;n).

The paper also claims $\mathit{minMax}(u;n)\le\Gamma^\theta(u;n)$ . That inequality is false and is not posed. Take $\Omega=[0,1]$ , $\theta$ Lebesgue measure and $n=2$ . There is an increasing continuous $u$ , built from dyadic "spike" sets, for which $\Gamma^\theta(u;2)\le0.075$ while every 2-partition has a share worth about $0.9$ .

Milestones

$u^\kappa$ and $u^\theta$ decrease weakly in $t^1$ and increase weakly in $t^2$ (p. 19).
Lemma 4 i), knife part: $u^\kappa$ is continuous on the triangle $0\le t^1\le t^2\le1$ .
Lemma 4 ii), knife part: $\Gamma^\kappa(u;n)$ is attained at a $\tau\in\Upsilon(n)$ equalising all $u^\kappa(t^k,t^{k+1})$ .
An equalising knife sequence cuts $\Omega$ into an $n$ -equipartition (proof of Theorem 2).
The trimming step and Proposition 1 ii): for $u\in\mathcal M^+(\Omega)$ , minMax and Maxmin are the infimum and supremum of equipartition utilities.
For every $\tau\in\Upsilon(n)$ , $\min_k u^\theta(t^k,t^{k+1})\le\mathit{Maxmin}(u;n)$ (p. 20).

A further item records what the page's left-hand argument for $\theta$ does prove: $\mathit{minMax}(u;n)\le\max_k u^\theta(t^k,t^{k+1})$ for every $\tau\in\Upsilon(n)$ .

Significance

The goal shows that, for a good manna, a Moving Knife rule is never worse than Divide & Choose by the minMax measure and never promises more than the Maxmin ceiling. Bid & Choose likewise never exceeds Maxmin. Since Maxmin profiles need not be feasible (the paper's Leontief example, p. 16), these inequalities locate the new guarantees inside the only interval where fair guarantees can live.

The mission also corrects the record. The paper is published, but its Lemma 4 and Theorem 2 iii) as printed in the arXiv v3 preprint are not right for $\theta$ . Lemma 4 i) asserts continuity of $u^\theta$ and Lemma 4 ii) the existence of an equalising $\theta$ -sequence, and both fail for some $u\in\mathcal M^+([0,1])$ . The left-hand θ-inequality fails as well. The mission states only true claims and leaves precise statements on record. As far as we know none of these results has been machine-checked. The platform has no prior cake-cutting, moving-knife or equipartition development, so the definitions here are new.

Difficulty

The knife sandwich hinges on an equalising sequence. One must show that $u^\kappa$ is jointly continuous and run an $n$ -step intermediate value argument whose optimality proof needs the two-sided monotonicity of $u^\kappa$ . Proposition 1 ii) needs the trimming step. A share must be continuously shrunk inside $\mathbb R^d$ while its utility is tracked, and then iterated across $n$ shares while all trimmed shares are kept equal. This is the longest argument in the mission.

For $\theta$ , the natural first idea is to copy the knife argument: prove $u^\theta$ continuous, then equalise. It fails, because $u^\theta$ is an inf–sup over the non-compact space of shares and can jump. The right-hand inequality has to hold for every $\tau$ without any attainment, and any argument for it requires shares of every prescribed $\theta$ -size, i.e. a non-atomicity (Sierpiński-type) argument for $\theta$ .

Formalization scope

Space: EuclideanSpace ℝ (Fin d) with volume, and $d\ge1$ is assumed in every theorem, because in $\mathbb R^0$ Lebesgue measure is a point mass, which the paper's non-atomic model excludes. Utilities are functions on all subsets, constrained on shares only. Partitions are Fin n-indexed, with union exactly $\Omega$ and null pairwise overlaps (not disjointness). Every min/max of the paper is an inf/sup (sInf, sSup), as the paper itself says on p. 9. Each defining set is nonempty and bounded for $n\ge1$ , which every theorem assumes. Knife continuity is $\varepsilon$ – $\eta$ continuity for $\delta$ on $[0,1]$ . $\theta$ is mutually absolutely continuous with volume.restrict Ω, with $\theta(\Omega)=1$ . $u^\theta$ quantifies over shares $S,T$ , with exact disjointness and exact $\theta$ -sizes. Only $\mathcal M^+(\Omega)$ is treated, as Theorem 2 states.

Ruled out: $\Gamma$ as a supremum over a possibly empty set, an inner supremum in $u^\theta$ over arbitrary sets, the sandwich without monotonicity of $u$ , a single rule in place of both, and $\Gamma^\alpha$ replaced by its value at one particular $\tau$ . None of these is the paper's statement, and some are trivially true.

Needed infrastructure: δ-continuity of set-valued paths, existence of measurable subsets of prescribed measure for non-atomic measures on $\mathbb R^d$ , and intermediate-value arguments in several variables. The model definitions are reusable for any non-atomic fair-division development. Proofs of any item are welcome, as are formal versions of the counterexamples to the θ claims.

Selected references

A. Bogomolnaia, H. Moulin, Guarantees in Fair Division: General or Monotone Preferences, Mathematics of Operations Research, 2023; preprint arXiv:1911.10009v3, 2020. https://arxiv.org/abs/1911.10009
S. Avvakumov, R. Karasev, Envy-free Division under Mapping Degree, 2019. https://arxiv.org/abs/1907.11183

10 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Load Balancing Under Strict Compatibility Constraints 1: On Proportionally Sparse Subcritical Compatibility Graphs, JSQ(d) Has the Fully Flexible Mean-Field Limit and Steady StateResearch Paper

Motivation

In large server farms and cloud platforms, not every server can process every task. Data locality, licences, hardware and security rules restrict each task type to a subset of servers. Such compatibility constraints are modelled by a bipartite compatibility graph between task types (dispatchers) and servers. Classical mean-field results for load balancing, such as Mitzenmacher's analysis of the power of $d$ choices (Mitzenmacher 2001) and Vvedenskaya, Dobrushin and Karpelevich's supermarket model (1996), assume full flexibility: every task may join every server. Rutten and Mukherjee (arXiv:2008.07562, Math. Oper. Res. 2023) identify graph conditions under which JSQ( $d$ ) on a sparse compatibility graph behaves, in the large-system limit, exactly like the fully flexible system. This holds both on finite time intervals and in steady state.

Related work includes Budhiraja, Mukherjee and Wu (2019), on the supermarket model on graphs whose vertices are servers; Mukherjee, Borst, van Leeuwaarden and Whiting (2018), on the universality of power-of- $d$ schemes; and Bramson (2011) and Cardinaels, Borst and van Leeuwaarden (2019), on the stability of JSQ-type policies under compatibility constraints.

Setting

There are $N$ servers $V_N$ and $M(N)\ge1$ dispatchers $W_N$ , with an edge set $E_N\subseteq V_N\times W_N$ . Dispatcher $w$ can only send tasks to its neighbourhood $\mathcal N_w=\{v:(v,w)\in E_N\}$ .

Tasks arrive at each dispatcher as independent Poisson streams of rate $\lambda N/M(N)$ , with $0<\lambda<1$ .
Each server has its own infinite-buffer queue with unit-mean exponential services.
Under JSQ( $d$ ), $d\ge2$ , an arriving task at $w$ samples $\min(d,|\mathcal N_w|)$ servers of $\mathcal N_w$ uniformly at random, without replacement, and joins a shortest of their queues. Ties are broken uniformly at random.

The state $\Phi(G_N,t)\in\mathbb N^{V_N}$ is the vector of queue lengths. Two statistics of a state $z$ are used:

the occupancy $q_i(z)=|\{v:z_v\ge i\}|/N$ ;
the local empirical distribution $x^w_i(z)=|\{v\in\mathcal N_w:z_v=i\}|/|\mathcal N_w|$ .

Occupancies live in $\mathcal Y=\{q\in\ell_1:q_i\in[0,1],\ q_i\ge q_j\text{ for }i<j\}$ .

The sequence $\{G_N\}$ is proportionally sparse if for every $\varepsilon>0$

\sup_{U\subseteq V_N}\frac1{M(N)}\Big|\Big\{w:\Big|\frac{|\mathcal N_w\cap U|}{|\mathcal N_w|}-\frac{|U|}{N}\Big|\ge\varepsilon\Big\}\Big|\to0 .

Put $k_w=\min(d,|\mathcal N_w|)$ . The sequence is subcritical if there are probability distributions $\gamma^U_w$ on the sampled sets $U$ with

\limsup_{N\to\infty}\max_{v}\frac{N}{M(N)}\sum_w\binom{|\mathcal N_w|}{k_w}^{-1}\sum_{U\subseteq\mathcal N_w,\,|U|=k_w}\gamma^U_w(v)\le1 .

This bounds the load that a static randomised routing would put on any server.

The fully flexible mean-field limit is the system of ODEs

\frac{dq^*_i}{dt}=\lambda\big((q^*_{i-1})^d-(q^*_i)^d\big)-(q^*_i-q^*_{i+1}),\qquad i\ge1,\quad q^*_0\equiv1,\qquad(3.3)

whose fixed point is $q^*_i(\infty)=\lambda^{(d^i-1)/(d-1)}$ .

Formalization targets

Goal: Theorem 3.4

Let $\{G_N\}$ be proportionally sparse and connected, and suppose $q^*(0)\in\mathcal Y$ with $\|q(\Phi(G_N,0))-q^*(0)\|_1\to0$ . Then, for every $T\ge0$ and $\varepsilon>0$ ,

P\Big(\sup_{t\le T}\|q(\Phi(G_N,t))-q^*(t)\|_1\ge\varepsilon\Big)\to0 .

If moreover $\{G_N\}$ is subcritical, then for all large $N$ the chain has a unique stationary distribution $\pi_N$ , and $\pi_N(\|q-q^*(\infty)\|_1\ge\varepsilon)\to0$ .

Milestones, in the order the proof uses them

Lemma 4.2: the JSQ( $d$ ) assignment function is Lipschitz.
Lemma F.1 and Proposition 4.5: on proportionally sparse graphs, local and global empirical distributions agree for almost all dispatchers, uniformly on $[0,T]$ .
Proposition 4.7: under the optimal coupling, the occupancy distance to the fully flexible system is at most twice the number of routing mismatches.
Theorem 4.3: the process-level limit for Lipschitz policies.
Lemmas H.2, H.4, H.5 and Theorem 4.8(i): Foster–Lyapunov stability for all large $N$ .
Lemmas 4.9, 4.10 and Theorem 4.8(ii): tightness of the steady states in a weighted $\ell_1$ space.
Theorem 4.11: exponential global stability of (3.3) in that weighted norm.

Significance

The result. The theorem separates two graph properties.

Proportional sparsity is an expansion property; it alone makes the transient dynamics universal.
Subcriticality is a capacity condition; it alone gives stability and tightness of the stationary distributions.

Together they justify using the fully flexible ODE (3.3) and its fixed point for the stationary performance of a constrained system. Companion results (Theorems 3.5 and 3.6, formalized in missions 2 and 3 of this series) show that random graphs with degrees growing only slightly faster than logarithmically satisfy both conditions, so the flexibility needed for full mean-field performance is far smaller than complete flexibility.

Formalizing it. The result is proved on paper but has no machine-checked proof. A formalization would produce the following.

A reusable model of a continuous-time Markov chain with bounded rates, realised by uniformisation.
Foster–Lyapunov and petite-set arguments on a countable state space.
A pathwise coupling bound.
A tightness criterion in weighted $\ell_1$ .
An interchange-of-limits argument.

The global stability of (3.3) relies on Mitzenmacher's weighted-potential theorem, which is posed separately on the platform (PowerTwoChoices.Limit.theorem_3) and is open.

Difficulty

The obvious argument couples the system on $G_N$ with the fully flexible system server by server. This fails because a task arriving at $w$ can only join $\mathcal N_w$ , so the two systems cannot place it at the same server. The paper instead couples the queue lengths chosen and counts mismatches. That bound is only useful if almost every dispatcher sees a local queue-length distribution close to the global one at all times. The set of good dispatchers changes with the state, and controlling it requires a uniform bound over all subsets of servers.

A second gap concerns the goal itself. Theorem 4.3 covers policies that depend only on the local empirical distribution. JSQ( $d$ ) without replacement also depends on $|\mathcal N_w|$ when neighbourhoods are small, so deducing the goal from Theorem 4.3 needs an approximation step that the paper does not spell out.

For the steady state, subcriticality bounds a $\limsup$ only, so stability holds for large $N$ and not for every $N$ . Tightness in a fixed $\ell_1$ -ball does not suffice: the limit is identified through a stability result that holds in a weighted norm with geometrically growing weights. The tightness has to be proved in that norm, through moment bounds on stationary tails.

Formalization scope

Graphs. Servers are Fin N, dispatchers Fin (M N) with $M(N)\ge1$ , and edges a Finset. Connectivity is a separate hypothesis (Definition 3.1 and §2). Proportional sparsity is the limit condition (3.1). In subcriticality the normaliser is $\binom{|\mathcal N_w|}{k_w}$ , and the distributions $\gamma^U_w$ are constrained only for nonempty $U$ . Both choices agree with the paper whenever $|\mathcal N_w|\ge d$ .
Dynamics. The process is the uniformised chain with kernel lbKernel, run at the epochs of an independent Poisson clock of rate $(\lambda+1)N$ . Statements quantify over every realisation on every probability space, for $N\ge1$ . JSQ( $d$ ) samples without replacement; with replacement, Theorem 4.8 is false under Definition 3.3.
Occupancy. The occupancy is indexed from $0$ with $q_0=1$ , and $\ell_1$ distances are l1dist in $[0,\infty]$ . "Converges weakly" to a deterministic limit is rendered as convergence in probability. Ergodicity is rendered as existence and uniqueness of a stationary distribution.
Repairs to the printed text. The printed (3.4) exponent $(d^i-d)/(d-1)$ is corrected to $(d^i-1)/(d-1)$ ; with the printed value the steady-state claim is false. "For each fixed $N$ , ergodic" becomes "for all $N\ge N_0$ ".
Ruled out. A rendering in which the hypotheses cannot all hold would make the statements vacuous. Every routing law here sums to one and every clock rate is positive, so neither the process hypotheses nor the ODE hypothesis are vacuous. The conclusion asserts the existence of the stationary distributions it then speaks about.
Reused definitions. PowerTwoChoices.Limit.SupermarketSystem (the ODE, fixed point and potential) and PowerOfDUniversality.Fluid.FluidSpace (l1dist, supDistL1).
Generic and reusable. The Markov-chain notions in CountableChain: stationarity, $n$ -step kernels, petite sets and uniformisation.

Contributions to any milestone are welcome. Lemma 4.2, Proposition 4.7 and Lemma H.4 are self-contained.

Selected references

D. Rutten, D. Mukherjee, Load Balancing Under Strict Compatibility Constraints, Math. Oper. Res. (2023); preprint arXiv:2008.07562v2 (cited version). https://arxiv.org/abs/2008.07562
M. Mitzenmacher, The Power of Two Choices in Randomized Load Balancing, IEEE Trans. Parallel Distrib. Syst. 12 (2001). https://doi.org/10.1109/71.963420
N. D. Vvedenskaya, R. L. Dobrushin, F. I. Karpelevich, Queueing system with selection of the shortest of two queues: an asymptotic approach, Probl. Inf. Transm. 32 (1996).
D. Mukherjee, S. C. Borst, J. S. H. van Leeuwaarden, P. A. Whiting, Universality of power-of-d load balancing in many-server systems, Stochastic Systems 8 (2018). https://arxiv.org/abs/1612.00723
M. Bramson, Stability of join the shortest queue networks, Ann. Appl. Probab. 21(4):1568–1625 (2011).
A. Budhiraja, D. Mukherjee, R. Wu, Supermarket model on graphs, Ann. Appl. Probab. 29(3):1740–1777 (2019).
E. Cardinaels, S. C. Borst, J. S. H. van Leeuwaarden, Job assignment in large-scale service systems with affinity relations, Queueing Syst. 93:227–268 (2019).
S. P. Meyn, R. L. Tweedie, Markov Chains and Stochastic Stability, Springer (1993).

22 thms2 active usersReviewed

Completed

Combinatorics Linear Optimization Operations Research+1·Captain: mikedeng1

Online Stochastic Max-Weight Bipartite Matching: Beyond Prophet Inequalities: Rounding LP-Match Online Earns 0.51 of the Optimal Online AlgorithmResearch Paper

Motivation

Ride hailing, online advertising and kidney exchange share a decision problem: resources that are present from the start must be matched, irrevocably and one at a time, to requests that arrive at random. When the arrival probabilities are known in advance, the natural benchmark for an online algorithm is not the offline optimum (the "prophet", who sees every arrival in advance) but the optimal online algorithm: the best expected profit any algorithm can earn when it must decide without seeing the future. That benchmark is well defined and computable in exponential time, so the question becomes one of approximation algorithms: how much of it can a polynomial-time algorithm guarantee?

Papadimitriou, Pollner, Saberi and Wajc (arXiv:2102.10261, Math. Oper. Res. 2024) answer both halves of that question for online Bayesian bipartite matching. They show that approximating the optimal online algorithm within some constant $\alpha<1$ is PSPACE-hard (Theorem 1.1, not part of this mission), and they give a polynomial-time algorithm that earns a $0.51$ fraction of it (Theorem 1.2). The number matters because $1/2$ is the best possible ratio against the prophet, already for a single bin, so $0.51$ shows that comparing with the online optimum genuinely permits better guarantees.

Timeline:

1978: Krengel and Sucheston's prophet inequality: for a single item, no online algorithm earns more than $1/2$ of the offline optimum in the worst case, and $1/2$ is achievable.
2015–2020: $1/2$ -competitive algorithms against the offline optimum for unit-demand combinatorial auctions (Feldman, Gravin and Lucier, SODA 2015) and for online stochastic max-weight matching with vertex arrivals (Ezra, Feldman, Gravin and Tang, EC 2020).
2017: Torrico and Toriello's LP relaxations for online bipartite matching (arXiv:1709.01557), which imply that LP-Match bounds the optimal online algorithm (Lemma 4.1 here).
2021: this paper, $0.51$ of the online optimum by rounding LP-Match online.
2021: Saberi and Wajc's online edge-colouring algorithm (ICALP 2021), whose ideas improve the ratio of Theorem 1.2 to $0.526$ (as reported on p. 4 of the paper).

Setting

A RideHail instance $I$ has a finite set of bins (taxis) $i$ and balls (passengers) $t=1,\dots,n$ , revealed in this fixed order. Ball $t$ arrives with probability $p_t\in[0,1]$ , independently of every other ball. If it arrives it may be matched, irrevocably and before ball $t+1$ is revealed, to an unmatched bin $i$ , earning $w_{i,t}\ge 0$ . A deterministic online policy chooses the bin for ball $t$ as a function of the arrivals of balls $1,\dots,t$ only. Its expected profit is the average, over the $2^n$ arrival patterns, of the total weight of the matching it builds, and $\mathrm{OPT}_{on}(I)$ is the largest expected profit over all such policies.

LP-Match is the linear program in variables $x_{i,t}$ , read as "the probability that the algorithm matches $t$ to $i$ ":

\max \sum_{i,t} w_{i,t}x_{i,t}\ \ \text{s.t.}\ \ \sum_t x_{i,t}\le 1,\ \ \sum_i x_{i,t}\le p_t,\ \ x_{i,t}\le p_t\Big(1-\sum_{t'<t}x_{i,t'}\Big),\ \ x_{i,t}\ge 0.

Its optimal value is $\mathrm{LP\text{-}Match}(I)$ . The third family of constraints, (11), holds for online algorithms only.

Algorithm 1 (Rounding LP-Match Online), with $c=0.01$ , takes an optimal solution $x$ of LP-Match, adds a weight-zero dummy bin for each ball so that $\sum_i x_{i,t}=p_t$ , and then processes the balls in order. When ball $t$ arrives it picks a bin $i$ with probability $x_{i,t}/p_t$ . If $i$ is vacant, $(i,t)$ is matched with probability

q_{i,t}=\min\Big(1,\ \frac{1/2+c}{1-\sum_{t'<t}x_{i,t'}(1/2+c)}\Big).

If $t$ is still unmatched, it picks again from the same distribution, and is matched to the new pick when that bin is vacant and $\sum_{t'<t}x_{i,t'}>\frac{1/2-c}{1/2+c}$ . Edges added by the first pick form $M_1$ , those added by the second pick form $M_2$ , and $M=M_1\sqcup M_2$ .

Formalization targets

Goal: Theorem 1.2

For every instance $I$ and every optimal solution $x$ of LP-Match,

\mathbb E\Big[\sum_{(i,t)\in M}w_{i,t}\Big]\ \ge\ 0.51\cdot \mathrm{OPT}_{on}(I),

where $M$ is the output of Algorithm 1 run on $x$ .

The path

The milestones follow the paper's proof. LP-Match is a relaxation of the online problem (Lemma 4.1). Algorithm 1 matches every edge with probability at least $x_{i,t}(1/2+c)$ (Theorem 4.2), which rests on two bounds:

the first-pick analysis, Lemma 4.4 with the vacancy bounds of Corollary 4.5;
the second-pick bound, Theorem 4.6. It uses Equation (20), Lemma 4.7, the covariance bound of Lemma 4.8 and the conditioning bound of Lemma 4.11.

Lemma 4.8 comes from the negative association of early-occupancy indicators: Lemma 4.9 and Corollary 4.10, resting on Definition 2.5 and Propositions 2.6–2.8.

Significance

The result. Theorem 1.2 is the first polynomial-time algorithm for online stochastic matching with a ratio above $1/2$ against the optimal online algorithm. It separates the online benchmark from the prophet benchmark in an algorithmic sense, and its main technical step, bounding positive correlation between bins' matched statuses through negative association, has been reused for online edge colouring.

Formalizing it. The result is proved on paper and is not machine-checked anywhere. The mission produces:

a formal model of online Bayesian matching, with the optimal online policy as a benchmark;
a formal LP relaxation and its validity for online policies;
a formal statement of a randomized online rounding scheme and its per-edge guarantee.

The negative-association layer (Definition 2.5, Propositions 2.6–2.8) is general probability, absent from Mathlib, and reusable well beyond this mission.

Difficulty

The obvious argument fails at the second pick. Once ball $t$ has been rejected by its first pick, the events "bin $i$ is vacant" and "the first pick was rejected" are dependent, for two reasons:

The second pick may re-draw the very bin that just rejected.
Bins' occupancy statuses may be positively correlated, so a rejection by one bin makes the others likely occupied too.

Either effect alone can make the second pick useless. The first is controlled by Constraint (11) (Lemma 4.7). The second needs a quantitative bound on the covariance of vacancy indicators (Lemma 4.8), proved by splitting occupancy into early and late parts and showing that the early parts are negatively associated, through a coupling of the algorithm's randomness with independent pick and coin variables. Lemma 4.1 is also not routine to formalize: it requires turning an arbitrary history-dependent online policy into a feasible LP solution, using the independence of arrivals from past decisions.

Formalization scope

Conventions committed to in Lean (namespace OnlineMaxWeightMatch.Approx):

Bins form a finite type ι; balls are Fin n in arrival order (paper ball $t$ is index $t-1$ ). Weights and probabilities are real numbers with $w\ge 0$ and $0\le p_t\le 1$ ; missing edges have weight $0$ .
$\mathrm{OPT}_{on}(I)$ is the supremum over deterministic non-anticipating policies: the choice for ball $t$ is a function of the arrival indicators of balls $s\le t$ . Randomized online algorithms are mixtures of these and add nothing. Policies never see later arrivals; comparing against the prophet would make the goal false.
$\mathrm{LP\text{-}Match}(I)$ is the supremum of the objective over the feasible set (9)–(12), which is nonempty and compact.
Algorithm 1's randomness is a finite product space: for each ball, an arrival bit, a first pick, one acceptance coin per bin and a second pick, all independent. $M$ , $M_1$ , $M_2$ are computed from an outcome by recursion over the balls.
Picks are Option-valued: "no bin" carries the leftover mass $1-\sum_i x_{i,t}/p_t$ . When $p_t=0$ , $x_{i,t}/p_t$ is $0$ in Lean and the ball never arrives.
Dummy bins are genuine bins of type ι ⊕ Fin n with weight $0$ . A dummy first pick is accepted with probability $1/2+c$ and consumes the ball's turn, as in the paper. A dummy is never matched as a second pick.
$c$ is the fixed constant $1/100$ , not a parameter.
The milestones are stated for any LP-Match-feasible $x$ with $\sum_i x_{i,t}=p_t$ (the paper's standing assumption); the goal does the augmentation and assumes optimality only.
Conditional probabilities use ProbabilityTheory.cond, which is $0$ on null events. Equation (20) and Lemma 4.7 therefore carry positivity hypotheses ( $x_{j,t}>0$ , $p_t>0$ ) that make the conditioning event non-null.
Negative association uses bounded, measurable, non-decreasing test functions; covariances are ProbabilityTheory.covariance.

"Polynomial time" is not formalized. Because "some online algorithm earns $0.51\cdot\mathrm{OPT}_{on}$ " is trivially true of the optimal online algorithm itself, the goal names Algorithm 1 run on an arbitrary optimal LP-Match solution. That solution exists, so the goal is not vacuous. Replacing $\mathrm{OPT}_{on}$ by an offline benchmark, dropping Constraint (11), restricting to non-adaptive policies, or treating the dummy pick as "pick nothing" would each change the theorem.

Infrastructure a complete development needs: negative association with its closure properties, finite product probability spaces, conditioning on events, covariance of indicators, and linear-programming feasibility arguments for online policies. Contributions to any milestone are welcome; the probability layer (Propositions 2.6–2.8) is independent of the rest.

Selected references

C. Papadimitriou, T. Pollner, A. Saberi, D. Wajc, Online Stochastic Max-Weight Bipartite Matching: Beyond Prophet Inequalities, arXiv:2102.10261v3 (2021); Mathematics of Operations Research (2024). https://arxiv.org/abs/2102.10261
K. Joag-Dev, F. Proschan, Negative Association of Random Variables, with Applications, Annals of Statistics 11(1):286–295, 1983. https://doi.org/10.1214/aos/1176346079
D. Dubhashi, D. Ranjan, Balls and Bins: A Study in Negative Dependence, BRICS Report Series 3(25), 1996; Random Structures & Algorithms 13(2), 1998. https://doi.org/10.1002/(SICI)1098-2418(199809)13:2<99::AID-RSA1>3.0.CO;2-M
A. Torrico, A. Toriello, Dynamic Relaxations for Online Bipartite Matching, arXiv:1709.01557, 2017. https://arxiv.org/abs/1709.01557
T. Ezra, M. Feldman, N. Gravin, Z. G. Tang, Online Stochastic Max-Weight Matching: Prophet Inequality for Vertex and Edge Arrival Models, EC 2020. https://doi.org/10.1145/3391403.3399513
A. Saberi, D. Wajc, The Greedy Algorithm Is Not Optimal for On-Line Edge Coloring, ICALP 2021. https://doi.org/10.4230/LIPIcs.ICALP.2021.109

21 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

Linear Programming and Community Detection 1: Minimum Bisection Recovers the Planted Bisection When d_in − d_out > n/4 − 1Research Paper

Motivation

Community detection asks for a partition of the vertices of a graph into groups that are densely connected inside and sparsely connected across. In its simplest form there are two communities of equal size, and the natural combinatorial formulation is the minimum bisection problem: among all ways of splitting the vertex set into two halves, find one that cuts the fewest edges. The problem is NP-hard in general, yet on graphs that genuinely contain two well-separated communities one expects it to return exactly those communities. For the two-community stochastic block model, minimum bisection is the maximum a posteriori estimator, so understanding when it returns the hidden partition is the baseline against which convex relaxations are compared.

Del Pia, Khajavirad and Kunisky (arXiv:2006.03213v2, Mathematics of Operations Research 2023) study this question deterministically, without a random graph model, in terms of two worst-case degree parameters. Their Theorem 1 gives a sufficient condition for the minimum bisection problem to recover the hidden partition, and Theorem 2 shows the condition cannot be weakened. The rest of the paper compares this with the metric linear programming relaxation of minimum bisection. This mission formalizes Theorem 1.

Setting

Let $G=(V,E)$ be a simple graph on $V=\{1,\dots,n\}$ . A bisection of $V$ is a partition of $V$ into two sets of equal cardinality $n/2$ ; it exists only for even $n$ . Its cost is the number of edges with one end in each set. The minimum bisection problem asks for a bisection of minimum cost.

A fixed bisection $V_1,V_2$ , unknown to the solver, is the planted bisection. Write $G[V_1]$ and $G[V_2]$ for the subgraphs induced on the two sides and $G_0=(V,E_0)$ for the bipartite graph of edges between them. Two parameters measure how well the planted bisection separates the graph:

$d_{\mathrm{in}}$ , the minimum degree of the nodes of $G[V_1]\cup G[V_2]$ : every vertex has at least $d_{\mathrm{in}}$ neighbours on its own side;
$d_{\mathrm{out}}$ , the maximum degree of the nodes of $G_0$ : no vertex has more than $d_{\mathrm{out}}$ neighbours on the other side.

An optimization problem recovers the planted bisection if its unique optimal solution corresponds to the planted bisection. For minimum bisection a solution is an unordered partition, so this means: every bisection whose cost is at most that of $V_1,V_2$ is the partition $\{V_1,V_2\}$ itself.

Formalization targets

Goal: Theorem 1 (p. 4)

d_{\mathrm{in}} - d_{\mathrm{out}} > \frac n4 - 1 \quad\Longrightarrow\quad \text{the minimum bisection problem recovers the planted bisection.}

The hypothesis is the only one; no connectivity, regularity or lower bound on $n$ is assumed.

Milestones: the three inequalities of the proof (p. 5)

Fix a second bisection $\tilde V_1,\tilde V_2$ and set $U_1=V_1\cap\tilde V_1$ , $t=|U_1|$ , $U_2=V_2\cap\tilde V_2$ , $W_1=V_1\cap\tilde V_2$ , $W_2=V_2\cap\tilde V_1$ . Let $R$ be the edges between $U_1$ and $W_2$ or between $W_1$ and $U_2$ , $S$ the edges between $U_1$ and $W_1$ or between $U_2$ and $W_2$ . The paper's proof combines

|S|\le|R| \ \text{ when } \tilde V_1,\tilde V_2 \text{ is optimal},\qquad |R|\le 2t\,d_{\mathrm{out}},\qquad |S|\ge 2t\,(d_{\mathrm{in}}-t+1).

The last two hold for every pair of bisections.

Significance

Theorem 1 is a purely combinatorial certificate of exact recovery: it applies to any graph, random or not, and its two parameters are computable in linear time. Together with Theorem 2 of the same paper, which shows that for every $n$ divisible by eight and every admissible $d_{\mathrm{in}}, d_{\mathrm{out}}$ with $d_{\mathrm{in}}-d_{\mathrm{out}}\le n/4-1$ some graph is not recovered, it determines exactly which degree pairs guarantee recovery. The paper then shows that the metric LP relaxation recovers under the nearly identical condition $d_{\mathrm{in}}-d_{\mathrm{out}}\ge n/4$ with an additional regularity assumption, so the LP loses almost nothing against the NP-hard problem in this deterministic regime.

The theorem and its proof are published, and the proof is elementary. To our knowledge no machine-checked version exists. Formalizing it fixes a reusable Lean vocabulary for planted bisections (bisections as Finsets, intra- and inter-community degrees, cut cost, recovery up to swapping the sides). The later missions of this series, on the LP relaxation and on the stochastic block model, use the same vocabulary.

Difficulty

The argument is short, and the work lies in the bookkeeping. The obvious contrapositive step, "an optimal bisection different from the planted one cuts at most as many edges", only compares two totals. The proof has to split those totals into the six edge classes between the four sets $U_1,U_2,W_1,W_2$ , and it relies on the identity $|U_2|=|U_1|$ , valid for any two bisections. The lower bound on $|S|$ needs a double-counting step: the degrees inside $G[V_1]$ of the vertices of $U_1$ sum to at least $t\,d_{\mathrm{in}}$ , and edges inside $U_1$ account for at most $t(t-1)$ of that sum. In Lean the edge classes are filters over ordered pairs $i<j$ , so each identity between them is a statement about disjoint unions of finite sets. The quantity $d_{\mathrm{in}}-t+1$ can be negative, so the integer arithmetic must not truncate.

Formalization scope

Vertices are Fin n (0-based, the paper's $\{1,\dots,n\}$ ), graphs are SimpleGraph (Fin n), and a bisection is a Finset V1 with 2 * V1.card = n, the other side being V1ᶜ. The second bisection $\tilde V_1$ of the proof is a Finset W, with $\tilde V_2$ = Wᶜ.
Degrees. dIn is the minimum over all vertices of the number of same-side neighbours (defined as $0$ when $n=0$ ), and dOut is the maximum over all vertices of the number of other-side neighbours. They are the paper's parameters, not free integers.
Recovery is ∀ S, IsBisection n S → cutCost G S ≤ cutCost G V1 → S = V1 ∨ S = V1ᶜ. Requiring S = V1 alone would make the theorem false, since $V_2$ has the same cost.
Arithmetic. The hypothesis of Theorem 1 is compared in $\mathbb R$ ( $n/4$ is real division, and $d_{\mathrm{in}}-d_{\mathrm{out}}$ is not truncated), and the lower bound on $|S|$ is stated in $\mathbb Z$ . A natural-number encoding would change both statements, and the formalization rules it out.
Edge classes. $|R|$ , $|S|$ , $|T|$ are sums of counts of edges between pairs of the disjoint sets $U_1,U_2,W_1,W_2$ . Since these classes are pairwise disjoint, the sums equal the cardinalities of the unions.
Milestone 1 assumes, as the page does, that $\tilde V_1,\tilde V_2$ is an optimal bisection. The paper's normalizations $|U_1|\le n/4$ and $U_1\ne\emptyset$ are not needed for any milestone and are not assumed.

The definitions are finite and decidable in principle and need nothing beyond Mathlib's SimpleGraph and Finset. Contributions of proofs of the three milestones and of the goal are welcome. Lemmas expressing the cut cost of $V_1$ as $|R|+|T|$ and that of $\tilde V_1$ as $|S|+|T|$ are useful intermediate results.

Selected references

A. Del Pia, A. Khajavirad, D. Kunisky, Linear Programming and Community Detection, Mathematics of Operations Research, 2023; arXiv:2006.03213v2 (2022). https://arxiv.org/abs/2006.03213
E. Abbe, A. S. Bandeira, G. Hall, Exact recovery in the stochastic block model, IEEE Transactions on Information Theory 62(1), 2016. https://doi.org/10.1109/TIT.2015.2490670
M. R. Garey, D. S. Johnson, L. Stockmeyer, Some simplified NP-complete graph problems, Theoretical Computer Science 1(3), 1976. https://doi.org/10.1016/0304-3975(76)90059-1

5 thms2 active usersReviewed

Analysis Numerical Analysis Operations Research+1·Captain: mikedeng1

A Generalized Newton Method for Subgradient Systems 2: Under Metric Regularity and Semismoothness*, the FBE-Based Newton Algorithm Converges Superlinearly in Quadratic Composite OptimizationResearch Paper

Motivation

Many optimization models in statistics, signal processing and machine learning minimize a smooth loss plus a nonsmooth regularizer, $\min_x f(x)+g(x)$ . When $f$ is quadratic this is the quadratic composite problem, which also appears as the subproblem of sequential quadratic programming and of proximal Newton methods. First-order splitting methods (proximal gradient, forward-backward) handle such problems with only the proximal mapping of $g$ , but converge at best linearly. Newton-type methods converge superlinearly but classically need either smoothness or convexity of $g$ , or strong regularity (uniqueness and Lipschitz stability) of the solution.

Khanh, Mordukhovich and Phat (arXiv:2009.10551v2, 2022; Mathematics of Operations Research 2023) designed a Newton-type method for the stationarity inclusion $0\in\partial\varphi(x)$ of a nonconvex composite cost whose steps use only the proximal mapping and the second-order subdifferential (generalized Hessian) of $g$ , and proved local superlinear convergence under metric regularity rather than strong metric regularity. This mission formalizes that result, Theorem 7.8 of the paper, together with the chain of propositions through which it is proved.

Setting

Work in $\mathbb R^n$ with the Euclidean inner product. A function $g:\mathbb R^n\to(-\infty,+\infty]$ is proper if it is finite somewhere, and prox-bounded if it is bounded below by a quadratic $-a\|x\|^2-c$ . The limiting subdifferential $\partial g(x)$ collects limits of Fréchet subgradients at nearby points with nearby values.

For a set-valued map $G:\mathbb R^n\rightrightarrows\mathbb R^m$ the limiting coderivative $D^*G(x,y)(w)$ is the set of $u$ with $(u,-w)$ a limiting normal to $\operatorname{gph}G$ at $(x,y)$ ; the second-order subdifferential is $\partial^2g(x,v)=D^*(\partial g)(x,v)$ . $G$ is metrically regular around $(\bar x,\bar y)$ if $\operatorname{dist}(x;G^{-1}(y))\le\mu\operatorname{dist}(y;G(x))$ near $(\bar x,\bar y)$ , and semismooth* at $(\bar x,\bar y)$ if $\langle u^*,u\rangle=\langle v^*,v\rangle$ for every $u^*$ in the directional coderivative $D^*G((\bar x,\bar y);(u,v))(v^*)$ .

$g$ is prox-regular at $\bar x$ for $\bar v\in\partial g(\bar x)$ with modulus $r>0$ if it is lower semicontinuous near $\bar x$ and, for some $\varepsilon>0$ ,

g(x)\ge g(u)+\langle v,x-u\rangle-\tfrac r2\|x-u\|^2

for $x,u$ within $\varepsilon$ of $\bar x$ , $|g(u)-g(\bar x)|<\varepsilon$ and $v\in\partial g(u)$ within $\varepsilon$ of $\bar v$ ; continuously prox-regular if in addition $g(x_k)\to g(\bar x)$ along subgradient pairs $(x_k,v_k)\to(\bar x,\bar v)$ .

The cost is $\varphi=f+g$ with $f(x)=\tfrac12\langle Ax,x\rangle+\langle b,x\rangle+\alpha$ , $A$ symmetric. The proximal mapping $\operatorname{Prox}_{\gamma g}(u)$ is the argmin set of $y\mapsto g(y)+\frac1{2\gamma}\|y-u\|^2$ , and the forward-backward envelope (FBE) is

\varphi_\gamma(x)=\inf_y\Big\{f(x)+\langle\nabla f(x),y-x\rangle+g(y)+\tfrac1{2\gamma}\|y-x\|^2\Big\}.

Algorithm 7.6 with parameter $\gamma$ : if $0\in\partial\varphi(x^k)$ stop; otherwise set $u^k=x^k-\gamma(Ax^k+b)$ , pick $v^k\in\operatorname{Prox}_{\gamma g}(u^k)$ , choose $d^k$ with

-\tfrac1\gamma(x^k-v^k)-Ad^k\in\partial^2g\big(v^k,\tfrac1\gamma(u^k-v^k)\big)(x^k-v^k+d^k),

and set $x^{k+1}=x^k+d^k$ .

Formalization targets

Goal: Theorem 7.8

Let $g$ be proper, prox-bounded and continuously prox-regular at a stationary point $\bar x$ ( $0\in\partial\varphi(\bar x)$ ) for $-A\bar x-b$ with modulus $r$ , and let $\partial\varphi$ satisfy at $(\bar x,0)$ : (H1) solvability of $-v\in\partial^2\varphi(x,v)(d)$ near $(\bar x,0)$ , (H2) metric regularity, (H3) semismoothness*. Then

\exists\gamma_0\in(0,r^{-1}]\ \forall\gamma\in(0,\gamma_0)\ \text{with }I-\gamma A\text{ nonsingular}\ \exists U\ni\bar x:\ \text{Algorithm 7.6 is well-defined from }U,

and every run from $x^0\in U$ converges Q-superlinearly to $\bar x$ .

Milestones

Theorem 5.7: the same conclusion for the $C^{1,1}$ Newton method $-\nabla\varphi(x^k)\in\partial\langle d^k,\nabla\varphi\rangle(x^k)$ .
Proposition 7.2: near $\bar x$ , the prox-gradient map is single-valued and Lipschitz, $\varphi_\gamma$ is $C^1$ with $\nabla\varphi_\gamma(x)=\gamma^{-1}(I-\gamma\nabla^2f(x))(x-\operatorname{Prox}_{\gamma g}(x-\gamma\nabla f(x)))$ , and $\nabla\varphi_\gamma(x)=0\iff0\in\partial\varphi(x)$ .
Proposition 7.3: the generalized Hessian of $\varphi_\gamma$ in terms of $\partial^2 g$ .
Remark 7.7: a step of Algorithm 7.6 is a step of Algorithm 5.3 for $\varphi_\gamma$ .
Proposition 7.4(i): $\partial\varphi$ is metrically regular iff $\nabla\varphi_\gamma$ is.
Proposition 7.5: semismoothness* of $\partial g$ passes to $\nabla\varphi_\gamma$ .

Significance

The result gives a locally superlinear method for nonconvex composite problems that uses only first- and second-order information of the regularizer, and it replaces strong metric regularity, which forces isolated solutions, by metric regularity. The FBE reduction (Propositions 7.2–7.5) is reusable on its own: it identifies the stationary points, the generalized Hessian, and the regularity of a nonsmooth composite cost with those of a smooth function.

Formalizing it builds the first machine-checked library of coderivative calculus on Prove2Me: normal cones to graphs, limiting and directional coderivatives, second-order subdifferentials, metric regularity and semismoothness*. As far as the platform record shows, none of the paper's results has a machine-checked proof. The paper's proofs lean on second-order sum and chain rules from Mordukhovich's monograph and on Poliquin–Rockafellar's analysis of Moreau envelopes of prox-regular functions; those external results are part of the work.

Difficulty

The FBE of a nonconvex $g$ is not globally smooth; its smoothness near $\bar x$ comes from the local single-valuedness of $\operatorname{Prox}_{\gamma g}$ , which prox-regularity provides only for small $\gamma$ and only near $\bar x-\gamma\nabla f(\bar x)$ . The printed parameter range $\gamma\in(0,r^{-1})$ is too large: a far-away deep well of $g$ can capture the proximal point (see the correction below). Transferring (H1)–(H3) from $\partial\varphi$ to $\nabla\varphi_\gamma$ requires exact second-order calculus (sum and chain rules for coderivatives), not inclusions, and metric regularity is not preserved by the obvious estimates: the paper uses a coderivative characterization. Finally, Theorem 5.7 itself requires an inexact Newton analysis in which the Newton inclusion is solved by an arbitrary element of a coderivative, not by a matrix.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); products carry the sup norm, which does not change any normal cone. A symmetric $A$ is a self-adjoint continuous linear operator.
$g$ and $\varphi$ take values in EReal; $g$ is assumed proper. The envelopes are EReal-valued infima; wherever $\varphi_\gamma$ is differentiated, finiteness on a neighbourhood is asserted and the real-valued function is differentiated. $\nabla^2 f(x)$ is the derivative of gradient f.
$\partial$ is the published analytic limiting subdifferential NonconvexSplitting.Shared.LimitingSubdiff. It agrees with the paper's geometric definition (2.9) for functions lower semicontinuous around the point, which covers every function the statements apply it to.
Metric regularity uses $\operatorname{dist}(\cdot;\emptyset)=+\infty$ . Directional normals read $t_k\downarrow0$ as $t_k>0$ , $t_k\to0$ . For a $C^{1,1}$ or $C^1$ function, $\partial^2\varphi(x)$ is the coderivative of the single-valued gradient map.
The proximal mapping is the argmin set; runs may select any proximal point and any direction solving the Newton inclusion; conclusions hold for every run. The stop rule is a constant tail. "Well-defined from $U$ " means every partial run from $U$ can be continued. Q-superlinear convergence is in $\varepsilon$ -form, which avoids the ratio $0/0$ .
Correction. Propositions 7.2–7.5, Remark 7.7 and Theorem 7.8 are claimed for every $\gamma\in(0,r^{-1})$ ; that is false. For $n=1$ , $A=0$ , $b=0$ and $g(y)=\tfrac12y^2$ on $[-5,5]$ , $g(y)=-1000-|y-10|$ on $[9,11]$ , $+\infty$ elsewhere ( $\bar x=0$ , $r=1$ , $\gamma=\tfrac12$ ), $\operatorname{Prox}_{\gamma g}=\{9\}$ near $0$ and every run jumps to the stationary point $9$ . All these items are posed as "there is $\gamma_0\in(0,r^{-1}]$ such that for every $\gamma\in(0,\gamma_0)$ ", the range the cited Poliquin–Rockafellar theorem supports. Theorem 5.7 is posed as printed.
The goal cannot be trivialized: $\gamma_0>0$ is asserted, the convergence is claimed for every run and every admissible $\gamma$ below $\gamma_0$ , and the hypotheses are satisfied, for instance, by $g=\tfrac12\|\cdot\|^2$ . Specializing $g$ to be convex, $A=0$ , $A$ positive definite, or $\bar x$ a tilt-stable minimizer would change the theorem and is not accepted.
Needed infrastructure: limiting normal cones and coderivatives, their sum and chain rules for a smooth plus a set-valued map, the Mordukhovich criterion, Moreau envelopes of prox-regular functions (Poliquin–Rockafellar). These are reusable well beyond this mission; contributions of any of them as separate theorems are welcome.

Selected references

P. D. Khanh, B. S. Mordukhovich, V. T. Phat, A Generalized Newton Method for Subgradient Systems, arXiv:2009.10551v2, 2022; Mathematics of Operations Research, 2023. https://arxiv.org/abs/2009.10551
B. S. Mordukhovich, Variational Analysis and Generalized Differentiation I: Basic Theory, Springer, 2006. https://doi.org/10.1007/3-540-31247-1
R. A. Poliquin, R. T. Rockafellar, Prox-regular functions in variational analysis, Transactions of the AMS 348 (1996) 1805–1838. 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 Journal on Optimization 31 (2021) 489–517. https://doi.org/10.1137/19M1257408
P. Patrinos, A. Bemporad, Proximal Newton methods for convex composite optimization, IEEE CDC 2013. https://doi.org/10.1109/CDC.2013.6760233

22 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Optimization+1·Captain: mikedeng1

Managing Outpatient Service with Strategic Walk-ins I: With Total Capacity μ ≤ √(λC_D/(2R)), the Observable Scheduling Setting Costs No More Than the Unobservable OneResearch Paper

Motivation

Outpatient clinics serve two kinds of patients: those who book an appointment and those who walk in on the day. Many providers now run open-access or hybrid schedules, which reserve part of the day for walk-ins. Whether patients book or walk in depends on what they know about the appointment delay. Some clinics publish the next available slot in real time (online booking). Others take requests asynchronously, so patients act on a typical delay. Liu, van Jaarsveld, Wang and Xiao (SSRN 3558209; Management Science, 2023, doi:10.1287/mnsc.2023.4676) model this choice as a game between strategic patients and a provider who splits capacity between appointment and walk-in hours. This mission formalizes their first comparison result: when capacity is short, showing patients the exact delay is at least as good for the provider as hiding it.

The model extends Naor's observable-queue joining problem (Naor, Econometrica, 1969) to an M/D/1 appointment queue with a continuous delay threshold, and adds a walk-in channel whose waiting cost depends on congestion.

Setting

Demand. Strategic patients arrive as a Poisson process of rate $\lambda>0$ per day. Exogenous walk-ins arrive at rate $\lambda_E\ge0$ and always walk in.

Capacity. The provider has total daily capacity $\mu>0$ . It allocates $\mu_S$ to appointment hours and $\mu_W=\mu-\mu_S$ to walk-in hours, with $0\le\mu_S<\mu$ . Appointments form a single-server queue with deterministic service time $1/\mu_S$ .

Utilities. Service is worth $R>0$ . A patient who books with delay $d$ gets $R-C_Dd$ , where $C_D>0$ . A patient who walks in gets $R-C_W\,w(\rho_W)$ , where $C_W>0$ and $\rho_W$ is the walk-in traffic intensity (walk-in arrivals divided by $\mu_W$ ). Balking is worth $0$ . The function $w$ is convex and strictly increasing on $[0,\infty)$ with $w(0)=0$ (Assumption 1).

Provider cost. Each balking patient costs $C_L\ge0$ , and overtime costs $C_O\,o(\rho_W)$ with $C_O\ge0$ , where $o$ is convex and strictly increasing on $[0,\infty)$ (Assumption 2).

Observable setting. Each patient sees the exact delay $(k+\tilde u)/\mu_S$ , where $k$ is the number waiting and $\tilde u$ is uniform on $[0,1]$ . A strategy is a triple $(\delta,p_W,p_B)$ : book if the delay is at most $\delta$ , and otherwise walk in or balk with probabilities $p_W$ and $p_B$ . The appointment queue is then the M/D/1/K−1+p queue with $K=\lceil\delta\mu_S\rceil$ and $p=\delta\mu_S+1-K$ . Its blocking probability has the closed form

\pi(\delta,\mu_S)=1-\frac{1}{q_0+\rho},\qquad \rho=\frac{\lambda}{\mu_S},

where $q_0$ is the probability that a departure leaves the system empty, given by Brun–Garcia sums of Poisson weights. An observable equilibrium satisfies conditions (6)–(10): booking is preferred to the walk-in/balk mixture exactly for delays up to $\delta$ ; $p_W+p_B=\pi(\delta,\mu_S)$ ; and patients walk in only if walking in is worth at least $0$ , and balk only if it is worth at most $0$ . The cost is

Z^o=C_L\,p_B\lambda+C_O\,o\Big(\frac{p_W\lambda+\lambda_E}{\mu_W}\Big).

Unobservable setting. Patients see only the expected M/D/1 delay $\bar d=\lambda_S/(2\mu_S(\mu_S-\lambda_S))$ and choose rates $(\lambda_S,\lambda_W,\lambda_B)$ that sum to $\lambda$ . An unobservable equilibrium uses only options of maximal utility among $u^1_S=R-C_D\bar d$ , $u^1_W=R-C_Ww((\lambda_W+\lambda_E)/\mu_W)$ and $0$ . The cost is

Z^u=C_L\lambda_B+C_O\,o\Big(\frac{\lambda_W+\lambda_E}{\mu_W}\Big).

Formalization targets

Goal: Theorem 2 (1)

If

\mu\le\sqrt{\frac{\lambda C_D}{2R}},

then for every allocation $\mu_S$ and every unobservable equilibrium $u$ at $\mu_S$ , there is an allocation $\mu'_S$ at which an observable equilibrium exists and every observable equilibrium costs at most $Z^u(u)$ . Equivalently, the optimal observable cost is at most the optimal unobservable cost. The paper states "when $\mu$ is sufficiently small"; the threshold is the one its proof establishes.

Milestones

(27), §C.1: the closed-form departure law $q_0,\dots,q_K$ is a probability vector that solves the departure-epoch balance equations.
Proof of Theorem 2(1): $\lambda/(1+\lambda/\mu_S)\le\lambda[1-\pi(\delta,\mu_S)]\le\lambda$ .
Proposition C.2 ( $\delta$ -part): $\pi(\cdot,\mu_S)$ is continuous and strictly decreasing.
Proposition 1 (observable setting): an observable equilibrium exists at every allocation.
Lemma D.3: an unobservable equilibrium exists at every allocation.
Lemma E.5 (1): at a fixed allocation, if $\lambda[1-\pi(\bar d^u,\mu_S)]\ge\lambda^u_S$ , the observable setting costs no more.

Significance

The result says that real-time delay information helps a capacity-constrained provider. Patients who see a short queue book instead of balking, so the appointment hours are better used. The second part of Theorem 2 shows that the comparison can reverse when capacity is large, so the information choice depends on the regime. The small-capacity side is the one that applies to clinics without spare capacity.

The formalization also produces reusable queueing content. It gives a machine-checked closed form for the M/D/1/K−1+p queue with fractional buffer (Hassin–Haviv notation): its departure-epoch law, its blocking probability, and the monotonicity and continuity of that probability in the buffer. The paper's proofs are in its Online Appendix: E.3 for Lemma E.5 and Theorem 2, and E.4 for Appendix C. None of these results has a machine-checked proof.

Difficulty

The obvious argument fixes an optimal unobservable allocation and compares both settings there. That argument has three gaps. First, the existence of an optimum of (Un.P) is never proved, so the comparison has to work at every allocation. Second, the same-allocation comparison (Lemma E.5) is a three-by-three case analysis over the equilibrium regimes (schedule-balk, schedule-walk-balk, schedule-walk) of the two settings. One printed case concludes the opposite inequality; under the lemma's hypothesis that case forces equal costs. Third, the closed-form blocking probability is an alternating sum. Its positivity, its bound $q_0\le1$ and its monotonicity across the seams where $\lceil\delta\mu_S\rceil$ jumps are not visible term by term. Existence of the observable equilibrium needs an intermediate-value argument through the continuity of $\pi$ in $\delta$ .

Formalization scope

Everything lives in the namespace OutpatientWalkIn.SmallCap, in two definition modules.

MD1Queue holds the Poisson weights, the $a_j$ recursion (one clause for $j\ge1$ ), $b_j$ , $a'_K$ of (26), the departure law (27), $\alpha'_j$ of (24) and $\pi(\delta,\mu_S)$ .
Setting holds the model, the standing assumptions, both equilibrium notions and both costs.

The conventions are the following.

Disengagement cost. $C_G$ is not a parameter. The observable ( $C_G=0$ ) and unobservable ( $C_G=+\infty$ ) settings are defined directly, as Lemmas 4 and 6 and Appendices D.3 and D.5 reduce them.
Standing assumptions. $\lambda>0$ , $\lambda_E\ge0$ , $R,C_D,C_W>0$ , $C_L,C_O\ge0$ , $\mu>0$ , and Assumptions 1–2 on $[0,\infty)$ . The paper leaves the signs other than $R,C_D,C_W>0$ implicit.
Allocations. $0\le\mu_S<\mu$ , so the walk-in intensity never divides by $0$ .
No appointment capacity. $\pi(\delta,0)=1$ . In the unobservable setting, $\mu_S=0$ forces $\lambda_S=0$ and drops $u^1_S$ from the comparisons.
Stability. An unobservable equilibrium must have $\lambda_S<\mu_S$ , so the junk value of (18) at $\lambda_S\ge\mu_S$ never enters.
Mixture weights. The observable equilibrium requires $p_W+p_B>0$ , which (8) implies.
Formula branches. $(1-p)^{-n}$ is written $((1-p)^n)^{-1}$ , and the branches $p=1$ and $p<1$ are separate.
Costs less. It means $\le$ (p. 26).

A trivializing formalization is ruled out on four counts: $\pi$ is the paper's closed form, not an assumed function; the goal quantifies over every unobservable equilibrium and every observable equilibrium at the chosen allocation; no infimum over a possibly empty set appears; and both equilibrium sets are nonempty (milestones 4 and 5).

The infrastructure needed is elementary real analysis and finite sums. Contributions are welcome on the queue lemmas (positivity of $a_j$ and $a'_K$ , the bound $q_0\le1$ , continuity across seams), which are reusable for any finite-buffer M/D/1 model. The companion mission on the triage model uses the same encoding.

Selected references

N. Liu, W. van Jaarsveld, S. Wang, G. Xiao, Managing Outpatient Service with Strategic Walk-ins, Management Science, 2023 (SSRN copy of 2022-07-05). https://ssrn.com/abstract=3558209, https://doi.org/10.1287/mnsc.2023.4676
P. Naor, The Regulation of Queue Size by Levying Tolls, Econometrica 37(1), 1969. https://doi.org/10.2307/1909200
O. Brun, J.-M. Garcia, Analytical Solution of Finite Capacity M/D/1 Queues, Journal of Applied Probability 37(4), 2000. https://doi.org/10.1239/jap/1014843085
R. Hassin, M. Haviv, To Queue or Not to Queue: Equilibrium Behavior in Queueing Systems, Kluwer, 1997 (2003 ed.). https://doi.org/10.1007/978-1-4615-0359-0

10 thms2 active usersReviewed

Machine Learning Reinforcement Learning Statistics·Captain: mikedeng1

Breaking the Sample Size Barrier in Model-Based Reinforcement Learning with a Generative Model 4: Finite-Horizon Model-Based Planning Is ε-Optimal w.p. 1−δ Once N ≥ c₀H³log(H|S||A|/δ)/ε²Research Paper

Motivation

Reinforcement learning with a generative model (a simulator) is a basic way to measure how many samples planning needs. A learner may query, for any state $s$ , action $a$ and step $h$ , a fresh next state drawn from the unknown transition law $P_h(\cdot\mid s,a)$ , and must output a near-optimal policy. Model-based planning is the simplest approach: estimate each transition law by empirical frequencies, then solve the estimated model exactly by dynamic programming. It is widely used, and its sample complexity is the reference point for model-free methods.

G. Li, Y. Wei, Y. Chi and Y. Chen (arXiv:2005.12900v8; Operations Research, 2024) show that model-based planning is minimax optimal over the full range of accuracies, for discounted MDPs (Theorems 1–3) and for time-inhomogeneous finite-horizon MDPs (Theorem 4). This mission covers the finite-horizon case. Earlier model-based analyses of the finite-horizon setting, such as Yin et al. (2021), required $N\gtrsim H^2$ samples per triple $(s,a,h)$ up to logarithmic factors before any guarantee applied; Theorem 4 needs only $N\gtrsim H$ .

Setting

A finite-horizon MDP $\mathcal M=(\mathcal S,\mathcal A,\{P_h\}_{h=1}^H,\{r_h\}_{h=1}^H,H)$ has a finite state space $\mathcal S$ , a finite nonempty action space $\mathcal A$ , a horizon $H$ , and for every step $h\in[H]=\{1,\dots,H\}$ a transition kernel $P_h(s'\mid s,a)$ and a reward $r_h(s,a)\in[0,1]$ . The kernels may differ across steps (time inhomogeneity).

A deterministic nonstationary policy $\pi=\{\pi_h\}$ chooses action $\pi_h(s)$ at step $h$ in state $s$ . Its value and Q-function satisfy the backward Bellman equations

V^\pi_{H+1}=0,\qquad Q^\pi_h(s,a)=r_h(s,a)+\sum_{s'}P_h(s'\mid s,a)V^\pi_{h+1}(s'),\qquad V^\pi_h(s)=Q^\pi_h(s,\pi_h(s)),

so $V^\pi_h(s)$ is the expected sum of rewards from step $h$ to $H$ started at $s$ , and lies in $[0,H]$ . The optimal values are $V^\star_h(s)=\max_\pi V^\pi_h(s)$ and $Q^\star_h(s,a)=r_h(s,a)+\sum_{s'}P_h(s'\mid s,a)V^\star_{h+1}(s')$ .

The generative model returns, for every triple $(s,a,h)$ , $N$ independent samples $s^i_h(s,a)\sim P_h(\cdot\mid s,a)$ , all samples independent. The empirical kernel is

\widehat P_h(s'\mid s,a)=\frac1N\sum_{i=1}^N\mathbb 1\{s^i_h(s,a)=s'\},

and the empirical MDP $\widehat{\mathcal M}$ replaces every $P_h$ by $\widehat P_h$ , keeping the rewards. Model-based planning returns the policy $\widehat\pi^\star$ obtained by backward dynamic programming on $\widehat{\mathcal M}$ : at each step, $\widehat\pi^\star_h(s)$ maximizes the empirical optimal Q-function $\widehat Q^\star_h(s,\cdot)$ . So $\widehat\pi^\star_h$ depends only on $\widehat P_h,\dots,\widehat P_H$ .

Formalization targets

Goal: Theorem 4 (p. 10)

There is a universal constant $c_0>0$ such that for every finite-horizon MDP, every $\delta>0$ and every $0<\varepsilon\le H$ : if

N\ge\frac{c_0H^3\log\big(H|\mathcal S||\mathcal A|/\delta\big)}{\varepsilon^2},

then with probability at least $1-\delta$ ,

\forall(s,a,h)\in\mathcal S\times\mathcal A\times[H]:\qquad V^{\widehat\pi^\star}_h(s)\ge V^\star_h(s)-\varepsilon,\qquad Q^{\widehat\pi^\star}_h(s,a)\ge Q^\star_h(s,a)-\varepsilon.

The constant $c_0$ is not specified, so the goal survives any improvement of constants.

Milestones

Lemma 12 (p. 34): the auxiliary vectors $V^{(l)}_h$ of (62), obtained by propagating square roots of one-step variances, obey $\|V^{(l)}_h\|_\infty\le(\sqrt{3H})^lH$ .
Lemma 9 (p. 21): if the one-step errors $(\widehat P_{h,\pi}-P_{h,\pi})V^{(l)}_{h+1}$ satisfy a Bernstein-type bound (63) with parameter $\beta_1$ for $0\le l\le\log_2H$ , and $N>12H\beta_1$ , then $\|\widehat V^\pi_h-V^\pi_h\|_\infty\le6H\sqrt{3\beta_1H/N}$ .
(66)–(67) (p. 21): for a fixed policy, the Bernstein-type bound holds for all $(s,a)$ with probability at least $1-\delta$ , with $\beta_1=4\log(H|\mathcal S||\mathcal A|/\delta)$ .
§7.3, second bullet (pp. 21–22): the same accuracy $\|\widehat V^{\widehat\pi^\star}_h-V^{\widehat\pi^\star}_h\|_\infty\le6H\sqrt{12H\log(H|\mathcal S||\mathcal A|/\delta)/N}$ holds for the data-dependent planner's policy.
(65) (p. 21): $V^\star_h-V^{\widehat\pi^\star}_h\le(\widehat V^{\widehat\pi^\star}_h-V^{\widehat\pi^\star}_h)+(V^{\pi^\star}_h-\widehat V^{\pi^\star}_h)$ .
(68) (p. 22): $0\le V^\star_h-V^{\widehat\pi^\star}_h\le12H\sqrt{12H\log(H|\mathcal S||\mathcal A|/\delta)/N}$ with probability at least $1-2\delta$ when $N\ge48H\log(H|\mathcal S||\mathcal A|/\delta)$ .

Significance

The result. The total number of samples is $NH|\mathcal S||\mathcal A|$ , so Theorem 4 gives $\varepsilon$ -optimal policies from $\widetilde O(|\mathcal S||\mathcal A|H^4/\varepsilon^2)$ samples, which matches the known lower bound up to logarithmic factors, for every $\varepsilon\in(0,H]$ . The extra factor of $H$ compared with the discounted case is the price of time inhomogeneity: each step has its own kernel to estimate. The guarantee holds from $N\gtrsim H$ samples per triple on, instead of $N\gtrsim H^2$ . Unlike the paper's discounted results, no reward perturbation or conservative action selection is needed. The step-by-step independence of the data makes the plain planner analyzable.

Formalizing it. The theorem is proved in the paper; nothing here is open mathematically, and no machine-checked proof of it is known. A formalization checks the details the paper leaves implicit: the index ranges of the backward recursions, the use of $\log_2H$ as an integer, the sample-size condition of Lemma 9 when it is applied to the planner's policy, and the independence argument that lets a data-dependent policy enjoy fixed-policy concentration. The finite-horizon layer here (time-inhomogeneous kernels, backward propagation, the DP planner, the empirical kernel and the finite law of the data) is reusable by other finite-horizon sample-complexity results.

Difficulty

The planner's policy $\widehat\pi^\star$ is built from the same data that define $\widehat{\mathcal M}$ , so the obvious route, applying a concentration inequality to $(\widehat P_h-P_h)V^{\widehat\pi^\star}_{h+1}$ as if $V^{\widehat\pi^\star}_{h+1}$ were fixed, is not justified by itself. The argument has to use the backward structure: the step- $h$ quantities depend only on the data of later steps, which are independent of $\widehat P_h$ .

A second difficulty is the sample-size range. A Hoeffding-type bound on each one-step error, summed over $H$ steps, gives an accuracy that only becomes meaningful when $N\gtrsim H^2$ . Reaching $N\gtrsim H$ requires Bernstein-type bounds and the control of a whole sequence of auxiliary value vectors $V^{(l)}$ , of which Lemma 12 bounds the size. Lemma 9 then has to close the recursion in $l$ after about $\log_2H$ levels.

Formalization scope

Steps are Fin H, 0-based: the paper's step $h$ is Lean's $h-1$ . Backward propagation returns $0$ at every index $\ge H$ , which encodes $V_{H+1}=0$ . The paper's ranges $1\le h\le H-1$ in (63) and (66) are written h.val + 1 < H.
Values are defined by the backward Bellman recursion (equal to the trajectory expectation of p. 6 for deterministic policies), $V^\star_h$ as a maximum over the finitely many deterministic nonstationary policies, and $Q^\star_h:=r_h+P_hV^\star_{h+1}$ .
The planner takes a tie-breaking rule sel (any argmax rule), fixed before the data and quantified outside the probability. Empirical Q-values tie with positive probability, and the proof needs $\widehat\pi^\star$ to be a fixed function of the empirical kernels.
Probability. A data set is an element of the finite type $[H]\times\mathcal S\times\mathcal A\times[N]\to\mathcal S$ ; its law is the product of the kernels, and probabilities are finite sums. "With probability at least $1-\delta$ " is written as a bound $\le\delta$ on the probability of the failure event. $N>0$ is assumed throughout, as in (6).
Constants. $c_0$ is quantified before the spaces, the horizon and the MDP. The page names "universal constants $c_0,c_1>0$ ", but $c_1$ does not occur in Theorem 4; only $c_0$ is quantified.
Generalizations disclosed in the items. Lemma 9 and (65) are stated for any family of transition kernels $\widehat P_h$ , and (66)–(67) for any data-independent policy instead of only $\pi^\star$ . The second bullet of §7.3 carries the condition $N\ge48H\log(H|\mathcal S||\mathcal A|/\delta)$ , which the page leaves implicit there and states with (68).

Trivializing formalizations are ruled out: the planner is computed from the empirical kernels, not from the true $P_h$ ; the model is time-inhomogeneous, with one kernel per step; and $c_0$ cannot depend on $H$ , $\mathcal S$ , $\mathcal A$ or the MDP.

The only external definition is the published FoundationsML.ReinforcementLearning.IsTransitionKernel. A complete development needs Bernstein's inequality for bounded i.i.d. averages (on finite product laws), a union bound, and the independence of the per-step data. Contributions are welcome on all six milestones and on general lemmas about the finite law of the data, such as independence across steps and the distribution of $\widehat P_h$ .

Selected references

G. Li, Y. Wei, Y. Chi, Y. Chen, Breaking the Sample Size Barrier in Model-Based Reinforcement Learning with a Generative Model, arXiv:2005.12900v8, 2023; Operations Research, 2024. https://arxiv.org/abs/2005.12900
M. G. Azar, R. Munos, H. J. Kappen, Minimax PAC bounds on the sample complexity of reinforcement learning with a generative model, Machine Learning 91(3):325–349, 2013. https://doi.org/10.1007/s10994-013-5368-1
A. Agarwal, S. Kakade, L. F. Yang, Model-Based Reinforcement Learning with a Generative Model is Minimax Optimal, COLT 2020. https://arxiv.org/abs/1906.03804
M. Yin, Y. Bai, Y.-X. Wang, Near-optimal provable uniform convergence in offline policy evaluation for reinforcement learning, AISTATS 2021, PMLR 130:1567–1575. https://proceedings.mlr.press/v130/yin21a.html
D. P. Bertsekas, Dynamic Programming and Optimal Control, 4th ed., Athena Scientific, 2017.

10 thms2 active usersReviewed

Algorithmic Game Theory Economics·Captain: mikedeng1

Sharing Sequentially Triggered Losses: Automated Conflict Resolution Through Smart Contracts 4: On Loss Trees the Same Four Axioms Characterize the Fixed-Fraction RulesResearch Paper

Motivation

When one agent breaches a contract, the breach often forces its counterparty to breach its own contracts in turn, and the losses propagate. Supply chains are the standard example: a supplier that fails to deliver makes its customer fail to deliver to its own customers. Gudmundsson, Hougaard and Ko (Management Science 70(3), 2024) ask how the total loss of such a cascade should be shared among the agents involved. Their aim is a rule simple enough to be written into a smart contract that settles disputes automatically. They first treat a single chain of agents and characterize the fixed-fraction rules by four axioms (Theorem 1). Section 5 then extends the model to loss trees, in which one agent may cause losses to several others, as when a firm supplies several downstream firms. Theorem 4 shows that the same four axioms, suitably extended, characterize the fixed-fraction rules on trees. This mission formalizes Theorem 4 and the steps of its proof in Appendix A.

The tree model follows a line of work on sharing liability and costs along hierarchies and networks; the paper compares its setting with Oishi, van der Laan and van den Brink (2023).

Setting

Agents are natural numbers. An edge $ij$ records that agent $i$ causes a loss to agent $j$ . A finite edge set $T$ covers the vertices $V(T)=\bigcup_{ij\in T}\{i,j\}$ . It is a tree if it has a root (a vertex with no incoming edge) and every other vertex has exactly one incoming edge and is reached from the root. The root is the initiator of the cascade. Leaves are victims only. The agents who share the losses are the non-leaf vertices $N(T)$ . A loss is a function $\ell\ge 0$ on edges, and the total loss is $L=\sum_{e\in T}\ell(e)$ .

A rule $\varphi$ assigns a liability $\varphi_i(T,\ell)$ to each agent $i\in N(T)$ . Liabilities are non-negative and sum to $L$ . A rule is required to be invariant to agent labels: renaming the agents by a bijection $\pi$ of $\mathbb N$ renames the liabilities. It is also continuous along $a\ell\to\ell$ as $a\to 1$ , the paper's standing assumption.

The fixed-fraction rule with parameter $\lambda\in[0,1]$ makes each agent pay the fraction $\lambda$ of the losses it causes directly. The root also pays the remaining fraction of the total:

\varphi^\lambda_i(T,\ell)=\lambda\sum_{ij\in T}\ell(ij)+[i\text{ is the root}]\,(1-\lambda)L .

The elementary tree problem $e_n=(T_n,\ell_n)$ is the chain $T_n=\{12,23,\dots,(n,n+1)\}$ with a unit loss on its last edge. For a vertex $v$ , $P^v$ is the set of edges on the path from the root to $v$ , $[v]$ is the number of vertices on that path, and $T^v$ is the subtree rooted at $v$ .

The four axioms are as follows.

Tree additivity: $\varphi(T,\ell)+\varphi(T,\ell')=\varphi(T,\ell+\ell')$ .
Tree zero truncation: adding a zero-loss edge from a vertex of $T$ to a new leaf leaves every liability in $N(T)$ unchanged.
Population monotonicity: inserting a zero loss into $e_n$ makes no agent worse off. On elementary problems this reads $\varphi_i(e_n)\ge\varphi_i(e_{n+1})$ for $1\le i\le j$ and $\varphi_k(e_n)\ge\varphi_{k+1}(e_{n+1})$ for $j<k\le n$ , for every $1\le j<n$ .
Merging proofness: $\varphi_i(e_3)+\varphi_{i+1}(e_3)\le\varphi_i(e_2)$ for $i\in\{1,2\}$ .

Formalization targets

Goal: Theorem 4

For every rule $\varphi$ on loss trees,

\varphi \text{ satisfies the four axioms}\iff \exists\,\lambda\in[0,1]:\ \varphi_i(T,\ell)=\varphi^\lambda_i(T,\ell)\ \text{for all trees } T,\ \ell\ge 0,\ i\in N(T).

Milestones

Each $\varphi^\lambda$ with $\lambda\in[0,1]$ is a rule on trees (p. 16).
Tree additivity and continuity give scale invariance, $\varphi(T,\alpha\ell)=\alpha\varphi(T,\ell)$ for $\alpha\ge 0$ (p. 25).
Edge-by-edge decomposition, $\varphi(T,\ell)=\sum_{jk\in T}\ell(jk)\,\varphi(T,\ell_k)$ (p. 25).
An agent $i$ with $jk\notin T^i$ is not liable for a unit loss on $jk$ (p. 25).
Trimming to the path, $\varphi_i(T,\ell_k)=\varphi_i(P^k,\ell_k)$ for $jk\in T^i$ (p. 25).
Relabelling, $\varphi_i(P^k,\ell_k)=\varphi_{[i]}(e_{[j]})$ (p. 25).
Proposition 3: tree additivity and tree zero truncation hold if and only if $\varphi_i(T,\ell)=\sum_{jk\in T^i}\ell(jk)\,\varphi_{[i]}(e_{[j]})$ (p. 25).
Proposition 2 on trees: population monotonicity and merging proofness hold if and only if $\varphi(e_n)=\varphi^\lambda(e_n)$ for all $n$ and some $\lambda\in[0,1]$ (pp. 12, 17).

Significance

Theorem 4 says that the axioms which single out the fixed-fraction rules on chains still single them out on trees, with nothing added. Because the rule only needs each agent's direct losses and the identity of the initiator, it can be computed locally. This is what the paper uses to implement liability sharing in a smart contract (Section 6, Figure 3). The characterization also justifies applying the rule to supply networks, where firms supply several customers, rather than only to chains.

The paper's proof of Theorem 4 is a short sketch: it reduces trees to chains by trimming and relabelling, then cites the chain argument. No machine-checked version of any part of the paper exists. Formalizing it would check the reduction in full, including the bookkeeping that the printed proof compresses. While preparing this mission, three places where the printed text differs from what the argument establishes were found; they are corrected here (see Formalization scope). The tree machinery built here (paths, depths, subtrees, relabelling of finite rooted trees over $\mathbb N$ ) is reusable for other liability and cost-sharing models on hierarchies.

Difficulty

The obvious argument works edge by edge: use additivity to isolate one edge, use zero truncation to cut the tree down to the path through that edge, then relabel the path into a chain. The first gap is that additivity yields only rational homogeneity. Continuity, or the monotonicity that additivity and non-negativity give, is needed for real multiples. The second is that zero truncation only adds or removes leaf edges, so trimming must proceed leaf by leaf, keeping a tree at every step. It must also be shown that agents removed from the tree carried no liability, which needs balance and non-negativity. The third is that relabelling requires a bijection of all of $\mathbb N$ that maps the path onto $1,\dots,[k]$ , together with a loss on the relabelled tree. Label invariance must hold for every such loss, not only one chosen extension. Finally, the chain part (Proposition 2) pins down $\varphi(e_n)$ by an induction that chains population-monotonicity inequalities with merging proofness.

Formalization scope

Trees are Finset (ℕ × ℕ) with the root, unique-parent and reachability conditions above. Vertex labels keep the paper's numbering ( $T_n$ uses $1,\dots,n+1$ ); Lean's $\mathbb N$ also contains $0$ , which label invariance makes harmless. A rule is a function φ T ℓ i on all edge sets, real functions and naturals. Every axiom and every conclusion is quantified only over trees, non-negative losses and agents $i\in N(T)$ . The conclusion $\varphi=\varphi^\lambda$ is equality at those arguments. A function equality would be false, since a rule's other values are arbitrary. The rule conditions (non-negativity, balance, label invariance, continuity) are a hypothesis of every statement. Dropping them makes Theorem 4 false: the parameter $\lambda$ need not lie in $[0,1]$ , and a rule need not respect the tree's labels. The root of $\varphi^\lambda$ is detected as the vertex with no incoming edge, never hard-coded as label 1.

Three disclosed departures from the printed text:

Axiom 6 adds leaves only. The axiom is stated with the extra condition that the new edge ends at a vertex outside $T$ , as the sentence before the axiom says. Read literally, the axiom would allow a zero-loss edge into the old root, which moves the root. The fixed-fraction rules with $\lambda<1$ violate that literal version, and Theorem 4 would be false.
Population monotonicity uses $1\le j<n$ . The page prints $1<j<n$ , under which Theorem 1 already fails.
Proposition 3 and the relabelling step use $e_{[j]}$ . The page prints $e_{[k]}$ for the edge $jk$ , but $P^k$ has $[k]-1=[j]$ edges. With $e_{[k]}$ , Proposition 3 is false for $\varphi^\lambda$ .

Continuity is taken from Section 2, where it is standing; the proof of Proposition 3 invokes it. A complete development needs finite rooted trees over $\mathbb N$ , reachability (Relation.ReflTransGen), the extension of a finite injection to a permutation of $\mathbb N$ , and leaf-by-leaf induction on trees. Proofs of any milestone are welcome, as are alternative routes to Theorem 4, for example through monotonicity instead of continuity.

Selected references

J. Gudmundsson, J. L. Hougaard, C. Y. Ko, Sharing Sequentially Triggered Losses: Automated Conflict Resolution Through Smart Contracts, Management Science 70(3), 1773–1786, 2024. https://doi.org/10.1287/mnsc.2023.4772 (formalized from the authors' accepted manuscript, 2023).
T. Oishi, G. van der Laan, R. van den Brink, Axiomatic analysis of liability problems with rooted-tree networks in tort law, Economic Theory 75, 229–258, 2023.

11 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research+1·Captain: mikedeng1

Marketplace Leakage 4: The Marketplace Prefers Not to Impose a Price-Parity Clause If and Only If q < 1/2 and μ > (v − c)/2Research Paper

Motivation

Online marketplaces (Amazon, Booking.com, Airbnb, Upwork) charge sellers a fee on every transaction they intermediate. Once a buyer has found a seller on the marketplace, both have an incentive to complete the sale off the platform and split the fee they save. This is leakage (also called disintermediation or showrooming), and it limits the fees a marketplace can sustain. Hagiu and Wright, Marketplace Leakage (Management Science, 2023, doi:10.1287/mnsc.2023.4757), build a minimal model of leakage and compare the strategies a marketplace can use against it.

One of these strategies is contractual: a price-parity clause (PPC), under which the seller must not charge less in its direct channel than on the marketplace, on pain of being delisted. The paper notes that such clauses have been used by hotel-booking platforms, price-comparison platforms and Amazon (p. 22). The paper's Proposition 4 asks when a marketplace that cannot observe how easily buyers switch actually wants such a clause. This mission formalizes that proposition and the profit formulas behind it.

Setting

A marketplace $M$ , a seller $S$ and a unit mass of buyers with unit demand. Every buyer values $S$ 's product at $v$ ; $S$ 's marginal cost is $c<v$ ; the outside option is worth $0$ . $S$ sells on $M$ at price $p_m$ , paying $M$ a fee $f$ per transaction, or directly at price $p_d$ with no fee. A buyer who buys directly bears a switching cost $s$ . In the baseline state switching costs are uniform on $[0,\mu]$ , $\mu>0$ , with clamped distribution function $G(s)=\min\{\max\{s/\mu,0\},1\}$ . In the no-switching state switching costs are infinite and nobody buys directly. The baseline state occurs with probability $q$ . $S$ knows the state when it decides; $M$ does not when it sets $f$ .

Without a PPC, $S$ always lists, sets $p_m=v$ , and in the baseline state picks $p_d\le v$ to maximize

\pi(f,p_d)=(p_d-c)G(v-p_d)+(v-c-f)\big(1-G(v-p_d)\big).

A maximizer is a seller-optimal price $p_d^*(f)$ . $M$ 's value is

\Pi^*=\max_{f\le v-c} f\big(1-q\,G(v-p_d^*(f))\big).

With a PPC, a listed seller must set $p_d=p_m=v$ and earns $v-c-f$ . A seller that delists earns $\max_{c\le p_d\le v}(p_d-c)G(v-p_d)$ in the baseline state and $0$ in the no-switching state. It accepts $M$ 's offer when listing pays at least as much, so $M$ 's value $\Pi^*_{PPC}$ is the largest expected revenue $f\cdot\Pr[\text{accept}]$ over all fees $f$ .

Formalization targets

Goal: Proposition 4 (p. 23)

For $c<v$ , $\mu>0$ and $0<q\le 1$ , both values exist, and

\Pi^*>\Pi^*_{PPC}\iff q<\tfrac12\ \text{ and }\ \mu>\tfrac{v-c}{2},\qquad\text{otherwise}\quad \Pi^*_{PPC}\ge\Pi^* .

The goal states the comparison for any values satisfying the optimality predicates, so it is insensitive to how either value is later computed.

Milestones

$\Pi^*_{PPC}=\max\{v-c-D,\ (1-q)(v-c)\}$ , where $D=\max_{c\le p_d\le v}(p_d-c)G(v-p_d)$ (p. 23).
$D=\dfrac{(v-c)^2}{4\mu}$ if $\mu\ge\frac{v-c}{2}$ and $D=v-c-\mu$ otherwise, so $\Pi^*_{PPC}$ has a closed form (p. 39).
For $q<\tfrac12$ : $\displaystyle\Pi^*=(v-c)\Big(1-q\min\Big\{\frac{v-c}{2\mu},1\Big\}\Big)$ (p. 39).

Significance

Proposition 4 identifies a trade-off. A PPC removes leakage entirely, but it also takes away the seller's ability to divert some buyers when the fee turns out to be too high, so the seller may refuse to participate. When the baseline state is unlikely and switching costs in it are high, the marketplace earns more by tolerating leakage and charging the full surplus $v-c$ . In every other case the clause pays. This makes the welfare and competition-policy debate about parity clauses explicit in a two-parameter region. It also contrasts with the case without uncertainty, where a PPC is always better for the marketplace.

The paper's proof (§8.5, pp. 39–40) is a short case comparison between closed forms. It has not been machine-checked. The printed formula for $\Pi^*$ when $q\ge 1/2$ omits the corner fee $f=v-c$ and is wrong for small $\mu$ . The conclusion $\Pi^*_{PPC}\ge\Pi^*$ still holds there, but by a different comparison. A formal proof pins down which steps survive.

Difficulty

Two optimizations are nested. The seller's optimal direct price changes regime at $f=2\mu$ , where the uniform distribution's kink binds. The marketplace's revenue without a PPC is therefore piecewise in $f$ , with an interior candidate $\mu/q$ that is feasible only when $q\ge 1/2$ . Under a PPC, revenue is discontinuous in $f$ because acceptance switches on and off. Its maximum is attained only because acceptance is weak. Comparing the two values requires a case split over $q\gtrless\tfrac12$ and $\mu$ against $(v-c)/2$ and $q(v-c)$ , and the boundary cases include genuine ties ( $\Pi^*=\Pi^*_{PPC}$ for $q<\tfrac12$ , $\mu\le\frac{v-c}{2}$ ). Reading off a single printed closed form for $\Pi^*$ fails in part of the $q\ge 1/2$ region.

Formalization scope

All objects are in one definitions file in namespace MarketplaceLeakage.Parity. The parameters are real numbers v c μ q, with standing hypotheses c < v, 0 < μ, 0 < q, q ≤ 1 on every theorem. The paper states $v>c$ (p. 5) and $\mu>0$ (p. 9). $q\in(0,1]$ is added: $q$ is a probability, and at $q=0$ both values equal $v-c$ , so the "if" direction of the goal fails. $q=1$ is allowed. The statements use the reduced seller problem (1), as the paper does after its Lemma 1 (p. 7), with $p_m=v$ . Lemma 1 itself is not posed.

Committed conventions:

$G$ is the clamped uniform CDF.
Seller-optimality is a predicate (IsSOpt), not a formula.
$\Pi^*_{PPC}$ (IsPPCValue) is the attained maximum of $f\cdot(q\,\mathbf 1[\text{accept}_B]+(1-q)\,\mathbf 1[\text{accept}_N])$ over all $f\in\mathbb R$ . Acceptance is weak and is stated against every delisting price $c\le p_d\le v$ .
$\Pi^*$ (IsNoPPCValue) is the attained maximum of $f(1-qG(v-p_d))$ over $f\le v-c$ and seller-optimal $p_d$ .
"Prefers not to impose" is strict; "otherwise prefers to impose" is weak.

These choices rule out the trivializing formalizations. Neither value is defined by its printed max-expression, which would make the milestones definitional. Strict acceptance would leave the PPC optimum unattained. A value given by sSup would be meaningless off its domain. Reading "prefers to impose" strictly would make the statement false at the ties.

No published platform definitions are reused. A complete development needs only elementary real analysis: maximizing piecewise-quadratic functions, attainment on compact intervals, and case analysis over min/max. The lemmas on the seller's best response under the uniform $G$ are reusable in the companion missions on Propositions 1–3 of the same paper. Proofs of any milestone are welcome independently.

Selected references

A. Hagiu, J. Wright, Marketplace Leakage, Management Science, 2023 (authors' manuscript dated March 2023). https://doi.org/10.1287/mnsc.2023.4757

6 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics·Captain: mikedeng1

Sharing Sequentially Triggered Losses: Automated Conflict Resolution Through Smart Contracts 1: Additive, Zero-Truncating, Merging-Proof, Population-Monotonic Rules Are the Fixed-Fraction RulesResearch Paper

Motivation

Contract breaches in supply chains rarely stay isolated. A supplier that delivers late forces its customer to breach its own downstream contract, which in turn harms the next firm, and so on. Each firm in such a chain both suffers a loss and causes one, and a court, an arbitrator or a self-executing smart contract has to decide who pays for what. Gudmundsson, Hougaard and Ko (Management Science 70(3), 2024) treat this as an axiomatic cost-sharing problem. The two classical readings of strict liability are extremes: under direct liability every agent pays exactly the loss it causes, and under indirect liability the initiator of the chain pays everything. The paper asks which compromises between the two are justified by normative requirements that are simple enough to be written into a contract, and answers that the requirements single out a one-parameter family, the fixed-fraction rules.

This mission formalizes that characterization (Theorem 1 of the paper) together with the two propositions and the lemma its proof rests on, and the examples showing that none of the four axioms is redundant.

Setting

A loss chain has agents $1,\dots,n$ . Agent $1$ initiates the chain, and agent $i$ causes a loss $\ell_i\ge 0$ to agent $i+1$ ; agent $n+1$ only suffers. A loss problem is a vector $\ell=(\ell_1,\dots,\ell_n)\in L^n=\mathbb R^n_{\ge0}$ with total $L=\ell_1+\dots+\ell_n$ .

An allocation $x\in X(\ell)$ assigns liabilities $x_i\ge0$ such that no initial segment of the chain pays less than the losses it caused, and the liabilities balance the total loss:

x_1+\dots+x_m\ge \ell_1+\dots+\ell_m\ (m<n),\qquad x_1+\dots+x_n=L.

A rule $\varphi$ assigns to every problem $\ell\in L^n$ , for every $n$ , an allocation $\varphi(\ell)\in X(\ell)$ , and is continuous along rays: $\varphi(a\ell)\to\varphi(\ell)$ as $a\to1$ .

For $\lambda\in[0,1]$ the fixed-fraction rule $\varphi^\lambda$ (Definition 1) charges every agent the fraction $\lambda$ of the loss it causes and the initiator in addition the residual:

\varphi^\lambda_1(\ell)=\lambda\ell_1+(1-\lambda)L,\qquad \varphi^\lambda_i(\ell)=\lambda\ell_i\ (i\ge2).

The elementary problem $e_n=(0,\dots,0,1)\in L^n$ has a single unit loss caused by the last agent.

The four axioms are:

Additivity: $\varphi(\ell)+\varphi(\ell')=\varphi(\ell+\ell')$ .
Zero truncation: $\varphi_i(\ell_1,\dots,\ell_n,0)=\varphi_i(\ell)$ for $i\le n$ .
Population monotonicity: for $1\le j<n$ and $1\le i\le j<k\le n$ , $\varphi_i(e_n)\ge\varphi_i(e_{n+1})$ and $\varphi_k(e_n)\ge\varphi_{k+1}(e_{n+1})$ , where $e_{n+1}$ is $e_n$ with a zero loss inserted after agent $j$ .
Merging proofness: $\varphi_i(e_3)+\varphi_{i+1}(e_3)\le\varphi_i(e_2)$ for $i=1,2$ .

Formalization targets

Goal: Theorem 1

A rule $\varphi$ satisfies additivity, zero truncation, merging proofness and population monotonicity if and only if there is $\lambda\in[0,1]$ with

\varphi(\ell)=\varphi^\lambda(\ell)\qquad\text{for every } n \text{ and every } \ell\in L^n .

Milestones

In attack order:

$\varphi^\lambda$ is a rule for $\lambda\in[0,1]$ (p. 8).
Lemma 1: an additive rule is scale invariant, $\varphi(\alpha\ell)=\alpha\varphi(\ell)$ for $\alpha\ge0$ .
Under zero truncation, agents after a single loss carry no liability.
Proposition 1: additivity and zero truncation hold iff $\varphi_i(\ell)=\sum_{j\ge i}\ell_j\,\varphi_i(e_j)$ .
Merging proofness forces $\varphi_2(e_3)=0$ .
Under population monotonicity and merging proofness, $\varphi_i(e_n)=0$ for $1<i<n$ .
Under the same axioms, $\varphi_1(e_n)=\varphi_1(e_2)$ and $\varphi_n(e_n)=\varphi_2(e_2)$ .
Proposition 2: population monotonicity and merging proofness hold iff $\varphi(e_n)=\varphi^\lambda(e_n)$ for some $\lambda\in[0,1]$ and all $n$ .

The proposal also contains four companion statements from Appendix B, which are not milestones: the serial rule $\varphi^A$ and the rules $\varphi^B,\varphi^C,\varphi^D$ each satisfy three of the axioms and violate the fourth.

Significance

Theorem 1 justifies a whole family of liability rules from four requirements, each of which has a concrete meaning: liability does not depend on how a loss is split into components, adding trailing zero losses changes nothing, adding agents without new losses makes no old agent worse off, and two consecutive agents cannot lower their joint liability by merging. The parameter $\lambda$ is left free, and the paper then uses separate arguments (equidistance from ideal allocations, the Shapley value and the nucleolus of an associated game; the later missions of this series) to single out $\lambda=1/2$ . Theorem 4 of the paper extends the characterization from chains to loss trees and relies on the same propositions.

A machine-checked proof of Theorem 1 adds an axiomatic cost-sharing layer to the platform, with reusable definitions of loss problems, allocations, continuous rules and the four axioms. It also fixes the axiom in a form under which the theorem is true: the manuscript's population-monotonicity axiom, read with its printed range, makes Theorem 1 false (see below). The result is proved in the paper; it has not been formalized before.

Difficulty

The proof combines three different kinds of argument. Additivity on the cone $L^n$ yields homogeneity only for rational factors; the step to real factors uses the weak, ray-wise continuity of rules, and needs care because continuity is only assumed at loss vectors, near the factor $1$ . The reduction to elementary problems decomposes a problem into single-loss problems and moves between problems of different lengths with zero truncation, so statements about vectors of different dimensions have to be related. Finally, the values on elementary problems are pinned down by population monotonicity, which compares problems of consecutive lengths only, so that information about $e_2$ and $e_3$ has to be carried to every $e_n$ . Without the case $j=1$ of the axiom the chain from $e_2$ to $e_3$ breaks, and the conclusion fails.

Formalization scope

Agents are Fin n, 0-based: the paper's agent $i$ is index $i-1$ . A rule is φ : (n : ℕ) → (Fin n → ℝ) → (Fin n → ℝ), a total function. IsRule φ requires, for every $n$ and every $\ell\ge0$ , that $\varphi(\ell)\in X(\ell)$ and $\varphi(a\ell)\to\varphi(\ell)$ as $a\to1$ in the product topology. Only values on loss vectors carry meaning. Every axiom quantifies over loss vectors only, and every conclusion " $\varphi=\varphi^\lambda$ " is agreement on every $\ell\ge0$ , never an equality of Lean functions, which would be false for an arbitrary extension of $\varphi$ to $\mathbb R^n$ .
$(\ell,0)$ is Fin.snoc ℓ 0; $n=0$ is admitted and adds nothing. $\lambda\in[0,1]$ is part of the conclusion of Theorem 1 and Proposition 2, not a hypothesis.
Correction. The manuscript prints Axiom 3 with $1<j<n$ . With that range the rule with $\varphi(e_2)=(\tfrac12,\tfrac12)$ , $\varphi(e_3)=(\tfrac12,0,\tfrac12)$ and $\varphi(e_n)=(\tfrac14,0,\dots,0,\tfrac12,\tfrac14)$ for $n\ge4$ , extended by Proposition 1, satisfies all four axioms but is no fixed-fraction rule. The paper's own consequences of the axiom (p. 11) and its proof of Proposition 2 use $j=1$ , so the axiom is formalized with $1\le j<n$ , exactly as the union over those $j$ ; it is not strengthened to all $i,k$ , which every $\varphi^\lambda$ with $\lambda<1$ would violate.
The manuscript leaves $\varphi^C$ undefined for $n=1$ and $\varphi^D$ undefined at $L=0$ ; the forced readings $\varphi^C(\ell_1)=(\ell_1)$ and $\varphi^D(0)=0$ are used.
Dropping the allocation condition or the continuity clause from IsRule changes the theorem (without $X(\ell)$ , $\lambda$ need not lie in $[0,1]$ ); both are hypotheses of every statement about an arbitrary rule.

Needed infrastructure: finite sums over Fin n with filters, Fin.snoc/Fin.castSucc/Fin.succ bookkeeping, and a density argument from $\mathbb Q$ to $\mathbb R$ with filters. The definitions are written to be shared with the other missions of this series. Proofs of the milestones in any order are welcome.

Selected references

J. Gudmundsson, J. L. Hougaard, C. Y. Ko, Sharing Sequentially Triggered Losses: Automated Conflict Resolution Through Smart Contracts, Management Science 70(3), 1773–1786, 2024 (accepted manuscript 2023). https://doi.org/10.1287/mnsc.2023.4772
J. L. Hougaard, J. D. Moreno-Ternero, M. Tvede, L. P. Østerdal, Sharing the proceeds from a hierarchical venture, Games and Economic Behavior 102, 98–110, 2017 (geometric rules; cited on p. 11 of the paper).
W. Thomson, Fair allocation, in M. D. Adler, M. Fleurbaey (eds.), The Oxford Handbook of Well-Being and Public Policy, Oxford University Press, ch. 7, 193–226, 2016 (population monotonicity; cited on p. 10).
L. S. Shapley, A value for n-person games, in H. Kuhn, A. Tucker (eds.), Contributions to the Theory of Games II, Princeton University Press, 307–317, 1953 (additivity; cited on p. 9).

12 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research+1·Captain: mikedeng1

Marketplace Leakage 2: Optimal Investment in Transaction Benefits Decreases in Its Cost and Is First Constant, Then Decreasing, Then Increasing in Switching CostsResearch Paper

Why marketplaces worry about leakage

Online marketplaces for services (home repair, tutoring, beauty appointments, freelancing) earn a fee on each transaction they intermediate. After a buyer has found a seller on the marketplace, both sides can often complete the transaction, or the next one, off the platform and avoid the fee. This leakage (also called disintermediation) is a central constraint on how such platforms price, and platforms respond to it in several ways: lower fees, bans on exchanging contact details, price-parity clauses, and investment in features that make transacting on the platform itself more valuable (payment protection, scheduling, reminders, dispute handling).

A. Hagiu and J. Wright, Marketplace Leakage (Management Science, 2023), build a minimal model of a marketplace, a seller and buyers with heterogeneous costs of buying directly, and compare these responses. This mission formalizes the paper's analysis of the last one: investing in transaction benefits (§5.1 and Proposition 2).

Setting

There is one marketplace $M$ , one seller $S$ and a unit mass of buyers who each want one unit of $S$ 's product. Every buyer values the product at $v$ ; $S$ 's marginal cost is $c$ , with $c < v$ ; the outside option is worth $0$ . A buyer who buys directly from $S$ instead of through $M$ bears a switching cost $s$ , drawn from the uniform distribution on $[0,\mu]$ with $\mu > 0$ :

G(s) = \min\{\max\{s/\mu, 0\}, 1\}.

The marketplace first chooses a transaction benefit $b \ge 0$ , which buyers receive when they buy on $M$ , at cost $K(b) = \tfrac{k}{2} b^2$ with $k > 0$ , and a per-transaction fee $f$ . Following the paper (p. 12), the marketplace's feasible choices are $b \ge 0$ and $b \le f \le v - c + b$ . Given $(b,f)$ , the seller lists on $M$ at price $p_m = v + b$ and sets a direct price $p_d \le v$ to maximize

\pi_b(f,p_d) = (p_d - c)\,G(v - p_d) + (v + b - c - f)\,\bigl(1 - G(v - p_d)\bigr).

The leakage is $G(v - p_d)$ , the share of buyers who buy directly. The marketplace earns

\Pi(b,f,p_d) = f\,\bigl(1 - G(v - p_d)\bigr) - \tfrac{k}{2} b^2 .

An optimum is a triple $(b,f,p_d)$ with $(b,f)$ feasible, $p_d$ seller-optimal at $(b,f)$ , and no feasible $(b',f')$ with seller-optimal $p_d'$ giving the marketplace more. The Lean development uses the same letters: G μ s, sProfitB, IsSOptB, MProfitB, leakage, IsOpt, and the threshold

\bar\mu = \frac{v-c}{2} + \frac{1}{4k} + \sqrt{\Bigl(\frac{v-c}{2}\Bigr)^2 + \frac{1}{16k^2}} \quad (\texttt{muBar}).

Formalization targets

Goal: Proposition 2 (p. 12)

An optimum exists, and at every optimum

b^* = \begin{cases} 1/k & \mu \le 1/(2k), \\ 1/\bigl(2k - 1/(2\mu)\bigr) & 1/(2k) \le \mu \le \bar\mu, \\ 1/k - (v-c)/(2k\mu) & \mu \ge \bar\mu. \end{cases}

Moreover $b^*$ is strictly decreasing in $k$ ; for fixed $k$ it is constant in $\mu$ on $(0, 1/(2k)]$ (with zero leakage there), strictly decreasing on $[1/(2k), \bar\mu]$ (with strictly increasing leakage), and strictly increasing on $[\bar\mu, \infty)$ (with strictly decreasing leakage).

Milestones (Appendix §8.3, pp. 34–37)

The seller's optimal direct price: $p_d^*(f) = v - \mu$ if $f \ge b + 2\mu$ and $v - (f-b)/2$ if $b \le f \le b + 2\mu$ (p. 34).
The marketplace's profit $\Pi(b,f)$ at that response (p. 34).
The value $\Pi(b)$ of the inner maximization over $f$ , in three regimes (p. 35).
$\bar\mu > \max\{v-c, 1/(2k)\}$ , and the translation of the thresholds on $k$ into thresholds on $\mu$ (pp. 36–37).
The equilibrium fee, direct price and profit in the three regimes (p. 37).

Significance

Proposition 2 says that a marketplace's investment against leakage is non-monotone in how costly leakage is for buyers. When switching costs are small, the marketplace invests enough ( $b^* = 1/k$ ) to remove leakage entirely and charges a fee equal to the benefit. For intermediate switching costs it tolerates growing leakage and invests less. For large switching costs, where the fee is pinned at the seller's participation constraint, it again invests more as leakage falls. Leakage itself is zero, then rising, then falling in switching costs, so the comparative static that matters for platform design (how much leakage to tolerate) is not monotone in the parameter that measures how attached buyers are to the platform.

The result is proved in the paper by an explicit case analysis. As far as known, it has no machine-checked proof. A complete formalization certifies the closed forms, the joint optimality over $(b,f)$ (not just the first-order conditions), and the strictness of each comparative-static claim, including across the regime boundaries $1/(2k)$ and $\bar\mu$ , which the paper treats as "easily seen".

Difficulty

Every step is elementary, but the obvious argument through first-order conditions is incomplete. For fixed $b$ the inner problem in $f$ has a kink at $f = b + 2\mu$ and corners at $f = b$ and $f = v - c + b$ , so $\Pi(b)$ is piecewise with three regimes. $\Pi(b)$ is not concave when $k < 1/(4\mu)$ and $\mu > v - c$ : its derivative first decreases, then increases, then decreases, and showing that $b^* = 1/k$ is the unique global maximizer requires comparing values across the pieces. The paper's case split is on $k$ for fixed $\mu$ ; the proposition is stated in $\mu$ for fixed $k$ , and translating one into the other needs the root structure of a quadratic in $\mu$ . Strict monotonicity in $k$ has to hold across regime changes, where the formula for $b^*$ changes.

Formalization scope

Primitives. Real parameters $v, c, \mu, k$ with standing hypotheses $c < v$ , $\mu > 0$ , $k > 0$ (pp. 5, 9, 12). Nothing is assumed about the sign of $c$ .
Reduced game. The statements use the seller's reduced problem written after Lemma 1 ( $p_m = v + b$ , $p_d \le v$ ), as the paper does. Lemma 1 itself is not posed: as printed it holds only up to payoff-equivalent choices of $p_m$ .
Feasible set. $b \ge 0$ , $b \le f \le v - c + b$ , exactly as in the paper's $\Pi^*$ (p. 12).
Distribution. $G$ is the clamped uniform CDF; its kinks carry the case analysis.
Optimality. The seller's response is the predicate IsSOptB; the marketplace's optimum is the predicate IsOpt over the joint choice $(b,f)$ . No closed form for $p_d^*$ , $f^*$ or $b^*$ is a definition; "max" is stated by attainment (IsGreatest), never by an unattained supremum. Comparative statics compare optimal choices at two parameter values, not formulas.
One printed slip is corrected: the third case of $\Pi(b)$ (p. 35) is used only for $b \le 2\mu - 2(v-c)$ ; with the printed $\max\{\cdot, 0\}$ it would wrongly apply at $b = 0$ when $\mu < v - c$ . The third case of $\Pi(b,f)$ (p. 34) is the second at $f = b$ and is not stated separately.

A formalization that defined $b^*$ or the seller's response by its cases, stated the comparative statics about the closed-form formulas alone, or replaced "max" by an unattained supremum would trivialize the mission and is ruled out. Contributions welcome: proofs of the milestones, and reusable lemmas on maximizing piecewise quadratics.

Selected references

A. Hagiu, J. Wright, Marketplace Leakage, Management Science, 2023. https://doi.org/10.1287/mnsc.2023.4757 (formalized from the authors' manuscript dated March 2023).

8 thms2 active usersReviewed

Linear algebra Linear Optimization Theoretical Computer Science·Captain: mikedeng1

A Strongly Polynomial Algorithm for Linear Exchange Markets II: A Z₊-Matrix Polyhedron P_M Lies Between an M2VPI Polyhedron and Its Scaling by B²Research Paper

Motivation

In a linear exchange market every agent owns one divisible good and has linear utilities over all goods; an equilibrium is a price vector at which every agent can spend its budget on goods that maximize utility per unit of money, and all goods are sold. Computing such an equilibrium in strongly polynomial time, with a number of arithmetic operations bounded by a polynomial in the number of agents alone, was an open question until Garg and Végh (arXiv:1809.06266; Operations Research, 2023). Their algorithm alternates two kinds of phases. One identifies "revealed" edges that appear in every equilibrium (the subject of mission I of this series). The other computes good starting prices for the current set of revealed edges by solving a linear program whose constraint matrix has a special sign structure.

No strongly polynomial algorithm is known for that linear program. Systems in which every inequality has at most one positive and at most one negative coefficient, by contrast, are strongly polynomially solvable (Megiddo, 1983; Hochbaum and Naor, 1994). The paper bridges the gap with Theorem 6.4: a polyhedron given by a $Z_+$ -matrix is sandwiched between a monotone two-variable-per-inequality polyhedron and its scaling by an explicit factor $B^2$ . This mission formalizes that theorem and the lemmas of §7 that prove it. It is a statement about matrices and polyhedra only; no market notions enter.

Setting

Matrices are rational. For integers $k, t \ge 0$ a matrix $M \in \mathbb{Q}^{k\times t}$ is a $Z_+$ -matrix, written $M \in \mathcal{Z}_+(k,t)$ , if every off-diagonal entry is nonpositive and every column sum is nonnegative:

M_{ij} \le 0 \quad (i \ne j), \qquad \sum_{i=1}^k M_{ij} \ge 0 \quad (j \in [t]).

For a non-square matrix the diagonal entries are the $M_{ii}$ with $1 \le i \le \min\{k,t\}$ . Square $Z_+$ -matrices are exactly the transposes of weighted Laplacians of directed graphs, or such transposes with one row and column deleted.

$\mathcal{M}_2(m,t)$ is the set of $m\times t$ rational matrices with at most one positive and at most one negative entry in every row. A system $\bar M x \le \bar b$ with $\bar M \in \mathcal{M}_2(m,t)$ is a monotone two-variable-per-inequality system (M2VPI).

For $M \in \mathcal{Z}_+(k,t)$ and $b \in \mathbb{Q}^k$ with $b > 0$ , the polyhedron of interest is

P_M = \{x \in \mathbb{R}^t : Mx \le b,\ x \ge 0\}.

Write $\ell$ for the number of nonzero entries of $M$ , $\alpha P = \{\alpha x : x \in P\}$ for $\alpha > 0$ , and

B = \frac{\sum_{j=1}^k b_j}{\min_{i\in[k]} b_i}.

In §7 the right-hand side is called $\gamma$ instead of $b$ , and $\lambda_i = \sum_{j\ne i}\gamma_j$ .

The proof works with a square $M \in \mathcal{Z}_+(t,t)$ with positive diagonal. Its digraph $([t],H)$ has an arc $ij$ whenever $M_{ij} < 0$ . $D_i$ is the set of vertices reachable from $i$ (including $i$ ), and $M^{(i)}$ is the submatrix of the rows $M_j$ , $j \in D_i$ . The vertices split into $T_1$ (at most one outgoing arc), $T_2$ (at least two arcs and $\operatorname{rk} M^{(i)} = |D_i|$ ) and $T_3$ (at least two arcs and $\operatorname{rk} M^{(i)} < |D_i|$ ).

Formalization targets

Goal: Theorem 6.4 (p. 15)

For $M \in \mathcal{Z}_+(k,t)$ with $k \ge 1$ and $\ell$ nonzero entries, and $b \in \mathbb{Q}^k$ with $b > 0$ , there are $\ell' \le \ell$ , $\bar M \in \mathcal{M}_2(\ell',t)$ and $\bar b \in \mathbb{Q}^{\ell'}$ with

P_M \subseteq \{x \in \mathbb{R}^t : \bar Mx \le \bar b,\ x \ge 0\} \subseteq B^2 P_M.

Milestones (§7, pp. 16–23)

Lemma 7.1: for $M \in \mathcal{Z}_+(t,t)$ and $\bar p \ge 0$ with $M\bar p \le \gamma$ , $\ M\bar p \ge -\lambda \ge -(B-1)\gamma$ .
Lemma 7.2: the Gaussian elimination of the proof, run on $T \in \mathcal{Z}_+(\ell,t)$ , returns $T' = YT$ with $Y \ge 0$ , $T'$ upper triangular with diagonal entries in $\{0,1\}$ and nonpositive off-diagonal entries, and $T'_{kk} = 1$ whenever some $T_{ik} < 0$ with $i > k$ .
Claim 7.3(iii): for $i \in T_3$ , $M_i$ is a linear combination of $\{M_h : h \in D_i \setminus\{i\}\}$ .
Lemma 7.4(i): for $i \in T_2\cup T_3$ there is a unique $q^{(i)} \in \mathbb{R}^t_+$ with $M_\ell q^{(i)} = 0$ ( $\ell \in D_i\setminus\{i\}$ ), $q^{(i)}_i = 1$ and $q^{(i)}_\ell = 0$ off $D_i$ .
Lemma 7.4(iv) and (iii): points $r^{(i)} \in P_M$ tight on $D_i\setminus\{i\}$ (for $i \in T_3$ ) and on $D_i$ with $r^{(i)}_i = \kappa(i)$ (for $i \in T_2$ ).
Claim 7.5: $\kappa(i)\,M_i q^{(i)} \le B\gamma_i$ for $i \in T_2$ .
The reduced case (§7, p. 16): Theorem 6.4 for square $M$ with positive diagonal.

Significance

Theorem 6.4 turns an LP over a $Z_+$ constraint matrix, for which no strongly polynomial algorithm is known, into an M2VPI system that is strongly polynomially solvable, at the price of a factor $B^2$ . In the exchange-market algorithm $B \le n$ , so the starting prices of each phase come within a factor $n^2$ of optimal (the proof of Theorem 3.7, p. 15). That bound is what lets the potential argument advance in a polynomial number of phases. The construction is not specific to markets: any LP of the form $\max \sum_i x_i$ over $P_M$ with $M$ a $Z_+$ -matrix, which includes LPs over transposed weighted Laplacians of directed graphs, inherits the same approximation.

The result is proved in the paper; to our knowledge none of it has been machine-checked. A formalization produces a checked proof of the sandwich. It also produces reusable facts about Gaussian elimination on $Z_+$ -matrices (Lemma 7.2), which hold for any matrix whose off-diagonal entries are nonpositive and whose column sums are nonnegative.

Difficulty

The obvious approach, deleting all but two variables from each inequality of $P_M$ , fails: the dropped negative terms make the resulting system either too weak or invalid. The paper instead derives one new constraint per arc $ij$ of $H$ , as a nonnegative combination of the inequalities $M\bar p \ge -\lambda$ . Finding it requires an ordering of $D_i$ in which every vertex but $i$ has an in-neighbour placed after it, and an elimination on the permuted submatrix whose penultimate row has exactly two nonzero entries. The reverse containment $\{\bar M\bar p \le \bar b\} \subseteq B^2P_M$ is the hard direction. It splits by whether the rows on $D_i$ are linearly independent ( $T_2$ ) or not ( $T_3$ ), and the $T_2$ case needs the extra constraint $\bar p_i \le \kappa(i)$ and the comparison of entries of the elimination multipliers $Y^{(ij)}$ in Claim 7.5. Every step relies on a sign invariant of the elimination that Lemma 7.2 proves by induction.

Formalization scope

Indices are 0-based (Fin k, Fin t); the paper's $[n] = \{1,\dots,n\}$ . Matrices $M$ , $\bar M$ and right-hand sides $b$ , $\bar b$ , $\gamma$ are rational (ℚ), as on p. 15, and act on real vectors $x \in \mathbb{R}^t$ through the cast. A diagonal entry of a rectangular matrix is one whose two indices agree as natural numbers. $B^2P_M$ is the image $\{B^2x : x \in P_M\}$ . $B$ is defined for $k \ge 1$ only, and every statement using it assumes $k \ge 1$ (resp. $t \ge 1$ ).

Not formalized: the running time $O(\ell(\min\{k,t\})^3)$ and the polynomial bound on the encoding size of $\bar M$ , $\bar b$ in Theorem 6.4. The goal is the existence statement that the construction (13) witnesses. The standing assumptions of §7 ( $\gamma > 0$ ; positive diagonal after the reduction) appear as hypotheses of the milestones that live in that setting.

Lemma 7.2 is stated about the specific elimination of the proof (p. 17), defined explicitly; an existential "there is $Y \ge 0$ " form would be nearly trivial, since $Y = 0$ satisfies all but one clause. In the goal, $\bar M$ must have at most one positive and at most one negative entry per row, and $\ell' \le \ell$ . Dropping either requirement makes the goal weaker than the paper's theorem.

$\kappa(i)$ , defined in (12) through the elimination for an arbitrarily chosen arc, is restated intrinsically as the $i$ -th entry of $(M_{D_i,D_i})^{-1}\gamma_{D_i}$ , a number the paper shows equal (proof of Lemma 7.4(iii)). It is used only for $i \in T_2$ , where that block is invertible. Claim 7.3(i)–(ii) and Lemma 7.4(ii), which concern the elimination output for a particular arc, are not milestones.

A complete development needs the elimination and its invariants, reachability in a finite digraph, ranks of row submatrices, and the construction (13). The elimination lemmas are reusable for any $Z_+$ -matrix. Contributions are welcome on any milestone, on the reduction from rectangular $M$ to the square positive-diagonal case, and on the two containments of the reduced case.

Selected references

J. Garg and L. A. Végh, A strongly polynomial algorithm for linear exchange markets, arXiv:1809.06266v3, 2022; Operations Research, 2023. https://arxiv.org/abs/1809.06266
N. Megiddo, Towards a genuinely polynomial algorithm for linear programming, SIAM Journal on Computing 12(2), 1983. https://doi.org/10.1137/0212022
D. S. Hochbaum and J. Naor, Simple and fast algorithms for linear and integer programs with two variables per inequality, SIAM Journal on Computing 23(6), 1994. https://doi.org/10.1137/S0097539793251876
R. W. Cottle and A. F. Veinott, Jr., Polyhedral sets having a least element, Mathematical Programming 3, 1972. https://doi.org/10.1007/BF01584975

11 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

A Strongly Polynomial Algorithm for Linear Exchange Markets I: Over Revealed Edges, the Prices of an F-Equilibrium Support a Market EquilibriumResearch Paper

Motivation

The linear exchange market (the linear Arrow–Debreu model) is the basic model of general equilibrium with linear utilities: each agent brings goods to the market, sells them at the going prices, and spends the proceeds on the goods that give the most utility per unit of money. Computing its equilibrium is a classical problem in algorithmic game theory and in mathematical economics. Gale characterised when an equilibrium exists; Eaves (1976) gave a finite algorithm; Jain (2007) and Ye (2008) gave polynomial-time algorithms through convex programming and interior-point methods; Duan and Mehlhorn (2015) gave a combinatorial weakly polynomial algorithm, later improved by Duan, Garg and Mehlhorn (2016). Whether a strongly polynomial algorithm exists (described by Duan and Mehlhorn as a major open question), one whose number of arithmetic operations depends on the number of agents and goods only and not on the bit size of the utilities, remained open until Garg and Végh (arXiv:1809.06266, STOC 2019, Operations Research 2023).

The algorithm of Garg and Végh maintains a set $F$ of revealed edges, pairs (agent, good) that are known to be maximum bang-per-buck edges in every equilibrium, and enlarges $F$ until a relaxed equilibrium, an $F$ -equilibrium, is found. Two lemmas of §3–§4 of the paper make this work: a large money flow on an edge reveals it (Lemma 3.3), and an $F$ -equilibrium for revealed $F$ can be converted into a genuine market equilibrium at the same prices (Lemma 3.4). This mission formalizes these lemmas and the claims of their proofs.

Setting

There are $n$ agents $A=[n]$ and $n$ divisible goods $G=\{g_1,\dots,g_n\}$ , one unit of each; agent $i$ owns the unit of good $g_i$ . Agent $i$ has utility $u_{ij}\ge 0$ per unit of good $g_j$ . The edge set is $E=\{(i,g_j):u_{ij}>0\}$ , $m=|E|$ , and every agent and every good has an edge.

Given prices $p>0$ , agent $i$ 's budget is $p_i$ . The maximum bang-per-buck (MBB) edges are the edges $(i,g_j)\in E$ with

\frac{u_{ij}}{p_j}=\alpha_i:=\max_{g_k\in G}\frac{u_{ik}}{p_k},

and $\mathrm{MBB}(p)$ is their set. A money flow $f=(f_{ij})$ records how much agent $i$ spends on good $g_j$ . The pair $(p,f)$ is a money allocation if $p>0$ , $f\ge0$ , $\operatorname{supp}(f)\subseteq\mathrm{MBB}(p)$ , no agent spends more than $p_i$ and no good receives more than $p_j$ . The surplus of good $g_j$ is $s_j(p,f)=p_j-\sum_i f_{ij}$ , and $(p,f)$ is a market equilibrium if $\lVert s(p,f)\rVert_1=0$ .

The set $F^*\subseteq E$ consists of the edges that are MBB edges in every market equilibrium. For an edge set $F$ , an $F$ -allocation relaxes a money allocation: money may be negative on the edges of $F$ , and every edge of $F$ must be MBB. It is an $F$ -equilibrium if $\lVert s(p,f)\rVert_1=0$ . The potential of an $F$ -allocation is $\varphi(p,f)=\lVert s(p,f)\rVert_\infty/(\prod_j p_j)^{1/n}$ , and $\Psi(F)$ is its minimum over the $F$ -allocations supported on $F$ .

Formalization targets

Goal: Lemma 3.4 (p. 6)

If a market equilibrium exists, $F\subseteq F^*$ , and $(p,f)$ is an $F$ -equilibrium, then there is a money flow $f'$ such that

(p,f')\ \text{is a market equilibrium.}

Milestones (attack order)

Lemma 3.3 (p. 6): if $F\subseteq F^*$ , $(p,f)$ is an $F$ -allocation, $(k,g_\ell)\in E$ and $f_{k\ell}>\lVert s(p,f)\rVert_1$ , then $(k,g_\ell)\in F^*$ .
Corollary 4.1 (p. 8): if $F\subseteq F^*$ , every $F$ -equilibrium $(p,f)$ has $\operatorname{supp}(f)\subseteq F^*$ .
Ratio claim (proof of Lemma 3.4, p. 9): if $\bar E\subseteq\mathrm{MBB}(p)\cap\mathrm{MBB}(p')$ , then $p_j/p_k=p'_j/p'_k$ for goods $g_j,g_k$ in one connected component of the bipartite graph $(A\cup G,\bar E)$ .
Components claim (p. 9): with $\bar E=F\cup\operatorname{supp}(f)$ , $\alpha=\max_j p'_j/p_j$ , $T$ the goods attaining $\alpha$ and $S$ the agents with an MBB edge at $p'$ into $T$ , the set $S\cup T$ is a union of connected components of $(A\cup G,\bar E)$ .
Block claim (p. 9): $\sum_{i\in S}p'_i=\sum_{g_j\in T}p'_j$ and $T=\{g_j: j\in S\}$ .

A further item, Lemma 3.9 (p. 7), is the progress step of the overall algorithm: if $\varphi(p,f)<\Psi(F)/(n(m+1))$ , some edge of $E\setminus F$ joining two components of $F$ carries more than $\lVert s(p,f)\rVert_1$ . It is not used by the goal and is not a milestone.

Significance

Lemma 3.4 is the termination step of the first strongly polynomial algorithm for linear exchange markets: the algorithm only ever needs to find an $F$ -equilibrium for a set $F$ of revealed edges, and Lemma 3.4 turns it into an equilibrium by one maximum-flow computation. Lemma 3.3 is the step that reveals new edges, and Lemma 3.9 is the step that guarantees one is revealed in every round. Together they reduce the computation of an equilibrium to a sequence of relaxed problems on a growing set of known edges; the paper notes (p. 3) that Lemma 3.3 is analogous to the identification of abundant arcs in Orlin's strongly polynomial minimum-cost flow algorithm.

The results are proved in the paper. As far as known, none of them, nor the linear exchange market model with money flows and MBB edges, has a machine-checked formalization. This mission produces the model as a reusable definition layer (markets, MBB edges, money allocations, equilibria, revealed edges, $F$ -allocations, the potential $\varphi$ ), and machine-checked proofs of the structural lemmas behind the algorithm. The proof of Lemma 3.4 in the paper ends with "repeat the same analysis on the remaining set of agents and goods", an induction the paper leaves informal; a formal proof makes it explicit.

Difficulty

The equilibrium $(p',f')$ used in the proofs is an arbitrary one, with prices unrelated to $p$ . The obvious attempt at Lemma 3.4, rounding the negative entries of $f$ to zero, breaks the budget and market-clearing equalities. The paper's argument instead compares $p$ with $p'$ through the maximal price ratio $\alpha$ , shows that the agents $S$ and goods $T$ of maximal ratio form a block that trades only internally both at $p$ and at $p'$ , and then removes the block and recurses. The step " $S\cup T$ is a union of components" is asserted in the paper without proof, and the recursion requires carrying an equilibrium of the remaining submarket. Lemma 3.3 is a counting argument over a set of goods whose prices increase; its sign bookkeeping, and the use of negative flows only on edges of $F$ , are where an informal reading goes wrong.

Formalization scope

Agents and goods are both indexed by Fin n (0-based), so the good owned by agent i has index i; the bipartite graph $(A\cup G,\cdot)$ lives on Fin n ⊕ Fin n with agents on the left and goods on the right. Utilities, prices and money are real. Every allocation predicate requires every price to be positive, and an MBB edge must have $u_{ij}>0$ . $\lVert s\rVert_1$ keeps the absolute values of the paper's norm. $F^*$ quantifies over all market equilibria, so it equals $E$ when the market has none. $\Psi(F)$ is taken as an infimum: it is the paper's minimum when the minimum exists and $0$ when no $F$ -allocation is supported on $F$ , which makes Lemma 3.9 vacuous, not false, in that case.

The paper's running-time claims (Theorem 3.1, the " $O(nm)$ time" of Lemma 3.4) are out of scope; the goal poses the existence of $f'$ that the maximum-flow computation witnesses. The goal adds the hypothesis that some market equilibrium exists. The paper guarantees one through its standing assumption $(\star)$ (strong connectivity of the digraph of positive utilities) and Gale's cited existence criterion; the hypothesis is what the proof uses and makes the statement more general. It cannot be dropped: without an equilibrium $F^*=E$ , and there are markets with an $E$ -equilibrium and no market equilibrium. A formalization in which a market equilibrium could carry negative money or nonzero surplus would make the goal trivial and is ruled out by the definitions: a money allocation has $f\ge0$ on every pair and an equilibrium has $\lVert s\rVert_1=0$ .

A complete development needs finite sums, real division, connectivity in a SimpleGraph (SimpleGraph.Reachable), and an induction on the number of agents for Lemma 3.4. The market definitions are reusable for any work on linear Fisher or exchange markets. Contributions welcome: proofs of the milestones, of the goal, of Lemma 3.9, and a formalization of the existence criterion (Lemma 2.3).

Selected references

J. Garg and L. A. Végh, A strongly polynomial algorithm for linear exchange markets, arXiv:1809.06266v3, 2022; Operations Research, 2023. https://arxiv.org/abs/1809.06266
D. Gale, The linear exchange model, Journal of Mathematical Economics 3 (1976) 205–209. https://doi.org/10.1016/0304-4068(76)90029-X
B. C. Eaves, A finite algorithm for the linear exchange model, Journal of Mathematical Economics 3 (1976) 197–203. https://doi.org/10.1016/0304-4068(76)90028-8
K. Jain, A polynomial time algorithm for computing an Arrow–Debreu market equilibrium for linear utilities, SIAM Journal on Computing 37 (2007) 303–318. https://doi.org/10.1137/S0097539705447384
Y. Ye, A path to the Arrow–Debreu competitive market equilibrium, Mathematical Programming 111 (2008) 315–348. https://doi.org/10.1007/s10107-006-0065-5
R. Duan and K. Mehlhorn, A combinatorial polynomial algorithm for the linear Arrow–Debreu market, Information and Computation 243 (2015) 112–132. https://doi.org/10.1016/j.ic.2014.12.009
J. B. Orlin, A faster strongly polynomial minimum cost flow algorithm, Operations Research 41 (1993) 338–350. https://doi.org/10.1287/opre.41.2.338

8 thms2 active usersReviewed

Completed

Linear Optimization Operations Research Probability+1·Captain: mikedeng1

Selection and Ordering Policies for Hiring Pipelines via Linear Programming 2: An LP-Rounding Policy That Sends Offers in Parallel Lists Earns at Least (1 − 1/e) Times the LP BoundResearch Paper

Motivation

Firms that hire for several roles at once face a timing problem. An offer occupies a candidate until they answer, a candidate can hold only one offer, and the hiring season has a fixed number of decision rounds. Sending offers one at a time is slow; sending them all at once risks over-hiring. Epstein and Ma (arXiv:2210.04059v3, Operations Research 2024) study three stylised models of this pipeline: interviewing with a cap on interviews (ProbeTop- $k$ ), offering in parallel rounds, and offering all at once. This mission formalizes their result for the second model, the Parallel Offering problem.

The question belongs to the literature on stochastic probing and LP-based approximation of adaptive policies. The Sequential Offering model of Purohit, Gollapudi and Raghavan (2019) sends one offer per round for identical positions. Parallel Offering lets each unfilled position send one offer per round, with heterogeneous positions, and asks how much a simple, non-adaptive policy loses against the best adaptive one.

Setting

A firm fills $k$ positions from $n$ candidates within $T$ rounds. Candidate $i\in[n]$ accepts an offer for position $j\in[k]$ with probability $p_{ij}$ and then adds the value $v_{ij}$ . An instance is $I=(k,T,n,p,v)$ with

1\le k\le T\le n,\qquad p\in[0,1]^{n\times k},\qquad v\in\mathbb R_+^{n\times k}.

In each round the firm may send one offer for every unfilled position, and each candidate receives at most one offer in total. Before the rounds start, each candidate $i$ has decided the set $A_i\subseteq[k]$ of positions they would accept, with $\mathbb P(j\in A_i)=p_{ij}$ . These decisions may be correlated across the positions of one candidate and are independent across candidates.

The linear program $\mathrm{LP}_{\mathrm{par}}(I)$ has a variable $y_{ij}$ for the probability that candidate $i$ is offered position $j$ :

\max\ \sum_{j=1}^k\sum_{i=1}^n v_{ij}y_{ij}p_{ij}\quad\text{s.t.}\quad \sum_i y_{ij}\le T,\quad \sum_i y_{ij}p_{ij}\le 1\ \ (\forall j),\qquad \sum_j y_{ij}\le 1\ \ (\forall i),\qquad 0\le y_{ij}\le 1.

The paper shows (Lemma 6) that its value bounds the expected reward of every policy.

The dependent rounding of Gandhi, Khuller, Parthasarathy and Srinivasan (2006) takes a bipartite graph with edge weights $x_e\in[0,1]$ and outputs random indicators $X_e\in\{0,1\}$ with (P1) $\mathbb E X_e=x_e$ ; (P2) every vertex degree $\sum_{e\ni u}X_e$ is the floor or the ceiling of its fractional degree, with probability 1; (P3) for every vertex $u$ , every set $S$ of edges at $u$ and every $c\in\{0,1\}$ , $\mathbb P(\bigcap_{e\in S}\{X_e=c\})\le\prod_{e\in S}\mathbb P(X_e=c)$ .

The algorithm $\mathrm{ALG}_{\mathrm{par}}$ solves $\mathrm{LP}_{\mathrm{par}}(I)$ to optimality, rounds the optimal $y$ on the complete bipartite graph candidates $\times$ positions, and puts candidate $i$ on the list of position $j$ iff $Y_{ij}=1$ . Every list is then run in parallel, in decreasing order of $v_{ij}$ : position $j$ offers to the next candidate on its list each round until someone accepts, the list ends or the $T$ rounds are over. $R_{\mathrm{ALG}_{\mathrm{par}}}(I)$ is its expected total value.

For the analysis, $D_j=\{i: Y_{ij}=1,\ j\in A_i\}$ is the set of candidates on list $j$ who would accept, $v^*_j(S)=\max_{i\in S}v_{ij}$ (zero on the empty set), $\tilde D_j$ is the same set built from independent Bernoulli( $y_{ij}$ ) variables instead of $Y_{ij}$ , and $L^*_j=\sum_i v_{ij}y_{ij}p_{ij}$ .

Formalization targets

Goal: Theorem 2

R_{\mathrm{ALG}_{\mathrm{par}}}(I)\ \ge\ \Big(1-\frac1e\Big)\,\mathrm{LP}_{\mathrm{par}}(I)\qquad\text{for every } I\in\mathcal I_{\mathrm{par}}.

The constant is tight (App. C.5 of the paper), so the goal states the paper's result in its final form.

Milestones

Properties (a) and (b) (§5.2): with probability 1 every list has at most $T$ candidates and every candidate is on at most one list.
$L_j=\mathbb E\,v^*_j(D)$ (§5.3): the expected value hired for position $j$ is the expected best value among the accepting list members.
Lemma 7: $\mathbb E\,v^*_j(D)\ge\mathbb E\,v^*_j(\tilde D)$ for every position $j$ .
Lemma 8: $\mathbb E\,v^*_j(\tilde D)\ge(1-1/e)L^*_j$ for every position $j$ .
Lemma 9 (companion, §5.4): if all positions are identical, $\mathrm{LP}_{\mathrm{par}}(I)=\mathrm{LP}_{\mathrm{seq}}(I')$ , where $I'$ is the Sequential Offering instance with the same candidates and a budget of $kT$ offers.

Significance

Theorem 2 shows that a non-adaptive policy, fixed before any offer is answered, earns at least $1-1/e\approx0.632$ of the LP bound, hence of the best adaptive policy, for heterogeneous positions and with acceptance decisions correlated across positions. Through Lemma 9 it also bounds the cost of batching: $T$ parallel rounds lose at most a factor $1-1/e$ against $kT$ sequential offers (Corollary 3 of the paper).

The results are proved in the paper; none of them is formalized. The mission adds to the platform a reusable statement of the GKPS rounding properties on bipartite graphs, an explicit finite model of a parallel offering process computed from its run, and a $(1-1/e)$ LP-rounding guarantee that a solver must connect end to end: the algorithm's reward, the per-position reduction, the comparison with independent rounding, and the bound for independent rounding.

Difficulty

The obvious first step, replacing the dependent rounding by independent rounding with the same marginals, is not free: the rounding couples the candidates of a list, and an expected maximum is not linear in the indicators. Only the negative correlation of the rounding at a single position rescues it, and the paper notes (App. C.3) that (P1) and (P3) alone do not suffice once several identical positions are pooled, so the argument is genuinely per position. The written proof of Lemma 7 (p. ec10) has a sign error and a wrong indicator; the statement is correct. Independent rounding then still has to be compared with the LP: the LP only controls each list in expectation, through $\sum_i y_{ij}p_{ij}\le1$ , while the algorithm collects at most one value per list.

Formalization scope

Candidates are Fin n, positions Fin k, all quantities real. All randomness is finite: an expectation is an explicit sum over the rounded edge set $Y\subseteq[n]\times[k]$ , weighted by a distribution $\mu$ , and over acceptance profiles $(A_i)_i$ , weighted by $\prod_i\mathrm{acc}_i(A_i)$ , where $\mathrm{acc}_i$ is any law on subsets of $[k]$ with marginals $p_{ij}$ . The rounding is independent of the acceptance decisions.

The rounding scheme is represented by its properties: the goal holds for every distribution $\mu$ with (P1)–(P3) for the weights $y$ , which includes the scheme of Gandhi et al. The LP solution is any optimal one. The order of list $j$ is a permutation of the candidates that is decreasing in $v_{ij}$ , ties in any order. $R_{\mathrm{ALG}_{\mathrm{par}}}$ is computed from the run: candidate $i$ is hired for $j$ iff $i$ is on list $j$ , would accept $j$ , nobody earlier on list $j$ would accept $j$ , and fewer than $T$ candidates precede $i$ on the list. It is not defined by the formula $\mathbb E\,v^*_j(D)$ , which is a milestone, and the goal is compared with the objective at an optimal LP solution, never at an arbitrary feasible point. The degree condition (P2) is kept in the rounding predicate, not replaced by the list properties it implies.

A complete development needs finite sums over product distributions, expected maxima of random subsets of sorted values, and elementary estimates involving $e^{-1}$ ; no measure theory is required. The GKPS definition is generic in the two vertex sets and reusable for other dependent-rounding results. Proofs of any milestone are welcome, as is a proof of Lemma 7 for general negatively correlated roundings.

Selected references

B. Epstein, W. Ma, Selection and Ordering Policies for Hiring Pipelines via Linear Programming, Operations Research, 2024; preprint arXiv:2210.04059v3, 2023. https://arxiv.org/abs/2210.04059
R. Gandhi, S. Khuller, S. Parthasarathy, A. Srinivasan, Dependent rounding and its applications to approximation algorithms, Journal of the ACM 53(3), 2006. https://doi.org/10.1145/1147954.1147956
M. Purohit, S. Gollapudi, M. Raghavan, Hiring under uncertainty, ICML 2019. https://proceedings.mlr.press/v97/purohit19a.html

8 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Optimization+1·Captain: mikedeng1

How Advance Sales Can Reduce Profits: When to Buy, When to Sell, and What Price to Charge: The Profit-Maximizing Price and Induced Arrival Rates Under High DemandResearch Paper

Why advance sales matter

A seller with scarce stock may offer a product before its main selling period. This gives buyers another chance to obtain it, but it can also alter when they compete for the stock. The seller must choose a price while anticipating that buyers respond to both the price and the chance that the unit will already be gone. Glazer, Hassin, and Nowik study this interaction for a single unit and strategic Poisson arrivals in their 2023 paper. Their high-demand model leads to an unusual comparative static: in the regime where buyers arrive in both periods, raising the price increases the total arrival rate (Theorem 1, p. 12). The eventual profit-maximizing price nevertheless induces arrivals in only one period (Theorems 3–4, pp. 13–15).

The two-period arrival game

The seller has one unit and posts one price for two selling periods. Potential buyers are identical and each chooses to try to buy early, try to buy late, or stay away. A buyer pays an arrival cost even if the unit is unavailable. The good is worth less to a buyer who obtains it early. If several buyers arrive while the unit is available, each has the same chance of receiving it. The number choosing each period follows a Poisson arrival model; write $x$ and $y$ for the early and late equilibrium arrival rates. These are expected counts, not probabilities, and may exceed one.

Divide monetary values by the positive arrival cost. Let $v$ be the normalized late value, $k>0$ the penalty for early purchase, and $p\ge0$ the single normalized price. Set $\phi(0)=1$ and $\phi(z)=(1-e^{-z})/z$ for $z\ne0$ . The two arrival utilities and the seller's expected profit are

u_1=-1+(v-p-k)\phi(x),\qquad u_2=-1+e^{-x}(v-p)\phi(y),\qquad \pi=p(1-e^{-(x+y)}).

The factor $e^{-x}$ in $u_2$ is the chance that no early buyer takes the unit. The value $\phi(0)=1$ is the continuous limit of the competition factor, so a buyer considering arrival when nobody else arrives still faces the correct utility. In the paper's high-potential-demand limit (§5, p. 10), an equilibrium has $x,y\ge0$ and satisfies complementarity: a period with a positive arrival rate has utility zero, while a period with zero arrivals offers nonpositive utility to a buyer who considers entering. This selects the paper's equilibrium types 1–4. The finite-demand equilibria in which every potential buyer tries to arrive are outside this mission.

Several thresholds have precise definitions. The principal Lambert function $W[a]$ is the inverse of $w\mapsto we^w$ on $w\ge-1$ (Definition 11, p. 26). Put $W=W[-(k+1)e^{-(k+1)}]$ . The border $v(k)>1$ between mixed and early-only arrivals solves $k=v(k)-\ln v(k)/(1-1/v(k))$ (p. 11). The switching threshold $v_f>k+1$ is the larger root of $f_k(v)=(1-v/(k+1))W-\ln(v-k)$ (Definitions 24 and 26, pp. 42–43).

Formalization targets

The goal is the four-case price rule of Theorem 4 (p. 15). It identifies a profit-maximizing price $p^*$ , its equilibrium rates $(x,y)$ , and the greatest attainable expected profit $\pi^*$ over all nonnegative prices:

(p^*,x,y,\pi^*)= \begin{cases} (\text{any }p\ge0,0,0,0),&v<1,\\ \left(v-\frac{\ln v}{1-1/v},0,\ln v,v-1-\ln v\right),&1<v\le e^{W+k+1},\\ \left(v-k-1,0,W+k+1,(v-k-1)(1-e^{-(W+k+1)})\right),&e^{W+k+1}<v\le v_f,\\ \left(v-k-\frac{\ln(v-k)}{1-1/(v-k)},\ln(v-k),0,v-k-1-\ln(v-k)\right),&v>v_f. \end{cases}

The printed formula in the second case has a removable $0/0$ at $v=1$ ; this mission states that case for $v>1$ and states the boundary $v=1$ separately: there every nonnegative price induces zero arrival rates (so $\lambda_2=\ln 1$ ) and the optimal profit is $\pi_2=0$ . A displayed price is a maximizer: the paper's candidates can tie at $v=v_f$ . The milestones cover equilibrium existence and uniqueness (Proposition 9), the regional Lambert-function formulas (Theorem 14), the mixed-arrival comparative statics (Theorem 1 and Corollary 2), and the candidate-profit comparisons and thresholds (Propositions 20–21 and Lemmas 22, 25, 29).

What the result provides

The theorem tells the seller which price and arrival pattern correspond to each value regime. It also gives an exact benchmark for comparing the option to sell early with selling only in the later period. In this model, offering an early period never raises the maximal profit above the late-only benchmark, a consequence discussed in Corollary 5 and Theorem 6 (p. 15). The price rule is proved in the paper; the work here is to give its model, boundaries, regional lemmas, and global optimality claim machine-checkable statements and ultimately proofs. The mission statements are compiled Lean targets with proof placeholders, not completed machine-checked proofs.

Why the optimization is difficult

A higher price usually suggests fewer buyers. Here an early arrival can remove the only unit before the late period. In the mixed-arrival region a price increase changes the early rate and therefore changes the late buyer's chance of finding stock. The total rate can rise even as the early rate falls. The seller's profit also depends on the price times a sale probability, and its regional price formulas do not automatically give a global maximum. The proof must account for each regional border and compare the relevant candidates; the Lambert formulas and the switching root make those comparisons explicit in the paper.

Formalization scope

Lean uses real parameters $v,k,p,x,y$ in units of the arrival cost. The standing assumptions $k>0$ and $p\ge0$ are explicit. The potential-demand limit is encoded directly by the utility complementarity conditions, and profit ranges over every price and every equilibrium satisfying them. The goal uses IsGreatest together with attainment at the displayed price, so it asserts an actual global maximum. The paper's $W$ , $v_f$ , and $v(k)$ are defined from their characterizing equations on the principal branch and the stated root domains; they are not free parameters. The statements guard the logarithms and quotients that arise at $v=1$ and $v-k=1$ . The separate region listings in the paper differ at some harmless boundaries, so each milestone uses the borders relevant to its own statement.

A valid formalization must keep $\phi(0)=1$ , define equilibrium through utility conditions rather than through the claimed closed forms, and compare profit across every nonnegative price. Otherwise the equilibrium and optimality results could become empty or immediate by definition. The reusable work includes the continuous Poisson competition factor, Lambert-function interface, and precise handling of attained extrema. The mission covers one unit and high potential demand; the paper's multiple-unit numerical section and finite-demand equilibrium types are separate topics.

Selected references

A. Glazer, R. Hassin, and I. Nowik, How Advance Sales Can Reduce Profits: When to Buy, When to Sell, and What Price to Charge, Manufacturing & Service Operations Management, 2023. arXiv:1912.02869v2

11 thms2 active usersReviewed

Completed

Mechanism Design Operations Research Optimization+1·Captain: mikedeng1

Intertemporal Price Discrimination via Randomized Promotions: A Two-Point Price Distribution Is Optimal for Randomized Pricing with Two Customer SegmentsResearch Paper

Motivation

Retailers that run predictable promotions teach their customers to wait for them. A customer who knows that a discount will come next week has no reason to buy at the list price today. Firms therefore lose margin on exactly the customers who would have paid in full. One response, documented in practice by Moon, Bimpikis and Mendelson (2017), is to randomize promotions: commit to a distribution of prices, draw a fresh price every period, and let customers know only the distribution. A customer cannot time a discount that arrives at random. Whether waiting is worthwhile then depends on how patient the customer is.

The classical deterministic answer to strategic waiting is cyclic pricing: Conlisk, Gerstner and Sobel (1984) showed that a durable-goods monopolist facing a stream of arriving customers lowers its price periodically. Besbes and Lobel (2015) characterized optimal deterministic policies when customers differ in valuation and patience. Randomized prices as a model of sales go back to Varian (1980) in a competitive setting. Chen, Hu and Wu (SSRN 3223844, published in Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2023.1194) ask the monopoly question directly: which price distribution should a seller commit to when two customer segments differ in both valuation and waiting cost? This mission formalizes their answer for the two-segment base model.

Setting

A monopolist sells one product over an infinite horizon. A fraction $\alpha\in(0,1)$ of arriving customers are low-valuation customers, who value the product at $v_L$ and pay a waiting cost $c_L$ per period; the remaining $1-\alpha$ are high-valuation customers, with valuation $v_H>v_L$ and waiting cost $c_H$ . Assumption (S) of the paper is $0<c_L<v_L$ and $0<c_H<v_H$ .

The firm announces a price distribution: a random price $P$ with finitely many possible values $p$ and probabilities $f(p)\ge0$ summing to one. Each period an independent price is drawn from it. Write $F(x)=\sum_{p\le x}f(p)$ for the distribution function, $\mathbb E[P\mid P\le x]$ for the mean price conditional on $P\le x$ , and $\mathbb E[(v-P)^+]=\sum_p f(p)\max(v-p,0)$ for the expected one-period surplus of a customer with valuation $v$ . The purchase threshold of a customer with waiting cost $c$ is

\underline p=\max\{v'\mid \mathbb E[(v'-P)^+]\le c\}.

A customer whose valuation exceeds her threshold waits and buys at the first price not above it.

The paper reduces the firm's choice to the regime where low-valuation customers wait and high-valuation customers buy on arrival. The firm's long-run profit per arriving customer is then the objective of problem (2):

\max_{F}\ \alpha\,\mathbb E[P\mid P\le \underline p^L]+(1-\alpha)F(v_H)\,\mathbb E[P\mid P\le v_H]\quad\text{s.t.}\quad \mathbb E[(v_L-P)^+]>c_L,\ \ \mathbb E[(v_H-P)^+]\le c_H,

where $\underline p^L$ is the low type's threshold. Replacing $\underline p^L$ by $v_L$ in the objective gives the relaxation, problem (3). The key constants are

\Delta_R=\sqrt{\frac{\alpha c_L}{(1-\alpha)(v_H-v_L)}},\qquad U_1=\alpha v_L+(1-\alpha)v_H-(1-\alpha)c_L-2(1-\alpha)(v_H-v_L)\Delta_R,

U_2=\alpha v_L+(1-\alpha)v_H-(1-\alpha)c_H-\alpha c_L\frac{v_H-v_L}{c_H-c_L}.

In Lean the parameters are vL vH cL cH α, a law is w : ℝ →₀ ℝ with IsPriceDist w, and the objects above are cdf, condExp, gain, thresh, Feas, obj2, obj3, ΔR, bnd $=(c_H-c_L)/(v_H-v_L)$ , U1, U2. Here $\underline p^L$ is written p^L in milestone text.

Formalization targets

Goal: Proposition 3 (p. 16)

Assume $c_L<c_H$ and $\Delta_R<1$ , and let $U=U_1$ if $\Delta_R<\frac{c_H-c_L}{v_H-v_L}$ and $U=U_2$ otherwise. Then every price distribution feasible for (2) earns at most $U$ in (2), and there is $\eta$ with $\eta(\delta)\to0$ as $\delta\searrow0$ such that the two-point law

f(p)=\begin{cases}\beta^* & p=\underline p^*,\\ 1-\beta^* & p=v_H,\end{cases}\qquad \beta^*=\min\Big\{\Delta_R,\frac{c_H-c_L}{v_H-v_L}-\delta\Big\},\quad \underline p^*=v_L-\frac{c_L}{\beta^*}-\eta(\delta),

is feasible for (2) for all small $\delta>0$ and its profit tends to $U$ . This is the $\epsilon$ -optimality of the paper's Definition 1.

Milestones

§3.2.2: for every law feasible for (2), $\mathbb E[P\mid P\le\underline p^L]\le\mathbb E[P\mid P\le v_L]$ , so (3) relaxes (2).
§3.2.2: every feasible law has $F(v_L)<\frac{c_H-c_L}{v_H-v_L}$ .
Lemma 5, in the form its proof establishes: moving all mass above $v_L$ to $v_H$ preserves feasibility and does not lower the objective of (3).
Lemma 6(ii)(a) and (b): every feasible law earns at most $U_1$ , respectively $U_2$ , in (3).
Lemma 6(i), the complementary regime $\Delta_R\ge1$ : no feasible law beats the static profit $\max\{v_L,(1-\alpha)v_H\}$ .

Significance

The result says that, in this model, the optimal randomized promotion is the simplest one. The firm posts the regular price $v_H$ most of the time and runs a promotion at $\underline p^*$ with probability $\beta^*$ . High-valuation customers buy on arrival; low-valuation customers wait for the promotion. The discount below $v_L$ , of size $c_L/\beta^*$ , is the price of keeping low types in the market. The closed forms $U_1,U_2$ quantify the profit lost relative to perfect discrimination $\alpha v_L+(1-\alpha)v_H$ . The paper uses them to compare randomized with static and cyclic pricing (Propositions 4 and 8) and generalizes the structure to myopic customers and to $n$ segments.

The result is proved on paper; no machine-checked version exists. The mission produces a formal statement of the firm's problem over all finitely supported price laws on $\mathbb R$ , a verified upper bound on its value, and a verified family that attains it in the limit. It also records three points the printed statements leave implicit (below).

Difficulty

The decision variable is an entire distribution, and the objective of (2) depends on it through the threshold $\underline p^L$ , itself defined by a maximization over the distribution. The obvious approach, guessing the two-point law and checking first-order conditions, gives no upper bound over all laws. The upper bound has to hold for laws with arbitrarily many support points, of either sign and above $v_H$ , and both incentive constraints enter it. Problem (3) has a strict constraint and no maximizer, so every statement about "the optimal profit" has to be read as a supremum. The attainment half then needs the threshold of the two-point law, computed from its definition, to sit exactly $\eta(\delta)$ below $v_L$ .

Formalization scope

Distributions. A price law is w : ℝ →₀ ℝ with nonnegative masses summing to one (finite support, as the paper assumes on p. 9). Prices range over all of $\mathbb R$ : $\underline p^*$ can be negative under the hypotheses, and with prices restricted to $[0,\infty)$ Proposition 3 is false for some admissible parameters.
Standing assumptions, hypotheses of every theorem: Assumption (S), $v_L<v_H$ (printed on p. 9), and $0<\alpha<1$ (added; $\Delta_R$ divides by $1-\alpha$ ).
Added hypothesis of the goal: $c_L<c_H$ . Without it $\beta^*<0$ and the two-point law is not a distribution.
Conventions. $\mathbb E[P\mid P\le x]$ is a quotient that Lean sets to $0$ when $F(x)=0$ ; this never happens for feasible laws. $\underline p^L$ is the real supremum of $\{v'\mid\mathbb E[(v'-P)^+]\le c_L\}$ , which is a maximum for every price law. "The optimal expected profit is no more than $U$ " is read as a bound on every feasible law. "Optimal" in Proposition 3 is $\epsilon$ -optimality for (2), stated as the upper bound plus the approaching family, with $\eta$ existential.
Lemma 5 as printed quantifies over optimal solutions of (3), which do not exist; the milestone states the dominance that its proof (Online Supplement p. 8) establishes.
Ruled out. The profit and the threshold of the two-point law are not given in closed form: they are the general obj2 and thresh applied to it. The upper bound ranges over all feasible laws, not two-point laws or laws on $[0,v_H]$ . "Optimal" is not read as "beats static pricing" (that is Proposition 4) or as an attained maximum, and $\eta$ may not depend on the competing law.
Not in the mission. The customer's optimal-stopping model (Lemma 1, Proposition 1, Lemma 2) is the paper's justification of the objective of (2); the mission states problem (2) as printed. Cyclic and Markovian pricing, myopic customers and $n$ segments are not posed.
Needed infrastructure. Finite sums over Finsupp supports, monotonicity and continuity of $v\mapsto\mathbb E[(v-P)^+]$ , and the elementary concavity argument for $\beta\mapsto U(\beta)$ . A general library of finitely supported real price laws (distribution function, partial expectations, expected surplus) would be reusable for other pricing papers. Proofs of any milestone are welcome.

Selected references

H. Chen, M. Hu, J. Wu, Intertemporal Price Discrimination via Randomized Promotions, SSRN preprint 3223844 (revision of 2022-11-16); Manufacturing & Service Operations Management, 2023. https://ssrn.com/abstract=3223844, https://doi.org/10.1287/msom.2023.1194
J. Conlisk, E. Gerstner, J. Sobel, Cyclic pricing by a durable goods monopolist, Quarterly Journal of Economics 99(3), 1984. https://doi.org/10.2307/1885961
O. Besbes, I. Lobel, Intertemporal price discrimination: Structure and computation of optimal policies, Management Science 61(1), 2015. https://doi.org/10.1287/mnsc.2014.2049
H. Varian, A model of sales, American Economic Review 70(4), 1980. https://www.jstor.org/stable/1803562
X. Su, Intertemporal pricing with strategic customer behavior, Management Science 53(5), 2007. https://doi.org/10.1287/mnsc.1060.0628
K. Moon, K. Bimpikis, H. Mendelson, Randomized markdowns and online monitoring, Management Science, 2017.

8 thms2 active usersReviewed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

Guarantees in Fair Division: General or Monotone Preferences 1: Kuhn's Divide & Choose Rule Guarantees Every Agent Her minMax Utility for Continuous Non-Atomic PreferencesResearch Paper

Motivation

Fair division asks how to share a resource among $n$ agents with different preferences so that each agent can be promised a minimum level of welfare, whatever the preferences of the others. Classical cake cutting treats a good cake, valued additively or at least monotonically. Many real problems mix goods and bads: a plot of land with both fertile and polluted parts, a set of chores some of which are welcome, a workload whose value first rises and then falls with its size. Bogomolnaia and Moulin (arXiv:1911.10009, Mathematics of Operations Research 2023) study the most general non-atomic model, in which a utility is only required to be continuous and bounded, and ask which utility levels can be guaranteed simultaneously to all agents.

Their first main result is that Kuhn's $n$ -person Divide & Choose rule (Kuhn 1967) guarantees each agent her minMax utility, in this full generality. The key ingredient is an equipartition theorem of Avvakumov and Karasev ([4]), which lets the current divider cut any piece into equally valued parts even when the utility is neither monotone nor of constant sign.

Setting

The manna $\Omega$ is a bounded Lebesgue-measurable subset of $\mathbb R^d$ , $d\ge1$ , with $|\Omega|>0$ ; $|\cdot|$ is Lebesgue measure. A share is a measurable subset $S\subseteq\Omega$ , possibly empty. For a share $S$ , an $n$ -partition $\Pi=(S_i)_{i=1}^n\in\mathcal P_n(S)$ is an $n$ -tuple of shares with $\bigcup_i S_i=S$ and $|S_i\cap S_j|=0$ for $i\ne j$ . The pseudo-metric on shares is $\delta(S,T)=|S\otimes T|$ , the measure of the symmetric difference.

A utility $u$ assigns a real number to each share, with $u(\emptyset)=0$ , and is bounded and continuous for $\delta$ . The set of utilities is $\mathcal D(\Omega)$ . Nothing else is assumed: $u$ may increase or decrease with the share and may take both signs.

An $n$ -equipartition of a share $S$ for $u$ is a partition $\Pi^e\in\mathcal P_n(S)$ whose parts all have the same utility $u(\Pi^e)$ ; their set is $\mathcal{EP}_n(S;u)$ . The two benchmarks are

\mathrm{minMax}(u;n)=\inf_{\Pi\in\mathcal P_n(\Omega)}\max_i u(S_i),\qquad \mathrm{Maxmin}(u;n)=\sup_{\Pi\in\mathcal P_n(\Omega)}\min_i u(S_i).

minMax is what an agent gets choosing first from the worst partition for her; Maxmin is what she gets choosing last from the best one.

In the D&C $_n$ rule the agents are ordered $1,\dots,n$ . At each step the first remaining agent, the Divider, proposes an $m$ -partition of the remaining manna $S$ among the $m$ remaining agents. Every other remaining agent reports which shares she likes (at least one); the Divider likes all of them. A set of agents is properly matched to a set of shares when they are matched one-to-one to liked shares and no other remaining agent likes any of those shares. The largest properly matchable set of agents is served; the other shares return to the manna, and the rule continues with the unserved agents.

Formalization targets

Goal: Theorem 1 i)

An agent $i$ with utility $u\in\mathcal D(\Omega)$ follows the minMax strategy when, as Divider, she proposes an equipartition $\Pi^e\in\mathcal{EP}_m(S;u)$ , and, as chooser, she likes exactly the shares $T$ with $u(T)\ge\mathrm{minMax}(u;n)$ , the level of the initial problem. Then, whatever the other agents do,

the Divider move is always available (an equipartition exists);
the chooser move is always available (some offered share is worth at least $\mathrm{minMax}(u;n)$ );
in every complete play,

u(S_i)\ \ge\ \mathrm{minMax}(u;n).

Milestones

The equipartition theorem of [4] on $[0,1]$ ; Lemma 1, $\mathcal{EP}_n(S;u)\ne\emptyset$ for every share and every $u\in\mathcal D(\Omega)$ ; Lemma 2, existence of a largest properly matchable set containing the Divider; and the three steps of the proof of Theorem 1 i): the invariant that previously assigned shares are worth less than minMax to an unserved agent, the chooser step and the Divider step.

Companions

Proposition 1 iii), $\mathrm{minMax}(u;n)\le u(\Pi^e)\le\mathrm{Maxmin}(u;n)$ for every $\Pi^e\in\mathcal{EP}_n(\Omega;u)$ , and the statement that $\mathrm{minMax}(\cdot;n)$ is a Fair Guarantee in $\mathcal D(\Omega)$ : every profile $(u_i)\in\mathcal D(\Omega)^n$ admits $\Pi\in\mathcal P_n(\Omega)$ with $u_i(S_i)\ge\mathrm{minMax}(u_i;n)$ for all $i$ (Definition 3).

Significance

Maxmin is an upper bound on any Fair Guarantee, and in the mixed-manna domain it is not itself a Fair Guarantee. Theorem 1 establishes minMax as a guarantee that holds on the whole domain, is implemented by a simple decentralised protocol, and requires no knowledge of the other agents' preferences. Together with the companion results it brackets what can be promised to every agent in non-atomic division with arbitrary continuous preferences.

The result is proved in the paper; nothing in this mission is open mathematics. None of it is machine-checked. The formalization adds a non-atomic fair-division layer (shares up to null sets, $\delta$ -continuous utilities, equipartitions, minMax and Maxmin) and a precise model of a sequential division protocol in which the other agents' behaviour is quantified over, rather than fixed. The goal also makes explicit the step the informal proof passes over quickly: the minMax strategy is always a legal move.

Difficulty

Once the protocol is modelled, the guarantee is an invariant argument over the steps of a play. The difficulty is Lemma 1. For an additive utility, Lyapunov's theorem gives equipartitions; for a utility of constant sign, the Knaster–Kuratowski–Mazurkiewicz lemma does (Remark 1). A utility that takes both signs defeats both arguments, and an obvious intermediate-value argument handles only $n=2$ . The paper reduces Lemma 1, through a moving knife, to the interval theorem of Avvakumov and Karasev, whose proof is topological (mapping degree). Mathlib has neither that theorem nor the degree theory it uses. Lemma 2 needs the Gallai–Edmonds decomposition of a bipartite graph, which Mathlib does not have either; Hall's theorem is available.

Formalization scope

The space is EuclideanSpace ℝ (Fin d) with volume, and every statement that needs non-atomicity assumes $d\ge1$ (on $\mathbb R^0$ , a point of measure $1$ , Lemma 1 fails). A utility is a function on all subsets, but every condition is imposed on shares only. Partitions are indexed by Fin n, have union exactly the share and null pairwise overlaps; disjointness is not required. minMax and Maxmin are real sInf/sSup; every statement using them assumes $n\ge1$ , which makes the defining sets nonempty and bounded. Agents are Fin n, the Divider is the least remaining agent, and a play is a list of steps, each recording the remaining agents and manna, the proposed partition, all reports and the assignment. A step is admissible exactly as Definition 4 requires, including that the served set is the largest properly matchable one.

The following formalizations would trivialize the goal and are ruled out: fixing the other agents' behaviour; accepting against the minMax of the remaining manna instead of the initial one; assuming the utility monotone, additive or of constant sign; defining minMax as a minimum over a possibly empty set; and omitting the availability parts 1–2, which would make Lemma 1 irrelevant.

A complete development needs the interval equipartition theorem (a topological result of independent interest), moving knives through a measurable set, a Gallai–Edmonds-type argument for bipartite graphs, and the invariant over plays. The non-atomic model and the equipartition lemmas are reusable for the Moving Knife and Bid & Choose rules of the companion mission. Proofs of any milestone, alternative proofs of Lemma 1 for special classes of utilities, and the run-level lemmas are all welcome.

Selected references

A. Bogomolnaia, H. Moulin, Guarantees in Fair Division: General or Monotone Preferences, Mathematics of Operations Research, 2023; arXiv:1911.10009v3. https://arxiv.org/abs/1911.10009
S. Avvakumov, R. Karasev, Equipartition of an interval, cited in the paper as [4] (2020, in preparation).
H. W. Kuhn, On games of fair division, in Essays in Mathematical Economics in Honour of Oskar Morgenstern, Princeton University Press, 1967, pp. 29–37.
L. Lovász, M. D. Plummer, Matching Theory, Annals of Discrete Mathematics 29, North-Holland, 1986 (Gallai–Edmonds decomposition, Chapter 3).

10 thms2 active usersReviewed

Control Theory Operations Research Probability+1·Captain: mikedeng1

An Approximate Analysis of Dynamic Pricing, Outsourcing, and Scheduling Policies for a Multiclass Make-to-Stock Queue in the Heavy Traffic Regime: The Two-Barrier Drift-Rate Control Policy Is OptimalResearch Paper

Motivation

A manufacturer that makes several products to stock for price-sensitive customers controls three levers at once: the prices it posts, which shape demand; outsourcing, which clears a large backlog at a cost; and scheduling, which decides which product the single server makes next. Ata and Barjesteh (Operations Research 71(1), 2023) study this multiclass make-to-stock queue in the heavy-traffic regime, where the queue is nearly saturated and the system is approximated by a Brownian control problem. The approximation collapses to a one-dimensional problem in the workload, the total amount of work in the system. Its solution is a two-barrier policy whose state-dependent drift translates back into a dynamic pricing rule, an outsourcing threshold and a scheduling priority (§7 of the paper).

The one-dimensional problem belongs to the family of drift-rate control problems for Brownian motion under a long-run average cost criterion (Ata, Harrison and Shepp, Ann. Appl. Probab. 2005; Rubino and Ata, Oper. Res. 2009). Problems of this kind are solved by a Bellman equation with free boundaries and a verification argument; the present paper adds two-sided singular control (outsourcing at the bottom, idling at the top) to a quadratic drift cost and a piecewise linear state cost.

Setting

There are $K\ge1$ products with mean production times $m_k>0$ and holding, backorder and outsourcing cost rates $h_k,b_k,r_k>0$ . A symmetric positive definite matrix $H$ describes the curvature of the revenue rate. Write $a=m'H^{-1}m$ and

h^\star=\min_k\frac{h_k}{m_k},\qquad b^\star=\min_k\frac{b_k}{m_k},\qquad \kappa=\min_k\frac{r_k}{m_k}.

The drift cost and the effective holding cost are

c(x)=\min\{\zeta'H\zeta:\ m'\zeta=x\},\qquad h(w)=h^\star w\ (w\ge0),\quad h(w)=-b^\star w\ (w<0).

Let $B$ be a Brownian motion with drift $\mu\ge0$ and variance $\sigma^2>0$ , started at $0$ , with respect to a filtration $\mathbb F$ . An admissible control consists of a progressively measurable drift rate $\theta$ and nondecreasing, right-continuous, adapted processes $L$ (effective outsourcing) and $U$ (idleness) with $L(0)=U(0)=0$ . The workload is

W(t)=B(t)-\int_0^t\theta(s)\,ds-U(t)+L(t),

and admissibility also requires $\mathbb E|W(t)|/t\to0$ . The equivalent workload formulation (EWF) is to minimize

\limsup_{t\to\infty}\frac1t\,\mathbb E\Big[\int_0^tc(\theta(s))\,ds+\int_0^th(W(s))\,ds+\kappa L(t)\Big]. \tag{29}

A barrier policy with barriers $l<u$ keeps $W$ in $[l,u]$ , increases $L$ only when $W=l$ and $U$ only when $W=u$ .

For $\gamma\ge0$ put $l_\gamma=-\frac1{b^\star}(\gamma+\mu\kappa+\frac a4\kappa^2)$ and $u_\gamma=\gamma/h^\star$ . Let $v^-_\gamma$ solve the Riccati equation

v'=\frac a{2\sigma^2}(v^2-\kappa^2)-\frac{2\mu}{\sigma^2}(v+\kappa)+\frac{2(h(l_\gamma)-h(w))}{\sigma^2}\ \text{on }[l_\gamma,0],\qquad v(l_\gamma)=-\kappa,

and $v^+_\gamma$ solve $v'=\frac a{2\sigma^2}v^2-\frac{2\mu}{\sigma^2}v+\frac{2(h(u_\gamma)-h(w))}{\sigma^2}$ on $[0,u_\gamma]$ with $v(u_\gamma)=0$ . The paper's $\gamma^\star$ is the unique $\gamma$ with $v^-_{\gamma}(0)=v^+_{\gamma}(0)$ ; $v$ pastes $v^-_{\gamma^\star}$ and $v^+_{\gamma^\star}$ at $0$ , and the candidate drift is $\theta(w)=\frac a2v(w)$ .

Formalization targets

Goal: Theorem 1

For every filtered probability space carrying such a Brownian motion,

\lim_{t\to\infty}\frac{J_{\text{cand}}(t)}t=\gamma^\star\quad\text{for every barrier policy at }(l_{\gamma^\star},u_{\gamma^\star})\text{ with drift }\theta(W),\qquad \limsup_{t\to\infty}\frac{J(t)}t\ge\gamma^\star\ \text{for every admissible control},

where $J$ is the expected cumulative cost in (29). The constant $\gamma^\star$ is the paper's construction, not a parameter.

Milestones

Lemma 1 and Lemma 2: the closed forms $c(x)=x^2/a$ and its conjugate $\varphi(y)=\frac a4y^2$ , maximized at $\psi(y)=\frac a2y$ .
Proposition 2: a barrier policy whose $(\gamma,f)$ solves the ODE (35)–(36) has long-run average cost $\gamma$ .
Lemma 3: any solution of the Riccati-form Bellman equation (43)–(45) has $\gamma>0$ , $l=l_\gamma<0$ , $u=u_\gamma>0$ .
Lemmas 18–20 and Corollary 6: sign and monotonicity of the Riccati solutions.
§6.3 well-posedness, Lemma 4(i)–(ii), Corollary 1: uniqueness of $v^\pm_\gamma$ , their monotone dependence on $\gamma$ , and the unique crossing $\gamma^\star$ .
Proposition 3 and Corollary 2: $(l_{\gamma^\star},u_{\gamma^\star},\gamma^\star,v)$ is the unique solution of (43)–(45), and $f=\int v$ solves the Bellman equation (37)–(39), uniquely up to a constant.

Significance

The theorem identifies an explicit optimal policy for a two-sided singular drift-control problem: two barriers and a strictly increasing, non-positive drift, all determined by a scalar root $\gamma^\star$ of a monotone equation. In the paper it drives the proposed pricing, outsourcing and scheduling policy (§7) and its asymptotic analysis; the Riccati structure is what makes $\gamma^\star$ computable by line search.

The result is proved in the paper; none of it has been machine-checked. Formalizing it gives a checked verification theorem for an average-cost Brownian control problem with singular controls, and checked statements of the Riccati comparison lemmas on which it rests. Several printed statements of the paper are corrected here (see the scope section), so the formal versions are the first fully precise ones.

Difficulty

The optimality half of Theorem 1 is a verification argument: apply Itô's formula to $f(W(t))$ for an arbitrary admissible control with jumps in $L$ and $U$ , use the Bellman inequality pointwise, and control $\mathbb E f(W(t))/t$ with the growth condition (32). Mathlib does not yet have Itô's formula for continuous semimartingales with finite-variation, possibly discontinuous parts, and the candidate's average cost (Proposition 2) needs the same tool plus the fact that a reflected diffusion spends zero time at the barriers.

The deterministic half is not routine either. The obvious reading of the paper, solving each Riccati problem for every $\gamma\ge0$ and passing $\gamma\to\infty$ , fails: the solutions blow up in finite time, so $v^\pm_\gamma$ exist only for $\gamma$ in a bounded initial interval, and the crossing argument must be run on that interval. The comparison arguments of Lemmas 18–20 also need second derivatives of solutions whose right-hand side has a kink at $w=0$ .

Formalization scope

Time is indexed by $\mathbb R$ and only $t\ge0$ matters. The Brownian motion is defined locally (drift, variance, start at $0$ , independence of increments from the filtration). Expected costs are computed in $[0,\infty]$ , so a control with infinite cost counts as $+\infty$ . The integrals in (34) are Lebesgue–Stieltjes integrals against the paths of $L$ and $U$ , jumps included. Derivatives at the barriers are one-sided; $C^1$ and $C^2$ up to the boundary are ContDiffOn on the closed interval. Minima and maxima (in $c$ , (37), (40)) are stated as attained.

Standing assumptions added to every statement, all implicit in the paper: $K\ge1$ ; $m_k,h_k,b_k,r_k>0$ ; $H$ symmetric positive definite; $\mu\ge0$ , $\sigma>0$ ; $B$ starts at $0$ ; $L,U$ right-continuous; $\theta$ progressively measurable with locally integrable paths; $l<u$ in the Bellman equations.

Corrected statements. Lemmas 18–20 are printed for solutions on $[0,\infty)$ , which do not exist; they are posed on every bounded interval where a solution exists. The §6.3 claim that $v^\pm_\gamma$ exist for every $\gamma\ge0$ is replaced by uniqueness, solvability at $\gamma=0$ and order-connectedness of the solvability sets. Lemma 4's limits as $\gamma\to\infty$ become unboundedness on those sets. Theorem 1's comparison class is every admissible control, which the paper's proof treats, and which contains the stationary Markov policies to which §6 restricts attention.

Not posed. The existence of the reflected diffusion realizing the candidate policy is presupposed by the paper and not claimed: the first half of the goal quantifies over all barrier policies with the given data. The second half is a statement about every admissible control and is not vacuous.

$\gamma^\star$ , $v$ , $f$ and $\theta$ are built from the Riccati solutions by choice, exactly as the paper constructs them; taking them as hypotheses-constrained parameters, or defining $c$ by its closed form, would trivialize the goal and is ruled out. Contributions are welcome on the Riccati lemmas (pure real analysis, reusable for other drift-control problems), on Itô's formula for semimartingales with finite-variation parts, and on Skorokhod-type existence of reflected diffusions.

Selected references

B. Ata and N. Barjesteh, An Approximate Analysis of Dynamic Pricing, Outsourcing, and Scheduling Policies for a Multiclass Make-to-Stock Queue in the Heavy Traffic Regime, Operations Research 71(1):341–357, 2023. https://doi.org/10.1287/opre.2022.2361 (accepted manuscript: https://ssrn.com/abstract=3464763)
B. Ata, J. M. Harrison and L. A. Shepp, Drift rate control of a Brownian processing system, Annals of Applied Probability 15(2):1145–1160, 2005. https://doi.org/10.1214/105051604000000855
M. Rubino and B. Ata, Dynamic control of a make-to-order, parallel-server system with cancellations, Operations Research 57(1):94–108, 2009. https://doi.org/10.1287/opre.1080.0532
J. M. Harrison, Brownian Models of Performance and Control, Cambridge University Press, 2013. https://doi.org/10.1017/CBO9781139087698

19 thms2 active usersReviewed

Completed

Control Theory Dynamic Programming Operations Research+1·Captain: mikedeng1

A Dynamic Model for Managing Volunteer Engagement I: The Bellman Equation of the Drift-Rate Control Problem Has a SolutionResearch Paper

Motivation

Non-profit organizations depend on volunteers whose availability they cannot schedule. They can only influence it, through recruiting drives, reminders and recognition events. Ata, Tongarlak, Lee and Field (arXiv:2312.02920) model a food-recovery non-profit's volunteer pool as a queueing network. Repeat volunteers rest between shifts, one-time volunteers arrive at random, and all signed-up volunteers wait on one sign-up list, from which they may abandon. The organization pays for engagement activities that speed up volunteers' return, and it is penalized when tasks go uncovered because the list is empty.

In heavy traffic the problem reduces to a one-dimensional drift-rate control problem. A workload process $W \ge 0$ behaves like a reflected Ornstein–Uhlenbeck process whose drift $\theta(t)$ the controller chooses from an interval $A = [\theta_0, \theta_L]$ at cost $c(\theta(t))$ , plus a penalty $p$ per unit of idleness at $W = 0$ . The analytic core of the paper is the Bellman equation of this problem: a first-order ordinary differential equation on $[0,\infty)$ with an unknown constant. Its solution yields the optimal long-run average cost and a nested threshold policy for when to run each engagement activity.

Setting

There are $L \ge 1$ 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 > 0$ , 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, 1, \dots, L,

and $A = [\theta_0, \theta_L]$ . The engagement cost $c : A \to \mathbb{R}_+$ is piecewise linear and convex: $c(\theta_0) = 0$ , with slope $c_l$ on $(\theta_{l-1}, \theta_l]$ , so that $c(x) = \sum_{i=1}^{l-1} c_i \eta_i + c_l (x - \theta_{l-1})$ for $\theta_{l-1} < x \le \theta_l$ . Its convex conjugate is

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

The Bellman equation (68)–(69) asks for a constant $\beta > 0$ and a continuously differentiable function $v$ on $[0,\infty)$ such that

\beta = \tfrac12 \sigma^2 v'(x) + x\kappa\,(p - v(x)) - \phi(p - v(x)), \qquad x \ge 0,

with $v(0) = 0$ , $v$ strictly increasing, and $\lim_{x\to\infty} v(x) = p$ .

The milestones use the shooting objects of the paper's Online Supplement §F:

the lower bound $\underline\beta = -\inf\{\phi(y) : y \le p\}$ ;
the initial value problem IVP( $\beta$ ): the same equation with only the condition $v(0) = 0$ ; its solution is $v_\beta$ ;
the set $\mathcal I$ of $\beta > \underline\beta$ for which $v_\beta$ is increasing;
the set $\mathcal D$ of $\beta > \underline\beta$ for which $v_\beta$ is nondecreasing on $(0, x_\beta)$ and nonincreasing on $(x_\beta, \infty)$ for some $x_\beta$ ;
the constant $\beta^* = \inf \mathcal I$ .

Formalization targets

Goal: Theorem 1 (p. 21)

\exists\, \beta > 0,\ \exists\, v \in C^1[0,\infty):\quad \beta = \tfrac12\sigma^2 v' + x\kappa(p - v) - \phi(p - v)\ \ (x \ge 0),\quad v(0) = 0,\quad v \uparrow,\quad v(x) \to p.

The goal asserts existence only. It does not identify $\beta$ with $\inf\mathcal I$ , and it does not claim uniqueness.

Milestones (Online Supplement §F, in attack order)

$\underline\beta > 0$ (OS p. 13).
Lemma 3: $\phi$ is Lipschitz with constant $\max_{0\le k\le L} |\theta_k|$ .
Lemma 4: IVP( $\beta$ ) has a unique $C^1$ solution on $[0,\infty)$ for $\beta > \underline\beta$ .
Lemma 6: $v_\beta(x)$ is strictly increasing in $\beta$ for $x > 0$ and continuous in $\beta$ .
Corollary 2: $v_\beta$ has no flat pieces.
Lemmas 10, 12, 15, 16: descriptions of $\mathcal D$ . Membership in $\mathcal D$ is equivalent to $v_\beta' < 0$ somewhere, to $v_\beta < 0$ somewhere, and to $v_\beta \to -\infty$ . $\mathcal D$ is closed downward.
Lemmas 13, 14: $\mathcal I, \mathcal D \ne \emptyset$ , and a characterization of the solutions in $\mathcal I$ that overshoot $p$ .
Lemmas 17, 18, 20: $\beta^* > \underline\beta$ , $\beta^* \in \mathcal I$ with $v_{\beta^*}$ bounded, and $v_{\beta^*}(x) \to p$ .
Corollary 4: $(\beta^*, v_{\beta^*})$ solves (68)–(69).

Significance

The Bellman equation is what makes the paper's policy computable. Theorem 1 provides the constant $\beta^*$ , which the paper's Theorem 2 identifies as the optimal long-run average cost of the workload problem. It also provides the increasing function $v$ , whose level sets $\tau_l = v^{-1}(p - c_l)$ are the thresholds of the optimal nested policy: engagement activity $l$ is used when the workload is below $\tau_l$ . The companion mission (II) gives $v$ in closed form between consecutive thresholds. Both results presuppose the existence proved here.

The paper proves Theorem 1 in its Online Supplement, partly by citation: Lemma 4 is called standard and its proof is omitted. As far as is known, none of these statements has a machine-checked proof. A formalization would also settle two points that the printed argument leaves loose. The lower bound $\underline\beta$ is written as an infimum over all of $\mathbb{R}$ , which is $-\infty$ when $\theta_L < 0$ . And one step in the proof of Lemma 9 claims that a set of positive measure contains an interval, which is false; the formal chain avoids this step by posing Corollary 2 directly.

Difficulty

The equation is first order but nonlinear through $\phi$ , and it is posed on an unbounded interval with a boundary condition at infinity. A local existence theorem does not suffice: the right-hand side has linear growth with a coefficient that grows with $x$ , so global existence on $[0,\infty)$ and monotone, continuous dependence on $\beta$ must be established separately.

The main difficulty is the shooting step. For a fixed $\beta$ the initial value problem has a solution, but it generally fails the condition $v(x) \to p$ : either it eventually turns down and tends to $-\infty$ , or it crosses $p$ and grows without bound. The proof must show the following:

the parameter range splits cleanly into these two behaviours, with no third behaviour such as a plateau or a limit strictly between $0$ and $p$ ;
both behaviours occur;
at the infimum $\beta^*$ of the increasing regime, the solution is increasing and bounded and converges exactly to $p$ .

Continuity in $\beta$ alone does not give the last point: it needs a separate argument at infinity.

Formalization scope

Everything is stated for one fixed parameter set satisfying an explicit predicate Standing: $L \ge 1$ , $\theta_0 < 0$ , $\eta_l > 0$ , $0 < c_1 < \dots < c_L < p$ , $p, \kappa, \sigma > 0$ . These are disclosed additions. The paper never restates them for the abstract control problem, but they follow from its queueing primitives ((24), (43), (50), p. 18). No hypothesis $\theta_L \ge 0$ is made.

Conventions:

$\eta$ and $c$ are sequences indexed by $\mathbb{N}$ and used at $1, \dots, L$ .
The cost is (52) written as one sum. It agrees with (52) on $A$ , and its values off $A$ are never used.
$\phi$ is the real supremum over the compact interval $A$ (attained). It is never defined by its closed form.
$\underline\beta$ is $-\inf\{\phi(y) : y \le p\}$ . This is the reading the paper's proofs use, and it agrees with the printed $-\inf_{y \in \mathbb{R}} \phi(y)$ whenever $\theta_L \ge 0$ .
"Continuously differentiable on $[0,\infty)$ " is a pair $(v, v')$ : $v'$ is continuous on $[0,\infty)$ and is the derivative of $v$ within $[0,\infty)$ at every point (one-sided at $0$ ).
"Increasing" means strictly increasing.
$\beta^* = \inf \mathcal I$ is a real infimum. Lemmas 13, 17 and 18 make it meaningful; no property of $\mathcal I$ is assumed.

Trivializing formalizations are ruled out. The solution $v_\beta$ is never chosen: every lemma quantifies over all solutions of IVP( $\beta$ ). The goal quantifies $\beta$ and $v$ existentially and requires all of (69), including the limit $p$ and strict monotonicity.

The source is the arXiv preprint v2, including its Online Supplement. The queueing network (§2) and the Brownian control problem (§3) motivate the equation but are not part of any formal statement.

A complete development needs:

global existence, uniqueness and comparison for scalar Lipschitz ODEs on $[0,\infty)$ (Mathlib's IsPicardLindelof and Gronwall bounds are the starting point);
the elementary theory of the conjugate of a piecewise linear convex function.

Both are reusable beyond this mission. Proofs of individual milestones are welcome in any order. Lemmas 3, 4 and 6 are independent of the shooting lemmas.

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
B. Ata, J. M. Harrison, L. A. Shepp, Drift rate control of a Brownian processing system, Annals of Applied Probability 15(2), 1145–1160, 2005 (cited in the paper for the conjugate's minimal maximizer).
H. B. Keller, Numerical Methods for Two-Point Boundary-Value Problems, Dover, 2018 (cited for Lemma 4).

17 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research+2·Captain: mikedeng1

Partial Vertical Ownership, Capacity Investment, and Information Exchange in a Supply Chain II: Truthful Cheap Talk Is an Equilibrium Iff the Ownership Share β Is at Least β̳Research Paper

Motivation

A supplier who must build capacity before a selling season would like to know how large demand will be, and the retailer downstream often knows better. Under a simple wholesale-price contract, however, the retailer gains from overstating demand: more capacity means more sales for her, and the cost of idle capacity falls on the supplier. Since the retailer's message costs nothing and binds nobody, a rational supplier ignores it. That such cheap talk (Crawford and Sobel, 1982) cannot convey information in a one-shot wholesale-price relationship is the benchmark result of Özer, Zheng and Chen (2011), yet firms are observed to share forecasts informally.

Avinadav and Shamir propose an explanation based on partial vertical ownership (PVO): retailers often hold passive equity stakes in their suppliers. A retailer that owns a share $\beta$ of the supplier bears a fraction $\beta$ of the losses her misreport inflicts on him. Their Theorem 2 says exactly how large the stake must be for truthful reporting to be self-enforcing, and how this depends on the gap between the two possible demand levels. This mission formalizes that theorem.

Setting

A retailer sources a component from a supplier. The supplier secures capacity $K$ at unit cost $c$ ; after demand is realized, the retailer orders and pays the wholesale price $w$ per unit and sells at the retail price $r$ , with $0<c<w<r$ . Unmet demand is lost, and leftover capacity is worthless.

Demand in market state $i\in\{L,H\}$ is $D_i=\mu_i+\varepsilon$ with $0<\mu_L<\mu_H$ , where $\varepsilon$ is a zero-mean random variable with a density, distribution function $F$ , and lower support end $\underline{\varepsilon}<0$ satisfying $\mu_L+\underline{\varepsilon}\ge0$ . The information gap is $\Delta=\mu_H-\mu_L$ . Write $F^{-1}(z)=\inf\{x: F(x)\ge z\}$ and define the critical fractiles $z_s=1-c/w$ and $z_r=1-w/r$ .

The retailer may commit to an advance order $q^{adv}$ which the supplier must cover. The supplier's and retailer's 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].

A retailer holding the share $\beta\in[0,1]$ of the supplier 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})$ .

Only the retailer observes the state. In the cheap-talk game she places no advance order and announces a state; a supplier who believes the announcement builds the newsvendor capacity $K_L=\mu_L+F^{-1}(z_s)$ or $K_H=\mu_H+F^{-1}(z_s)$ . Truthful reporting requires

\text{(12)}\quad v_r(0,K_H\mid\mu_H)\ge v_r(0,K_L\mid\mu_H),\qquad\text{(13)}\quad v_r(0,K_L\mid\mu_L)\ge v_r(0,K_H\mid\mu_L).

Formalization targets

Goal: Theorem 2

Let

\underline{\underline{\beta}}=\frac{\pi_r(0,K_H\mid\mu_L)-\pi_r(0,K_L\mid\mu_L)}{\pi_s(K_L\mid\mu_L,0)-\pi_s(K_H\mid\mu_L,0)},\qquad R(d)=\frac1d\int_{F^{-1}(z_s)}^{d+F^{-1}(z_s)}F(x)\,dx\quad(d>0).

The goal asserts: (12) holds for every $\beta\in[0,1]$ ; for every $\beta\in[0,1]$ , (12) and (13) hold if and only if $\beta\ge\underline{\underline{\beta}}$ ;

\underline{\underline{\beta}}=\frac{z_r}{1-z_r}\left(\frac{1-z_s}{R(\Delta)-z_s}-1\right),\qquad R(\Delta)<1;

and for every $\beta\in(0,1]$ the equation $R(d)=z_s+\frac{1-z_s}{1+\beta(1/z_r-1)}$ has a unique root $\underline{\underline{\Delta}}>0$ , and truthful cheap talk is possible only if $\Delta\ge\underline{\underline{\Delta}}$ .

Milestones

In attack order: the closed forms (2) and (3) of the expected profits; condition (12) always holds; (E.1), that (13) is equivalent to $\beta\ge\underline{\underline{\beta}}$ with positive numerator and denominator; (E.2), the closed form of $\underline{\underline{\beta}}$ ; and the properties of $R$ (strictly increasing on $(0,\infty)$ , limits $z_s$ at $0^+$ and $1$ at $\infty$ , values in $(z_s,1)$ ). A companion item states Proposition 1: $\underline{\underline{\beta}}<1$ if and only if the integrated chain earns less with $K_H$ than with $K_L$ in the low state.

Significance

Theorem 2 identifies an ownership channel through which a one-shot wholesale-price relationship can sustain truthful information exchange, in contrast with the impossibility of cheap talk without such links. The threshold $\underline{\underline{\beta}}$ is the ratio of the low-type retailer's operational gain from lying to the supplier's loss from being misled, and part (ii) turns it into a lower bound on the information gap: a sufficiently small gap rules out cheap talk for every stake. Proposition 1 translates feasibility ( $\underline{\underline{\beta}}<1$ ) into a comparison of the integrated chain's profits. The same comparisons underlie the paper's later analysis of signaling with advance orders, which takes cheap talk as its benchmark.

The result is proved in the source, in Appendix E of the authors' manuscript; it has no machine-checked proof. The mission produces a formal statement in which every profit is an expectation over a general noise distribution, so that the closed forms the paper derives become theorems rather than definitions, together with the supporting analysis of the averaged distribution function $R$ .

Difficulty

The algebra after the closed forms is short. The work lies in two places. First, the closed forms (2) and (3) are integration-by-parts identities for expectations of truncated linear functions of $\varepsilon$ , under a general law rather than a density on a compact interval, including the case of an upper support end at $+\infty$ . Second, the properties of $R$ : the paper differentiates $R$ and applies L'Hôpital's rule, which presumes more regularity than the standing assumptions give; positivity of the numerator and denominator of $\underline{\underline{\beta}}$ , the strict bounds $z_s<R<1$ , and the existence and uniqueness of $\underline{\underline{\Delta}}$ all rest on continuity and strict increase of $F$ near $F^{-1}(z_s)$ . The case $\beta=0$ in part (ii) is degenerate: the argument of $R^{-1}$ is then $1$ , which $R$ never attains.

Formalization scope

The source is the authors' manuscript of 2022-06-06; theorem numbers, equation numbers and pages are the manuscript's. The model is a structure with real fields $c,w,r,\mu_L,\mu_H,\underline{\varepsilon}$ and a measure $P$ on $\mathbb R$ (the law of $\varepsilon$ ), with $F=$ cdf P. Every theorem assumes the standing hypotheses:

$P$ is a probability measure, absolutely continuous with respect to Lebesgue measure;
$\varepsilon$ is integrable with mean zero (integrability is implicit in "zero-mean");
$\underline{\varepsilon}<0$ , $F(\underline{\varepsilon})=0$ , and $F$ is strictly increasing on $\{x\ge\underline{\varepsilon}:F(x)<1\}$ (added: the paper uses $F^{-1}$ as an inverse);
$0<\mu_L<\mu_H$ , $\mu_L+\underline{\varepsilon}\ge0$ , and $c<w<r$ together with the added $c>0$ .

The profits $\pi_s,\pi_r,v_r$ are Bochner integrals against $P$ , $\underline{\underline{\beta}}$ is the plain quotient of profit differences (the first expression of (14)), and conditions (12)–(13) are the payoff comparisons themselves. Defining any of these by the paper's closed forms would make the milestones definitional and is ruled out. $R$ is used only at $d>0$ ; $\underline{\underline{\Delta}}$ is characterized as the unique positive root rather than through a junk inverse, and part (ii) is stated for $\beta\in(0,1]$ . The supply-chain profit $\pi_{sc}$ is taken at advance order $0$ , as in the proof of Proposition 1. The prior over market states and the signaling and pooling equilibria (Theorems 3–4) are outside this mission.

Mathlib provides distribution functions, Bochner and interval integrals and limits. A complete development needs layer-cake identities for $\mathbb E[\min(K,\cdot)]$ and $\mathbb E[(\cdot)^+]$ in terms of $\int F$ , continuity of the CDF of an absolutely continuous law, and the monotonicity and limits of interval averages of a monotone function; these are reusable well beyond this model. Proofs of any milestone, or of general lemmas they need, are welcome.

Selected references

T. Avinadav and N. Shamir, Partial Vertical Ownership, Capacity Investment, and Information Exchange in a Supply Chain, Management Science, 2023 (authors' manuscript of 2022-06-06). https://doi.org/10.1287/mnsc.2023.4673
V. P. Crawford and J. Sobel, Strategic Information Transmission, Econometrica 50(6), 1982. https://doi.org/10.2307/1913390
Ö. Özer, Y. Zheng and K.-Y. Chen, Trust in Forecast Information Sharing, Management Science 57(6), 2011. https://doi.org/10.1287/mnsc.1110.1348

8 thms2 active usersReviewed

Completed

Economics Operations Research Optimization+1·Captain: mikedeng1

Partial Vertical Ownership, Capacity Investment, and Information Exchange in a Supply Chain I: Under Complete Information the Retailer Finances the Entire Capacity Iff β ≥ β̲, and β̲ < 1Research Paper

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

9 thms2 active usersReviewed

Completed

Dynamical Systems Economics Operations Research+1·Captain: mikedeng1

Minimum Earnings Regulation and the Stability of Marketplaces II: Without Subsidies a Utilization Shock u₀ Can Be Absorbed Exactly When u₀ ≥ M/J(C(M))Research Paper

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)

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))$ .
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$ .
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

6 thms2 active usersReviewed

Completed

Dynamical Systems Economics Operations Research+1·Captain: mikedeng1

Minimum Earnings Regulation and the Stability of Marketplaces III: A Minimum Earnings Marketplace Is Dynamically Stable Exactly When It Is Statically StableResearch Paper

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.

A statically stable marketplace is stable.
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.
Along the same kind of policy, if $w_t\ge M/u_t$ for some $t$ , the marketplace is statically stable.
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]).

7 thms2 active usersReviewed

Completed

Control Theory Dynamic Programming Operations Research+1·Captain: mikedeng1

A Dynamic Model for Managing Volunteer Engagement II: The Bellman Solution in Closed Form Between Consecutive Engagement ThresholdsResearch Paper

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

(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).

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].

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

6 thms2 active usersReviewed

Analysis Numerical Analysis Operations Research+1·Captain: mikedeng1

A Generalized Newton Method for Subgradient Systems 1: Under Metric Regularity and Semismoothness*, the Prox-Based Newton Algorithm Converges Superlinearly for Prox-Regular FunctionsResearch Paper

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

17 thms2 active usersReviewed

All missions

Guarantees in Fair Division: General or Monotone Preferences 2: For Monotone Preferences the Moving Knife Guarantee Lies Between minMax and Maxmin and the Bid & Choose Guarantee Is at Most MaxminResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 iii), the provable part

Milestones

Significance

Difficulty

Formalization scope

Selected references

Load Balancing Under Strict Compatibility Constraints 1: On Proportionally Sparse Subcritical Compatibility Graphs, JSQ(d) Has the Fully Flexible Mean-Field Limit and Steady StateResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.4

Milestones, in the order the proof uses them

Significance

Difficulty

Formalization scope

Selected references

Online Stochastic Max-Weight Bipartite Matching: Beyond Prophet Inequalities: Rounding LP-Match Online Earns 0.51 of the Optimal Online AlgorithmResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1.2

The path

Significance

Difficulty

Formalization scope

Selected references

Linear Programming and Community Detection 1: Minimum Bisection Recovers the Planted Bisection When d_in − d_out > n/4 − 1Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 4)

Milestones: the three inequalities of the proof (p. 5)

Significance

Difficulty

Formalization scope

Selected references

A Generalized Newton Method for Subgradient Systems 2: Under Metric Regularity and Semismoothness*, the FBE-Based Newton Algorithm Converges Superlinearly in Quadratic Composite OptimizationResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 7.8

Milestones

Significance

Difficulty

Formalization scope

Selected references

Managing Outpatient Service with Strategic Walk-ins I: With Total Capacity μ ≤ √(λC_D/(2R)), the Observable Scheduling Setting Costs No More Than the Unobservable OneResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (1)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Breaking the Sample Size Barrier in Model-Based Reinforcement Learning with a Generative Model 4: Finite-Horizon Model-Based Planning Is ε-Optimal w.p. 1−δ Once N ≥ c₀H³log(H|S||A|/δ)/ε²Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4 (p. 10)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Sharing Sequentially Triggered Losses: Automated Conflict Resolution Through Smart Contracts 4: On Loss Trees the Same Four Axioms Characterize the Fixed-Fraction RulesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4

Milestones

Significance

Difficulty

Formalization scope