Operations Research

Motivation

Classical mechanism design assumes that agents optimize exactly: a buyer facing a menu of lotteries picks the one that maximizes expected utility, and an incentive compatible (IC) mechanism makes truth-telling optimal. Buyers that are only approximately rational, or that face small costs of computing or reporting, need only be made to prefer the truth up to a slack $\varepsilon$. Approximate incentive compatibility ($\varepsilon$-IC) is the corresponding relaxation of the IC constraints. It is also used in computer science as a robustness notion and in learning settings where a mechanism is only approximately optimal for the buyer.

Balseiro, Besbes and Castro (arXiv:2103.03403) ask how much revenue a seller of one item can gain from such a relaxation. For a single buyer, Myerson's theory gives the IC optimum as a posted price. With $\varepsilon$-IC the feasible set grows, and the paper determines the order of the additional revenue as $\varepsilon\downarrow 0$.

Timeline. The rounding argument attributed to Noam Nisan, first used by Balcan, Blum, Hartline and Mansour (FOCS 2005), turns an $\varepsilon$-IC mechanism into an IC one with a small revenue loss; for a single buyer it bounds the gain by $O(\sqrt\varepsilon)$ for every distribution (Proposition 1 of the paper). Balseiro, Besbes and Castro (2021; v2 2022; Operations Research 2024) prove an $\tilde O(\varepsilon^{\alpha/(2\alpha-1)})$ upper bound (Theorem 1) under a curvature condition on the revenue curve, show that deterministic mechanisms gain only $\Theta(\varepsilon)$ (Theorem 2), and give a matching $\Omega(\varepsilon^{\alpha/(2\alpha-1)})$ lower bound by an explicit randomized construction (Theorem 3). This mission formalizes the lower bound.

Setting

A seller sells one item to one buyer. The buyer's value $v$ has a cumulative distribution function $F$ with density $f$ supported on $S=[0,\bar v]$, $\bar v>0$. Assumption 1 requires $f$ to have bounded variation on $S$. Write $\bar F=1-F$, the revenue curve $R(v)=v\,\bar F(v)$ (the revenue of a posted price $v$), and $\dot R(v)=\bar F(v)-v f(v)$.

A direct mechanism $m=(x,t)$ gives a buyer who reports $v$ the item with probability $x(v)\in[0,1]$ and charges $t(v)$. It is individually rational (IR) if $v\,x(v)-t(v)\ge 0$ for all $v\in S$, and $\varepsilon$-incentive compatible (IC$_\varepsilon$) if

$$v\,x(v)-t(v)\ \ge\ v\,x(v')-t(v')-\varepsilon\qquad\forall v,v'\in S.$$

$\mathcal M(\varepsilon)$ is the set of IR and IC$_\varepsilon$ mechanisms, $\Pi(m)=\int_0^{\bar v}t(v)f(v)\,dv$ the expected revenue, and $\Pi^\star(\mathcal M(\varepsilon))=\sup_{m\in\mathcal M(\varepsilon)}\Pi(m)$. A best reporting mapping $v^\star$ for $m$ picks, for each value $v$, a report in $\arg\max_{w\in S}\{v\,x(w)-t(w)\}$.

Local $\alpha$-power envelopes (Definition 1): $R$ has a unique maximizer $p^\star$ on $S$, interior, and there are $\alpha>1$, $\kappa_L,\kappa_U>0$ and $\ell>0$ with $(p^\star-\ell,p^\star+\ell)\subset(0,\bar v)$ and

$$\kappa_L\alpha|v-p^\star|^\alpha\le(p^\star-v)\,\dot R(v)\le\kappa_U\alpha|v-p^\star|^\alpha\quad\text{on }(p^\star-\ell,p^\star+\ell).$$

The parameter $\alpha$ measures how flat $R$ is at its peak; $\alpha=2$ is the generic smooth case.

Perturbed delayed mechanisms (§5.1). For $\mu,\delta>0$ the buyer is steered to report $v^\star(v\,|\,\mu,\delta)$, equal to $0$ below $p^\star-\delta$, to $v-\mu$ on $[p^\star-\delta,p^\star+\delta+\mu]$, and to $p^\star+\delta$ above. With $w$ its generalized inverse, the allocation $x_{pd}$ solves on $[0,p^\star+\delta]$ the ordinary and delay differential equations

$$\dot x(v)=\frac{x(v)}{w(v)-v}\ \ (v\le p^\star-\delta),\qquad x(0)=\frac{\varepsilon}{p^\star-\delta},\qquad \dot x(v)=\frac{x(v)-x(v^\star(v))}{w(v)-v}\ \ (p^\star-\delta\le v\le p^\star+\delta),$$

is $1$ above $p^\star+\delta$, and the payment $t_{pd}$ is given explicitly in terms of $x_{pd}$ and $v^\star$.

Formalization targets

Goal: Theorem 3 (p. 27)

Under Assumption 1 and local $\alpha$-power envelopes there are $C>0$ and $\varepsilon_0>0$ such that for all $\varepsilon\in(0,\varepsilon_0]$ some $m\in\mathcal M(\varepsilon)$ satisfies

$$\Pi(m)\ \ge\ \Pi^\star(\mathcal M(0))+C\,\varepsilon^{\alpha/(2\alpha-1)} .$$

The constants may depend on the distribution, but not on $\varepsilon$.

Milestones

1. Lemma 5 (p. 59): solutions of (ODE)-(DDE) are non-decreasing on $[0,p^\star+\delta]$.
2. Proposition 3 (p. 31): if $x_{pd}(v)\to 1$ as $v\uparrow p^\star+\delta$, then $v^\star(\cdot\,|\,\mu,\delta)$ is a best reporting mapping for $m_{pd}$.
3. Proposition 4 (p. 33): the system has a unique solution on $[0,p^\star+\delta]$, which is positive, non-decreasing and given in closed form (eq. (25)).
4. Lemma 6 (p. 60): with $\Gamma(t)=\sum_{j=0}^{\lfloor t\rfloor+1}\frac{(-1)^je^{-j}}{j!}(t+1-j)^j$,

$$2(t+1)e^{-1}e^{-t}<\Gamma(t)\le2(t+2)e^{-(t+1)}\qquad(t\ge0).$$

5. Proposition 5 (p. 34): for $\mu>\varepsilon e$ some $\delta\in[\mu^2/(4\varepsilon)-\mu,\ \mu^2/(4\varepsilon)]$ makes $x_{pd}$ reach $1$ at $p^\star+\delta$, and then $m_{pd}\in\mathcal M(\varepsilon)$.
6. Proposition 6 (p. 35): the revenue identity

$$\Pi(m_{pd})=\int_0^{p^\star+\delta}x_{pd}(v)\big(vf(v)-\bar F(v+\mu)\dot w(v)\big)dv+R(p^\star+\delta)+\int_{p^\star+\delta}^{p^\star+\delta+\mu}\bar F(v)\,dv .$$

Significance

The result. Theorem 3 shows that the $\tilde O(\varepsilon^{\alpha/(2\alpha-1)})$ upper bound of Theorem 1 is tight up to the logarithm. Since $\alpha/(2\alpha-1)<1$ for $\alpha>1$, the revenue gain from approximate incentive compatibility is supralinear in $\varepsilon$: a seller who exploits $\varepsilon$-optimizing buyers gains strictly more than the order-$\varepsilon$ gain available to deterministic mechanisms (Theorem 2). Randomization is therefore what makes the relaxation valuable, and the curvature $\alpha$ of the revenue curve at the optimal price determines the exponent, which ranges from $1$ (as $\alpha\downarrow1$) to $1/2$ (as $\alpha\to\infty$), the latter matching Nisan's universal bound.

Formalizing it. The result is proved in the paper's online appendix; none of it is formalized. A formal development would supply a machine-checked revenue lower bound for an explicit class of $\varepsilon$-IC mechanisms, a formal treatment of a linear delay differential equation with a piecewise history (method of steps, closed-form solution), and the two-sided bound on $\Gamma$, which the paper derives from the renewal function of uniform interarrival times.

Difficulty

The obvious approach, perturbing the optimal posted price or a hard/soft floor mechanism, gains only order $\varepsilon$ (Theorem 2). To gain more, the mechanism must make the buyer misreport downward in a coordinated way, and the allocation that sustains a prescribed misreporting strategy is the solution of a delay differential equation. Three steps are delicate: showing that this solution exists, is unique and is monotone (the delay term couples $x(v)$ to $x(v-\mu)$); choosing the delay $\delta$ so that the allocation reaches exactly $1$ at $p^\star+\delta$, which requires the sharp two-sided bound on $\Gamma$ and an intermediate value argument; and verifying global $\varepsilon$-IC, since a best-response argument must rule out every deviation, not only local ones. The final bound balances the gain $\bar F(p^\star+\delta+\mu)\,\mu$ against losses of order $\kappa_U(\delta+\mu)^\alpha$, with $\mu$ of order $\varepsilon^{\alpha/(2\alpha-1)}$.

Formalization scope

Values are reals, every function is a total function $\mathbb R\to\mathbb R$ whose values matter only on $S=[0,\bar v]$, and the density is integrable on $S$ with total mass $1$. Mechanisms are required to be measurable, which the expectation $\mathbb E_v[t(v)]$ presumes. $\Pi^\star$ is a supremum (sSup); the goal is stated with an explicit witness $m\in\mathcal M(\varepsilon)$, which is equivalent because the revenue image is nonempty and bounded above by $\bar v$. $\dot R$ is defined as $\bar F-vf$, not as a derivative. The $\Omega$ constants are quantified after the distribution and before $\varepsilon$.

The derivatives in (ODE)-(DDE) are one-sided at the endpoints of their closed intervals. At $p^\star-\delta$ the two right-hand sides differ, so a two-sided derivative would make the system unsolvable and every statement about its solutions vacuous; this encoding rules out that trivialization. The goal does not mention perturbed delayed mechanisms: any witness is acceptable.

Disclosed additions relative to the page: $\mu\le p^\star-\delta$ in the §5.1 statements (presumed by the paper's definition of $w$); Propositions 3–6 and Lemma 5 are stated for any price $p^\star$ with $0<\delta<p^\star$ and $p^\star+\delta+\mu<\bar v$, since their proofs never use optimality of $p^\star$; in Proposition 6 the integrand $\psi\cdot f$ is written in product form because $\psi$ divides by $f$.

A complete development needs: absolutely continuous distribution functions and integration by parts on intervals; existence and uniqueness for linear ODEs and for a delay equation by the method of steps; Irwin–Hall distributions or a direct analytic bound for Lemma 6; and the intermediate value theorem. The delay-equation and $\Gamma$ results are reusable outside mechanism design. Contributions to any milestone, and alternative proofs of Lemma 6, are welcome.

Selected references

• S. R. Balseiro, O. Besbes, F. Castro, Mechanism Design under Approximate Incentive Compatibility, arXiv:2103.03403v2, 2022; Operations Research, 2024. https://arxiv.org/abs/2103.03403
• M.-F. Balcan, A. Blum, J. D. Hartline, Y. Mansour, Mechanism Design via Machine Learning, FOCS 2005, 605–614. https://doi.org/10.1109/SFCS.2005.50
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 58–73, 1981. https://doi.org/10.1287/moor.6.1.58
• P. Milgrom, I. Segal, Envelope Theorems for Arbitrary Choice Sets, Econometrica 70(2), 583–601, 2002. https://doi.org/10.1111/1468-0262.00296
• R. D. Driver, Ordinary and Delay Differential Equations, Springer, 1977 (reprint 2012). https://doi.org/10.1007/978-1-4684-9467-9

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

1. $u^\kappa$ and $u^\theta$ decrease weakly in $t^1$ and increase weakly in $t^2$ (p. 19).
2. Lemma 4 i), knife part: $u^\kappa$ is continuous on the triangle $0\le t^1\le t^2\le1$.
3. 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})$.
4. An equalising knife sequence cuts $\Omega$ into an $n$-equipartition (proof of Theorem 2).
5. The trimming step and Proposition 1 ii): for $u\in\mathcal M^+(\Omega)$, minMax and Maxmin are the infimum and supremum of equipartition utilities.
6. 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

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

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:

1. The second pick may re-draw the very bin that just rejected.
2. 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

Motivation

Reward-based crowdfunding platforms such as Kickstarter let a project creator collect pledges from the public for a fixed period. Two numbers are fixed before launch and cannot be changed afterwards: the pledge level $p$ each backer pays, and the campaign duration $T$. A high pledge level earns more per backer but deters backers with low valuations; a long campaign gives more backers time to arrive but, because backers are paid out only at the end, discounts the project's value in their eyes. Zhang, Savin and Veeraraghavan (SSRN 3065267, published in Manufacturing & Service Operations Management, 2022, doi:10.1287/msom.2022.1147) model this trade-off as a revenue-management problem for a deterministic fluid model of the pledging process, with two kinds of backers: independent backers, who arrive on their own, and herding backers, who arrive at a rate proportional to the amount already pledged, in the spirit of the imitators of the Bass diffusion model. The mission formalizes the paper's model, its closed-form solution, and its main optimization result for valuations with a right-triangular distribution.

Setting

A campaign has a population $\hat I>0$ of independent backers, who arrive at rate $k>0$ times the number not yet arrived, and herding backers, who arrive at rate $\Lambda_h q p$ times the number of pledges made so far ($\Lambda_h\ge0$ an arrival rate, $q\ge0$ a propensity). A backer's valuation $V$ is drawn from a law on $[0,\bar v]$ with survival function $\bar F_i$ (independent) or $\bar F_h$ (herding). A backer arriving at time $t\in[0,T]$ pledges iff $Ve^{-r(T-t)}\ge p$, where $r>0$ is the backers' discount rate; that happens with probability $\bar F(pe^{r(T-t)})$. The numbers $n^p_i,n^l_i$ of pledging and lost independent backers obey the linear system (1)–(4),

$$\frac{dn^p_i}{dt}=k(\hat I-n_i)\,\bar F_i(pe^{r(T-t)}),\qquad \frac{dn^l_i}{dt}=k(\hat I-n_i)\bigl(1-\bar F_i(pe^{r(T-t)})\bigr),\qquad n_i=n^p_i+n^l_i,$$

and the herding counts $n^p_h,n^l_h$ obey (8)–(10),

$$\frac{dn^p_h}{dt}=\Lambda_h q p\,(n^p_i+n^p_h)\,\bar F_h(pe^{r(T-t)}),\qquad \frac{dn^l_h}{dt}=\Lambda_h q p\,(n^p_i+n^p_h)\bigl(1-\bar F_h(pe^{r(T-t)})\bigr),$$

all starting from $0$. The total number of pledges is $n(p,T)=n^p_i(T)+n^p_h(T)$, the revenue is $\pi(p,T)=p\,n(p,T)$, and the creator solves

$$\max\ \pi(p,T)\quad\text{over}\quad 0<p\le\bar v,\ \ 0\le T\le\tfrac1r\ln(\bar v/p).\qquad(18)$$

Two reduced revenue functions appear in the limiting regimes: without herding, $R_i(p,T)=k\hat Ipe^{-kT}\int_0^Te^{kx}\bar F_i(pe^{rx})dx$ (22); in the herding-dominated regime, the proxy $R_h(p,T)=p\int_0^T\bar F_h(pe^{ry})dy$ (27). A right-triangular law on $[0,\bar v]$ has mode $0$ ($\bar F(y)=(1-y/\bar v)^2$) or mode $\bar v$ ($\bar F(y)=1-(y/\bar v)^2$).

Formalization targets

Goal: Proposition 7

With $x^*_0$, $x^*_1$ the explicit algebraic constants (34), (35):

• (a) if $k=r$ and $\Lambda_h=0$, the unique maximizer of (18) is

$$(p^*,T^*)=\Bigl(\bar v\tfrac{x^*_0-\sqrt{x^*_0}+1}{(x^*_0)^2+x^*_0+1},\ \tfrac1r\ln x^*_0\Bigr)\ \text{(mode 0)},\qquad \Bigl(\tfrac{\bar v}{\sqrt{1+x^*_1+(x^*_1)^2}},\ \tfrac1r\ln x^*_1\Bigr)\ \text{(mode }\bar v);$$

• (b) the unique maximizer of $R_h$ over the same feasible set is $(\beta^*\bar v,\frac1r\ln\frac1{\beta^*})$ with $\beta^*$ the unique root in $(0,1)$ of $\ln\frac1\beta=\frac32(\beta-\frac43)^2-\frac16$ (mode 0), and $(\beta\bar v,\frac1r\ln\frac1\beta)$ with $\beta=\sqrt{-W(-3e^{-3})/3}$ (mode $\bar v$).

Milestones

1. Proposition 1 and Proposition 2: every solution of (1)–(4) and (8)–(10) equals the closed forms (5)–(7), (11)–(12), and these solve the systems.
2. Corollary 2: $n(p,T)$ equals the single integral (17); and (22): $\pi=R_i$ when $\Lambda_h=0$.
3. Proposition 4(a), (b): with $\Lambda_h=0$, $k=r$, the optimal duration $T^*(p)$ for each fixed $p$ and the optimal pledge level $p^*(T)$ for each fixed $T>0$, in closed form (23)–(26).
4. Proposition 5(a), (b): the same for $R_h$, (28)–(31).

Significance

Proposition 7 is the paper's answer, for triangular valuations, to the question that motivates it: how a creator should set both levers together. Its four cases show how the optimal pledge level and duration move between campaigns dominated by low- or high-valuation independent backers and those dominated by herding backers; in particular herding-dominated campaigns call for markedly longer durations. Propositions 4 and 5 are the "limited-flexibility" policies for platforms where one lever is fixed by convention, and they are what the joint optimization is built from.

The model results (Propositions 1–2, Corollary 2) are proved in the manuscript's Appendix. The proofs of Propositions 4, 5 and 7 are in the paper's online Technical Appendix, which is not part of the source this mission cites; the decomposition into milestones follows the statements of the main text. None of these results has a machine-checked proof. A formalization produces verified closed forms for a nonlinear-in-parameters pricing problem and pins down three printing slips of the source (below).

Difficulty

Propositions 1 and 2 concern linear ordinary differential equations whose coefficients jump whenever the valuation law has an atom, so the classical theory does not apply directly; solutions are absolutely continuous and must be handled in integral form, and uniqueness needs a Grönwall-type argument for measurable coefficients. Corollary 2 is an integration by parts and a change of variables inside a double integral with an exponential of an inner integral. For the optimization results the obstacle is not the first-order condition but the global statement: each "optimal" claim asserts a unique global maximizer over a curved feasible region whose boundary $T=\frac1r\ln(\bar v/p)$ is active in some cases (Proposition 5) and inactive in others (Proposition 4, Proposition 7(a)). The first-order conditions are cubic or quartic equations whose roots are given by trigonometric and Cardano-type formulas, and part (b) involves transcendental equations; matching the right root and excluding boundary maxima is where the work lies.

Formalization scope

The model is a structure Campaign with real parameters Ihat, k, r, Lh ($\Lambda_h$), q, vbar and the survival functions Fbi, Fbh. Standing assumptions: $\hat I,k,r,\bar v>0$, $\Lambda_h,q\ge0$, and each survival function is non-increasing, $[0,1]$-valued, $1$ below $0$ and $0$ from $\bar v$ on. The positivity $p>0$ is added to the feasible set of (18), since $\ln(\bar v/p)$ needs it and $\pi(0,T)=0$. The pledging probability $\mathbb P(Ve^{-r(T-t)}\ge p)$ is written $\bar F(pe^{r(T-t)})$. The differential systems are stated in integral form with continuity on $[0,T]$; Propositions 1–2 assert both that every solution equals the closed forms and that the closed forms solve the system. "Optimal" always means: feasible, attaining the maximum, and the unique point that does. For a fixed $T$ the optimal pledge level is posed only for $T>0$, because $\pi(\cdot,0)$ and $R_h(\cdot,0)$ vanish identically.

Three corrections of printing slips are part of the statements: (12) is stated with the factor $\Lambda_h q p$ of (9) and with the inner integration limits read as $u$; (39) has the second root $\beta=1$, so uniqueness is posed on $(0,1)$; (40) is printed with $i$ and a complex Lambert $W$, and is stated in the equivalent real form with $W(-3e^{-3})$ characterized as the unique $w\in(-1,0)$ with $we^w=-3e^{-3}$. Printed decimals (one of which, $0.191\bar v$ in (36), is wrong: the exact value is $\approx0.198\bar v$) are not part of any statement.

Trivializing formalizations are ruled out: $n(p,T)$ is built from (5) and (11), not defined as (17); the differential systems are integral equations, not their closed forms and not a classical-derivative condition that no solution of a discontinuous system satisfies; optimality is a unique-maximizer statement, not an sSup or a first-order condition; and part (b) maximizes the explicit function (27), not a limit $\Lambda_h\to\infty$.

The development needs interval integrals, the exponential, logarithm, square and cube roots from Mathlib, and a uniqueness argument for linear Volterra integral equations; the latter, and the change-of-variables identity behind (22) and Corollary 2, are reusable for other fluid models of diffusion. Proofs of any milestone, and alternative routes to Proposition 7 (for instance through the profile functions $T\mapsto\pi(p^*(T),T)$), are welcome.

Selected references

• J. Zhang, S. Savin, S. Veeraraghavan, Revenue Management in Crowdfunding, manuscript of May 26, 2021, SSRN 3065267. https://ssrn.com/abstract=3065267 — published in Manufacturing & Service Operations Management, 2022. https://doi.org/10.1287/msom.2022.1147
• F. M. Bass, A New Product Growth for Model Consumer Durables, Management Science 15(5), 1969, 215–227. https://doi.org/10.1287/mnsc.15.5.215
• R. M. Corless, G. H. Gonnet, D. E. G. Hare, D. J. Jeffrey, D. E. Knuth, On the Lambert W function, Advances in Computational Mathematics 5, 1996, 329–359. https://doi.org/10.1007/BF02124750

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