Operations Research

Motivation

A retailer who sees her own demand before her supplier does can decide how much of that knowledge to pass upstream. Sharing everything is not obviously best: the supplier uses the information to set his production quantity for his own benefit, and the retailer bears a cost when he under-produces. Candogan and Gurkan (SSRN 4378997; published in Management Science, 2024, doi:10.1287/mnsc.2023.03004) treat this as a Bayesian persuasion (information design) problem in the sense of Kamenica and Gentzkow (AER 2011): the retailer commits in advance to a signalling policy, and the supplier best-responds to the posterior belief that each signal induces. The paper characterizes the retailer's optimal policy in closed form for uniform demand. This mission covers its first main result, the case where one demand support is nested inside the other.

The question links the supply-chain literature on information sharing between firms, where sharing is usually all-or-nothing, with the persuasion literature, where optimal signals are typically partial.

Setting

The state is $\omega\in\{0,1\}$, with prior $p_0=\mathbb P(\omega=0)\in[0,1]$. Demand is $D_\omega$, where $D_0$ is uniform on $[a_0,b_0]$ and $D_1$ is uniform on $[a_1,b_1]$. The supports are nested: $0\le a_0\le a_1<b_1\le b_0$ and $a_0<b_0$.

A disclosure policy $\Gamma=(\pi,\mathcal M)$ is a finite message space $\mathcal M$ and conditional probabilities $\pi(m\mid\omega)$. After message $m$ the supplier holds the posterior

$$p=\frac{\pi(m\mid\omega=0)\,p_0}{\pi(m\mid\omega=0)\,p_0+\pi(m\mid\omega=1)(1-p_0)}.$$

Full disclosure sends message $m_i$ exactly in state $i$; no disclosure sends the same message in both states.

At belief $p$ the supplier solves the newsvendor problem

$$\min_{Q\ge 0}\; p\,\mathbb E\big[\xi(D_0-Q)^+ + (1-\xi)(Q-D_0)^+\big] + (1-p)\,\mathbb E\big[\xi(D_1-Q)^+ + (1-\xi)(Q-D_1)^+\big],$$

where $\xi=C_s/(C_s+C_e)\in(0,1)$ is his critical ratio (shortage cost $C_s$, excess cost $C_e$). A best-response profile $Q^*$ picks an optimal quantity $Q^*_p$ for every belief $p\in[0,1]$. The retailer pays the expected shortage $p\,\mathbb E(D_0-Q^*_p)^+ + (1-p)\,\mathbb E(D_1-Q^*_p)^+$ at the induced posterior. Her design problem (3) minimizes the expectation of this cost over the random posterior, jointly over policies $\Gamma$ and best-response profiles $Q^*$. The function $K(p)$ of (B.1) is her cost when both parties hold belief $p$.

The thresholds are

$$\xi_h=\frac{a_1-a_0}{b_0-a_0-b_1+a_1},\qquad \underline\tau(p)=\frac{p(a_1-a_0)}{b_0-a_0},\qquad \bar\tau(p)=1-\frac{p(b_0-b_1)}{b_0-a_0}.$$

Formalization targets

Goal: Theorem 1 (p. 9)

For every prior $p_0\in[0,1]$:

$$\xi\in[\xi_h,1)\Rightarrow\text{full disclosure is optimal};\qquad \xi\in[\underline\tau(p_0),\xi_h]\Rightarrow\text{no disclosure is optimal};$$ $$\xi\in(0,\underline\tau(p_0)]\Rightarrow\Gamma^*\text{ is optimal},\quad \pi^*(m_1\mid\omega=0)=\frac{1-p_0}{p_0}\,\frac{\xi(b_0-a_0)}{(a_1-a_0)-\xi(b_0-a_0)},\ \ \pi^*(m_1\mid\omega=1)=1.$$

Milestones

1. Proposition 1 (p. 8): the supplier's optimal quantity $Q^*_p$ is unique and has an explicit three-piece form in $(p,\xi)$.
2. (B.2) (p. 25): the optimal value of (3) is $\kappa(p_0)$, where $\kappa$ is the lower convex envelope of $K$ on $[0,1]$.
3. (B.5) (p. 28): $K$ in closed form when $\xi\le(a_1-a_0)/(b_0-a_0)$.
4. Lemma 1 (p. 25): $\kappa$ in the three regimes of $\xi$.
5. The $\Gamma^*$ display (p. 26): under $\Gamma^*$, message $m_0$ has probability $(p_0-\hat p)/(1-\hat p)$ and induces posterior $1$, and, when $p_0<1$ (so that $m_1$ has positive probability), $m_1$ induces $\hat p=\xi(b_0-a_0)/(a_1-a_0)$.

Significance

The result shows that the optimal amount of disclosure depends on the critical ratio. When $\xi$ is high the retailer reveals everything; in an intermediate band she reveals nothing; when $\xi$ is low she uses a two-message policy that always reveals the narrow-support state ($\omega=1$ always sends $m_1$) but pools part of the wide-support state with it. Corollaries 1–4 of the paper read the thresholds off this theorem (independence of the prior for large $\xi$, full disclosure when $a_0=a_1$, never full disclosure when $b_0=b_1$), and Theorem 2 of the paper, on the value of information design relative to full and no disclosure, is built on Lemma 1 and (B.5).

The paper proves the result in its Online Appendix, citing Kamenica and Gentzkow for the reduction to a convex envelope. None of it has been machine-checked. A formalization would make the persuasion reduction explicit for finite message spaces and best-response profiles, and would check the case analysis of the envelope, where the paper prints one overlapping-indicator slip (Lemma 1, case 3).

Difficulty

The obvious argument is to compare the three named policies and pick the cheapest. That is not a proof: optimality is over every policy on every finite message space, and it is only the convex-envelope reduction that cuts the comparison down to splittings of the prior into posteriors. The reduction itself requires showing that the attainable expected costs are exactly the convex combinations of values of $K$ at Bayes-plausible posteriors. The envelope computation then needs the shape of $K$: the supplier's quantity is piecewise defined, so $K$ is a piecewise rational function of $p$ whose convexity changes across the boundaries $\underline\tau(p)=\xi$ and $\bar\tau(p)=\xi$. In the low-$\xi$ regime $K$ is neither convex nor concave on $[0,1]$, so its greatest convex minorant is a genuine mixture of $K$ itself and a line segment, whose junction point $\hat p$ has to be located exactly.

Formalization scope

States are Fin 2; a policy on a finite type $M$ is a map $\pi : \mathrm{Fin}\,2\to M\to\mathbb R$ with nonnegative entries and rows summing to $1$. The paper does not bound $\mathcal M$; finite message spaces are a convention, and binary spaces already attain the optimum. Uniform expectations are interval integrals divided by the length. The supplier's cost is normalized by $C_s+C_e$ and parameterized by $\xi$, which leaves its minimizers unchanged. A message of probability zero is given posterior $0$ and weight $0$.

The supplier's response is defined as an argmin of (2), never by the closed form of Proposition 1, and optimality quantifies over all finite policies and all best-response profiles, never over the three named policies; a formalization that hard-codes either would make the goal a statement about a formula. $K$ is evaluated at the largest optimal quantity, which is the unique one under the mission's hypotheses. The envelope $\kappa$ is the published definition BiconvexProg.BranchBound.convexEnvelope (greatest convex minorant) on $[0,1]$.

Standing hypotheses, stated in every theorem: $a_0<b_0$, $a_1<b_1$, $0<\xi<1$, $p_0\in[0,1]$, and nesting $a_0\le a_1$, $b_1\le b_0$. The hypotheses $0\le a_0$, $0\le a_1$ are added: demand is nonnegative, and without them the constraint $Q\ge0$ can bind. Equal supports are allowed; the threshold $\xi_h$ is then $0/0=0$ in Lean and the goal remains true. Lemma 1's third case is formalized as the piecewise function its two indicators intend.

A complete development needs: the convex-envelope (concavification) theorem for finite-support distributions on $[0,1]$, the newsvendor quantile characterization for a mixture of uniforms, and calculus for piecewise rational functions. The first two are reusable beyond this mission. Contributions to any milestone are welcome.

Selected references

• O. Candogan, H. Gurkan, The Value of Information Design in Supply Chain Management, Management Science, 2024. SSRN preprint: https://ssrn.com/abstract=4378997; DOI: https://doi.org/10.1287/mnsc.2023.03004
• E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590
• R. Levi, G. Perakis, J. Uichanco, The Data-Driven Newsvendor Problem: New Bounds and Insights, Operations Research 63(6), 2015. https://doi.org/10.1287/opre.2015.1422

Motivation

Large retail platforms both host independent sellers and sell their own products, and they control the order in which products appear in search results. When the platform ranks its own product first regardless of relevance, it engages in self-preferencing. Regulators have treated this as a competition problem: the European Commission opened a second antitrust investigation into Amazon's treatment of its own retail offers in 2020 (CNBC, 2020), and search neutrality, the requirement that results be ranked by relevance alone, is the remedy most often proposed.

Zou and Zhou ask whether such a rule helps consumers once prices respond to it. Their model builds on the economics of prominence in consumer search (Armstrong, Vickers and Zhou, 2009), in which the product shown first is searched first and so enjoys a demand advantage. The answer they obtain is negative in an identifiable region: when the two competing products are similarly popular, search neutrality strictly lowers consumer surplus. This mission formalizes that result and the equilibrium analysis on which it rests.

Setting

A platform sells its own product $F$ and hosts a third-party seller of a competing product $T$; marginal costs are zero. A unit mass of consumers has unit demand. A product either matches a consumer (value $1$) or not (value $0$).

• A fraction $\alpha\in[0,1]$ of consumers are of type $f$: product $F$ matches them with probability $\rho_H$ and $T$ with probability $\rho_L$. The remaining $1-\alpha$ are of type $t$, with the probabilities reversed. Throughout, $1>\rho_H>\rho_L>0$. The parameter $\alpha$ is the popularity of $F$.
• Prices satisfy $p_F,p_T\in[0,1]$. The platform keeps a commission $r$ of the third party's revenue, so its profit is $\pi_F=p_FD_F+r\,p_TD_T$ and the third party's is $\pi_T=(1-r)p_TD_T$.
• A ranking assigns each type a prominent product. Consumers see both prices, search the prominent product for free, and search the other one at a cost $c\sim U[0,1]$. This yields the per-type demands of equations (1)–(2) of the paper: for prominent product $1$ and non-prominent product $2$ with match probabilities $\rho_1,\rho_2$,

$$d_1=\begin{cases}\rho_1(1-\rho_2^2p_1+\rho_2^2p_2),&p_1>p_2,\\ \rho_1,&p_1\le p_2,\end{cases}\qquad d_2=\begin{cases}\rho_2^2(1-\rho_1+\rho_1p_1-p_2),&p_1>p_2,\\ (1-\rho_1)\rho_2^2(1-p_2),&p_1\le p_2.\end{cases}$$

• Without search neutrality (NS), the sellers set prices simultaneously, and then the platform chooses, for each type, the prominent product that maximizes its expected profit from that consumer. An equilibrium is a price pair together with a ranking rule that is optimal at every price pair, such that no seller gains from a price deviation (anticipating the ranking it induces).
• With search neutrality (S), $F$ is prominent for type $f$ and $T$ for type $t$; an equilibrium is a Nash equilibrium in prices.
• Consumer surplus $CS$ is the expected surplus of a consumer, averaged over the search cost $c$ and the two types.
• Condition 1 is the low-commission region $r\le0.64\,\rho_L/\rho_H$ and $\rho_L\le0.975$, assumed throughout §4.1 of the paper.

Formalization targets

Goal: Proposition 3(1)

Under Condition 1 there are thresholds $\underline\alpha,\bar\alpha$, depending only on $(\rho_H,\rho_L,r)$, with

$$\underline\alpha<\alpha_2^S=\frac{\rho_L^2(1-r\rho_H)}{\rho_L^2(1-r\rho_H)+\rho_H}<\frac12<\alpha_3^S=\frac{\rho_H}{\rho_H+\rho_L^2}<\bar\alpha,$$

such that for every $\alpha\in[0,1]\cap(\underline\alpha,\bar\alpha)$, consumer surplus in every equilibrium with search neutrality is strictly smaller than in every equilibrium without it:

$$CS^{S}<CS^{NS}.$$

Milestones

The equilibria without neutrality: the price order $p_T\le p_F$ when $F$ is prominent for all (Appendix, p. 42); the closed-form equilibrium of that pricing game (cases (A)–(B), pp. 42–43); the statement of Lemma A1 (p. 42); Proposition 1 (p. 16) and the uniqueness claim before it. The equilibria with neutrality: the price order by $\alpha\lessgtr\frac12$ (pp. 44–45); cases (A2), (A3)/(B3) and (B2) (pp. 45–46); Proposition 2 (pp. 17–18). The two consumer-surplus displays (pp. 43–44 and 46). Proposition 3(2) and Corollary 1 are included as companion statements.

Significance

The result. Proposition 3(1) shows that a relevance-based ranking rule can backfire. Under self-preferencing the third-party product is never prominent, so its seller prices low to invite search, and this disciplines the platform's own price. Under neutrality each seller is prominent for the consumers who like its product best, and for similarly popular products both sellers charge the maximal price $1$; on $[\alpha_2^S,\alpha_3^S]$ consumer surplus with neutrality is exactly zero. The goal makes this precise and shows that the harmful region strictly contains that interval. It is the paper's central short-term finding and the basis of its policy discussion.

Formalizing it. No part of this analysis is machine-checked anywhere, and the platform has no model of consumer search with prominence. The source file contains the equilibrium derivations of §4.1 in its Appendix, but the proofs of Propositions 1–3 and of Lemma A1 are in an online appendix that is not part of the source; a formal proof would supply them. Several of the Appendix's closed forms are misprinted (the interior prices of cases (A1) and (B1), the thresholds $\alpha_1^S$ and $\alpha_4^S$), and the threshold $\alpha_1^{NS}$ misclassifies the boundary $\alpha=1$ when $\rho_L>\sqrt{2/(3-r)}$; the formal statements fix what is actually true.

Difficulty

The profits are piecewise quadratic with a kink at $p_F=p_T$, so first-order conditions do not characterize equilibria: every candidate must be checked against global deviations across the kink. Without neutrality, a deviation can also change the platform's ranking, so the deviating seller faces a different demand system; this is the content of Lemma A1 and the reason Condition 1 is needed. The obvious argument for the goal, "consumer surplus with neutrality is zero on $[\alpha_2^S,\alpha_3^S]$ and positive without it", proves only the closed interval. The strict extension to $(\underline\alpha,\bar\alpha)$ requires controlling the neutral equilibrium just outside that interval, in the regions (A2) and (B2), where it is no longer at the corner.

Formalization scope

• Parameters. $\rho_H,\rho_L,r,\alpha$ are real numbers with $0<\rho_L<\rho_H<1$, $0\le r\le1$ (the paper never states a range for $r$; Condition 1 forces $r<0.64$) and $\alpha\in[0,1]$. Condition 1 is the numbered form with "$\le$" (p. 15); the Appendix restates it with "$<$".
• Prices and deviations are restricted to $[0,1]$.
• Demands are the paper's equations (1)–(2), aggregated over types for any ranking.
• The ranking without neutrality is a rule from price pairs to rankings that maximizes the platform's per-consumer profit for each type at every price pair, ties broken arbitrarily. The equilibrium is subgame perfect: deviations are evaluated at the ranking the rule selects at the deviated prices.
• Consumer surplus is $\sum_k N_k\int_0^1 CS_k(c)\,dc$ with the per-consumer surplus written for an arbitrary ranking; the closed-form displays are theorems, not definitions.
• "The equilibrium" is read as "every equilibrium"; existence is a separate conjunct (Propositions 1–2), so the goal is not vacuous.
• Thresholds printed incorrectly in the Appendix ($\alpha_1^S$, $\alpha_4^S$) are existential; $\alpha_1^{NS}$, $\alpha_2^S$, $\alpha_3^S$ and the closed-form prices without neutrality are defined as printed. In Proposition 1, the corner $\alpha=1$ with $\rho_L>\sqrt{2/(3-r)}$ is excluded from the constant region.
• A formalization in which the ranking rule is free or optimal only at the equilibrium prices, in which consumer surplus is defined by its closed form, or in which the thresholds may depend on $\alpha$ or collapse to the interval $[\alpha_2^S,\alpha_3^S]$ would trivialize the goal; the statements rule each of these out.

A complete development needs elementary real analysis only: piecewise quadratic optimization on $[0,1]$, the integral $\int_0^1(a-c)^+dc=a^2/2$, and continuity of the neutral equilibrium in $\alpha$. The model definitions are shared, with the same names, with the companion mission on equal popularity and the commission rate. Proofs of any milestone are welcome, as are proofs of Lemma A1 and of uniqueness, whose arguments are not in the source.

Selected references

• T. Zou and B. Zhou, Self-Preferencing and Search Neutrality in Online Retail Platforms, Management Science (authors' manuscript), 2024. https://doi.org/10.1287/mnsc.2022.01795
• M. Armstrong, J. Vickers and J. Zhou, Prominence and Consumer Search, RAND Journal of Economics 40(2), 209–233, 2009. https://doi.org/10.1111/j.1756-2171.2009.00062.x
• S. Amaro, EU says Amazon breached antitrust rules, opens second investigation into its e-commerce business, CNBC, 2020. https://www.cnbc.com/2020/11/10/eu-hits-amazon-with-antitrust-charges-for-distorting-competition.html

Why self-preferencing is a regulatory question

Large retail platforms such as Amazon both host independent sellers and sell their own products in competition with them. The platform also controls the search ranking, the order in which products are shown to a consumer. The European Commission and the US Federal Trade Commission have examined whether platforms rank their own products ahead of rivals' (self-preferencing), and proposals of search neutrality would oblige a platform to rank products by relevance alone. The intuitive case for such a rule is that it protects consumers and third-party sellers.

T. Zou and B. Zhou, Self-Preferencing and Search Neutrality in Online Retail Platforms (Management Science, DOI 10.1287/mnsc.2022.01795), study this intuition in a duopoly model with consumer search and find that it can fail: when consumers see prices before searching, a platform free to steer consumers forces the third-party seller to cut its price to attract search, and neutrality removes that pressure. This mission formalizes their §4.2, which isolates the role of the commission rate $r$ the platform charges the third-party seller, at equal popularity of the two products.

Setting

A platform sells its own product $F$ and hosts a third-party seller of product $T$; production costs are zero. A unit mass of consumers has unit demand. A consumer of type $k\in\{f,t\}$ values a product at $1$ if it matches her taste and at $0$ otherwise. A type-$f$ consumer is matched by $F$ with probability $\rho_H$ and by $T$ with probability $\rho_L$; for a type-$t$ consumer the roles are swapped. Throughout, $0<\rho_L<\rho_H<1$. In this mission the two types have equal mass, $\alpha=1/2$.

Sellers set prices $p_F,p_T\in[0,1]$. The platform keeps a fraction $r$ of the third-party seller's revenue, so the profits are

$$\pi_F=p_FD_F+r\,p_TD_T,\qquad \pi_T=(1-r)\,p_TD_T,$$

where $D_j$ is the demand for product $j$.

For each consumer type the platform shows one product first: the prominent product. A consumer sees both prices before searching, learns whether the prominent product matches for free, and pays a search cost $c$, uniform on $[0,1]$, to inspect the other product. Optimal search yields the per-type demands (1)–(2) of the paper and a consumer surplus equal to the expected payoff of optimal search, averaged over types and over $c$.

Under search neutrality the ranking is fixed: $F$ is prominent for type $f$ and $T$ for type $t$. An equilibrium with neutrality is a pair of prices from which neither seller gains by a unilateral change. Without neutrality, the sellers set prices first and the platform then chooses, at whatever prices it sees, the ranking that maximizes its own profit from each consumer. An equilibrium is a pair of prices together with an optimal ranking rule $\sigma$, mapping prices to rankings, such that neither seller gains by changing its price, given that the ranking will respond.

Formalization targets

Goal: Proposition 5

At $\alpha=1/2$:

1. If $\rho_L/\rho_H<r<1$, search neutrality does not affect the outcome: every equilibrium without neutrality has the same prices, ranking, profits and consumer surplus as every equilibrium with neutrality.
2. If $0\le r<\rho_L/\rho_H$, every pair of equilibria satisfies

$$CS^{S}<CS^{NS},\qquad \pi_T^{NS}<\pi_T^{S}.$$

3. There is $\bar\rho<1$ such that, for $\bar\rho<\rho_L<\rho_H<1$ and every $r<\rho_L/\rho_H$, also $\pi_F^{NS}<\pi_F^{S}$.

Milestones

• Lemma 1 (p. 25): with neutrality the unique equilibrium is $p_F=p_T=1$, with $\pi_F=\rho_H(1+r)/2$ and $\pi_T=\rho_H(1-r)/2$.
• Proposition 4(1) (p. 24): without neutrality and with $r>\rho_L/\rho_H$, every equilibrium ranks neutrally and has $p_F=p_T=1$.
• The fixed-ranking game (Appendix, pp. 42–43): with $F$ prominent for all, the equilibrium is an explicit interior pair when $r<3-2/(\rho_H\rho_L)$ and $(1,\tfrac12)$ otherwise.
• Proposition 4(2) (p. 24): without neutrality and with $r<\rho_L/\rho_H$, every equilibrium makes $F$ prominent for all and has $p_F>p_T$; the prices are monotone in $r,\rho_H,\rho_L$ on the region $r\le 3-2/(\rho_H\rho_L)$ and equal $(1,\tfrac12)$ beyond it.
• The surplus display (Appendix, pp. 43–44): consumer surplus without neutrality as an explicit quadratic in the prices.

Significance

The result separates two regimes of a single policy question. With a high commission the platform already earns most of the revenue of product $T$ and has no incentive to steer; neutrality is then moot. With a low commission the platform steers every consumer to $F$; the third-party seller responds by pricing below $F$ to make search worthwhile, and consumers benefit from this competition. Imposing neutrality removes it, prices rise to $1$, and consumer surplus falls to zero, while the third-party seller gains. For high match probabilities the platform gains as well, which makes neutrality a commitment device a platform might accept voluntarily. Proposition 5 is the equal-popularity version of the paper's main short-term finding (Proposition 3, under a low commission), now valid for every commission rate.

The paper proves Proposition 5, Proposition 4 and Lemma 1 in an online appendix that is not part of the manuscript used here; the manuscript's own Appendix contains only the equilibrium derivations for the game with a fixed ranking. None of these results is machine-checked. A formalization would produce the first verified treatment of a pricing game with an endogenous, profit-maximizing ranking stage and of a consumer-surplus integral over search costs; the definitions are reusable for the companion mission on the low-commission regime and for other prominence models.

Difficulty

The demands are piecewise quadratic with a kink where the two prices cross, so profits are not concave on $[0,1]^2$, and first-order conditions only locate candidates. The central difficulty is the ranking stage. A seller's deviation can change the platform's ranking: the third-party seller may raise its price to make prominence for type $t$ worthwhile to the platform, and the platform as a seller may cut its price to undercut. Checking an equilibrium therefore requires comparing profits across ranking regimes at every deviation price, not only inside the regime of the candidate. The uniqueness claims require excluding equilibria in every regime, including those supported by an unusual tie-break of the ranking rule. The comparison of platform profits in part 3 compares the explicit interior prices of Proposition 4(2), a rational function of $(\rho_H,\rho_L,r)$, with $\rho_H(1+r)/2$; the paper gives no explicit threshold $\bar\rho$.

Formalization scope

• Parameters: $0<\rho_L<\rho_H<1$ and $0\le r<1$. The paper calls $r$ a percentage commission without stating its range; $r<1$ is needed because at $r=1$ the third-party seller's profit is identically zero and Lemma 1's uniqueness fails. Prices range over $[0,1]$ (p. 8).
• The equilibrium without neutrality is subgame perfect: the ranking rule must be optimal for the platform, type by type, at every price pair, and deviations are evaluated at the ranking chosen at the deviated prices. A ranking that is arbitrary, or optimal only at the equilibrium prices, would allow spurious equilibria and is ruled out by the definitions. Ties in the ranking may be broken arbitrarily, and statements about "every equilibrium" hold for every tie-break.
• "The equilibrium" is read as "every equilibrium"; existence is a separate conjunct of the milestones, so the comparisons of Proposition 5 are not vacuous.
• At the boundary $r=\rho_L/\rho_H$ the platform is indifferent for type-$t$ consumers at prices $(1,1)$, and two different equilibria exist depending on the tie-break. Statements about every equilibrium are made for $r>\rho_L/\rho_H$, and at the boundary only existence is claimed.
• Consumer surplus is defined from the search model as $\int_0^1$ over the search cost of the optimal-search payoff. It is not defined by the paper's closed-form display, which is a milestone.
• "Reduces" and "improves" in Proposition 5 and "increase/decrease" in Proposition 4(2) are read strictly. "Sufficiently large" is read as one threshold $\bar\rho<1$ independent of $r$.
• Definitions needed: two finite types, the demands (1)–(2), profits, ranking rules and their optimality, both equilibrium notions, and the surplus integral, all in SearchNeutrality.Commission.Model; the closed-form prices and surplus in SearchNeutrality.Commission.ClosedForms. These duplicate, with the same names, the definitions of the companion mission SearchNeutrality.ShortTerm.
• Contributions welcome: proofs of the milestones in any order, reusable lemmas on the per-type ranking comparison, and an explicit admissible $\bar\rho$.

Selected references

• T. Zou, B. Zhou, Self-Preferencing and Search Neutrality in Online Retail Platforms, Management Science (authors' manuscript), 2024. https://doi.org/10.1287/mnsc.2022.01795
• M. Armstrong, J. Vickers, J. Zhou, Prominence and consumer search, RAND Journal of Economics 40(2), 2009. https://doi.org/10.1111/j.1756-2171.2009.00067.x
• M. Armstrong, J. Zhou, Paying for prominence, Economic Journal 121(556), 2011. https://doi.org/10.1111/j.1468-0297.2011.02469.x

Motivation

Heavy-traffic analysis is the standard tool for scheduling queues whose servers are almost always busy: after diffusion scaling, a multiclass queue is approximated by a reflected Brownian motion, and asymptotically optimal policies are read off a limiting control problem. Classical results of this kind, such as the asymptotic optimality of the cµ rule (serve the class with the largest holding cost times service rate first; van Mieghem, 1995), assume that the job-size distributions are known.

In practice the first moments of service times are usually estimated well, while their variability is not. Atar, Castiel and Shadmi study a high-uncertainty regime: the means of the job-size distributions are pinned down to within $O(n^{-1/2})$, but their variances are uncertain at order one, and an adversary chooses them job by job with full knowledge of the past. The scheduler wants to minimize, and the adversary to maximize, a discounted holding cost. The paper solves this game asymptotically: the nonpreemptive cµ policy is asymptotically optimal against every adversary, and the value of the game converges to the value at $0$ of a one-dimensional Hamilton–Jacobi–Bellman (HJB) equation.

Setting

There are $L$ job types and one server. In the $n$-th system one job of each type arrives at each time $k/n$, $k=1,2,\dots$, and the server works at rate $n$, so that a job of size $x$ occupies it for $x/n$ time units. The system starts empty.

Adversary. For each $n$ and type $\ell$ an uncertainty class $\Pi^{\ell n}$, a nonempty closed set of probability distributions on $[0,\infty)$, is given. At each epoch $k/n$ the adversary chooses $\pi^{\ell n}_k\in\Pi^{\ell n}$ for every $\ell$, based on the past job sizes, and the job sizes $J^{\ell n}_k$ are then drawn independently across types from these distributions. The set of such controls is $\mathcal A^n$.

Scheduler. The scheduler chooses the cumulative effort $B^{\ell n}_t$ devoted to each type, an $L$-dimensional Lipschitz path whose increments over $[s,t]$ lie in $(t-s)\cdot\{x\in[0,1]^L:\sum_\ell x_\ell\le 1\}$. An admissible strategy $\beta^n\in\mathbb B^n$ is a measurable, non-anticipating, work-conserving map from the adversary's control path to such an effort path that never serves more work than has arrived.

Cost and value. With $A^{\ell n}_t=\sum_{k\le nt}J^{\ell n}_k$, the workload is $W^{\ell n}_t=A^{\ell n}_t-nB^{\ell n}_t$, the queue length $Q^{\ell n}_t$ is the number of arrived type-$\ell$ jobs not yet completed, and hats denote scaling by $n^{-1/2}$. For holding costs $h^\ell>0$,

$$C^n(\beta^n(a^n),a^n)=\mathbb E\Big[\int_0^\infty e^{-t}\,h\cdot\hat Q^n_t\,dt\Big],\qquad V^n=\inf_{\beta^n\in\mathbb B^n}\sup_{a^n\in\mathcal A^n}C^n(\beta^n(a^n),a^n).$$

Assumptions. With $\xi^\pi$ the mean and $q^\pi$ half the variance of $\pi$, and $b^{\pi\ell n}=n^{1/2}(\xi^\pi-1/\mu^\ell)$, the sets $K^{\ell n}=\{(b^{\pi\ell n},q^\pi):\pi\in\Pi^{\ell n}\}$ converge in the Hausdorff distance to compact sets $K^\ell\subset\mathbb R\times(0,\infty)$; fourth moments are uniformly bounded; $\sum_\ell 1/\mu^\ell=1$ (heavy traffic); and types are labelled so that $h^1\mu^1\le\dots\le h^L\mu^L$, with $h^1\mu^1=1$.

HJB equation. With $H^\ell(v_1,v_2)=\max_{(b,q)\in\mathrm{ch}(K^\ell)}(bv_1+qv_2)$,

$$\sum_{\ell=1}^L H^\ell(u'(w),u''(w))-u(w)+w=0,\quad w\ge0,\qquad u'(0)=0,\quad \limsup_{w\to\infty}|u(w)|/w<\infty .$$

Formalization targets

Goal: Theorem 2.1

$$V^n\longrightarrow u(0)\qquad(n\to\infty),$$

for the classical solution $u$ of the HJB equation. The paper states $V^n\to\mathsf V(0)=u(0)$ with $\mathsf V$ the value of a martingale control problem; the goal uses the $u(0)$ form, which leaves the martingale problem out of the statement.

Milestones

• β*ⁿ ∈ 𝔹ⁿ: the nonpreemptive cµ strategy is admissible.
• Lemma 2: the total workload does not depend on the strategy.
• Lemma 3: second moments of the scaled workload and queue length grow at most like $(t+1)^2$, uniformly in $n$, the control and the strategy.
• Lemma 4: $\hat Q^{\ell n}-\mu^\ell\hat W^{\ell n}\to0$ uniformly in probability over strategies (the snapshot principle).
• Lemma 5: under the cµ policy the workload of types $2,\dots,L$ vanishes.
• Theorem 1: $\inf_{\beta^n}C^n(\beta^n(a^n),a^n)-C^n(\beta^{*n}(a^n),a^n)\to0$ for every adversary.
• Proposition 1.1: the HJB equation has a unique classical solution. Proposition 1.3: it is nonnegative, non-decreasing and convex.
• (47): $\limsup_nC^n(\beta^{*n}(a^n),a^n)\le u(0)$ for every control sequence.
• Theorem 2.2: measurable selectors $\psi^{\ell n}$ attaining the prelimit Hamiltonian.
• (55): for the feedback control $\pi^{\ell n}_k=\psi^{\ell n}(\mathsf W^n_{k-1})$, $u(0)\le\liminf_nC^n(\beta^{*n}(a^{*n}),a^{*n})$.

Significance

The result gives the first-order asymptotics of a scheduling game with model uncertainty: the scheduler loses nothing by ignoring the adversary and using the cµ rule, and the adversary's best response is a state-feedback choice of drift and variance determined by $u'$ and $u''$. Theorem 1 is a robustness statement for one of the most widely used scheduling rules; Theorem 2 reduces a game on path space to a scalar nonlinear ODE.

The paper's proofs are complete, so the remaining work is formalization. No part of this result, and none of its objects (heavy-traffic queues with adversarial service distributions, the nonpreemptive cµ policy as a map on path space, the HJB equation of a reflected controlled diffusion), has a known machine-checked statement or proof.

Difficulty

The statement is a limit of a real sequence, but each term is an infimum over measurable, causal, work-conserving maps on path space of a supremum over feedback choices of distributions. The proofs (§§4–7 and the appendix) use uniform C-tightness of prelimit processes, weak convergence in $D[0,\infty)$, the existence theory for fully nonlinear uniformly elliptic equations (Gilbarg–Trudinger, Thm 17.18), martingale characterizations of limits (Jacod–Shiryaev, Cor. VI.6.30; Karatzas–Shreve, Thm 5.5.15), measurable selection (Budhiraja–Dupuis, Lemma 8.10), and Taylor expansion of $u$ along the prelimit workload. The obvious route through the uncontrolled diffusion limit fails because the adversary's variance choice is state dependent, so no single limiting Brownian motion describes all adversaries; the limit is a control problem, not a process.

Formalization scope

The Lean development lives in the namespace HighUncertHT.Game. Types are Fin L, 0-based (the paper's type 1 is index 0). Distributions are ProbabilityMeasure ℝ with no mass on $(-\infty,0)$, with the weak topology. Systems are indexed by $n\ge1$; the class at $n=0$ is required to satisfy the same conditions so that control sequences indexed by $\mathbb N$ exist. Costs and values are in $[0,\infty]$ (lower Lebesgue integrals), sup norms are in $[0,\infty]$, the Hausdorff distance is the extended one, and derivatives of $u$ are one-sided on $[0,\infty)$.

An adversary control is encoded by its feedback map from past job sizes to distributions and the measurable Markov kernel it induces; its law is the Ionescu–Tulcea trajectory measure. By (5), the Doob–Dynkin lemma and (7), this has the same laws, hence the same costs, as the paper's $\mathcal A^n$. Strategies are measurable for the product σ-algebras. The cµ strategy $\beta^{*n}$ is defined explicitly by an event recursion over service decisions.

The standing assumptions (Assumptions 1–2, labelling (14), $h^1\mu^1=1$) are fields of the Setting and hold in every statement. Corrected printed slips: the priority rule serves the highest index (p. 9 prints "lowest", contradicting the cµ rule and Lemma 5); the departure count is capped at the number of arrived jobs (p. 6); "→ 0 in probability" for processes is read as convergence of the sup norm on compact intervals (Lemma 5); (55) is stated for the control (61), not (15).

Trivializing formalizations are ruled out: $\mathbb B^n$ is nonempty because $\beta^{*n}\in\mathbb B^n$ is a milestone; the HJB has a classical solution (Proposition 1.1), so the goal is not vacuous; no expectation is a Bochner integral that could vanish for non-integrable integrands; $u'$ is not a junk deriv; and (55) asserts that its feedback control exists.

Needed infrastructure: diffusion-scaled processes and their tightness in $D[0,\infty)$, the one-dimensional Skorokhod map and its Lipschitz property, martingale estimates for sums of conditionally centred job sizes, and the existence theory for the HJB equation. The Skorokhod map, the queue primitives and the cµ policy are reusable for other heavy-traffic missions. Contributions on any milestone, or on general lemmas they need, are welcome. Not included: Lemmas 1, 6, 7, 8, Proposition 1.2, Proposition 2, Theorem 2.3 and the martingale control problem.

Selected references

• R. Atar, E. Castiel, Y. Shadmi, Scheduling in the High Uncertainty Heavy Traffic Regime, Mathematics of Operations Research, 2025; preprint arXiv:2204.05733v1, 2022. https://arxiv.org/abs/2204.05733v1
• J. A. van Mieghem, Dynamic scheduling with convex delay costs: the generalized cμ rule, Annals of Applied Probability 5(3), 1995. https://doi.org/10.1214/aoap/1177004702
• M. I. Reiman, Some diffusion approximations with state space collapse, in Modelling and Performance Evaluation Methodology, Springer LNCIS 60, 1984. https://doi.org/10.1007/BFb0005161
• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Springer, 2001. https://doi.org/10.1007/978-3-642-61798-0
• A. Budhiraja, P. Dupuis, Analysis and Approximation of Rare Events, Springer, 2019. https://doi.org/10.1007/978-1-4939-9579-0

Motivation

In adaptive video streaming and online gaming, tasks are dispatched to one of $n$ identical server pools; all tasks in a pool are served in parallel, so a task's duration does not depend on the load, but its quality of service does. The total number of tasks then does not depend on how tasks are dispatched (the pools together form an infinite-server system), and the relevant objective is a balanced distribution of tasks over the pools: every Schur-concave utility of the occupancy vector, including the $\alpha$-fair utilities, rewards balance (Goldsztajn, Borst & van Leeuwaarden 2024, §1). Join the Shortest Queue is optimal for this purpose but needs the exact occupancy of every pool.

A threshold dispatching rule needs much less. With an integer $\Delta\ge1$ and a threshold $\ell_n$, it keeps every pool between $\ell_n$ and $h_n:=\ell_n+\Delta$ tasks whenever it can. Choosing $\ell_n$ well requires the offered load $\rho=\lambda/\mu$, which in practice is unknown and varies in time. The refined learning scheme of Goldsztajn, Borst and van Leeuwaarden adjusts $\ell_n$ online, in steps of $\Delta$, using the same coarse state information as the dispatcher. This mission formalizes their main result on that scheme (Theorem 2 of arXiv:2012.10142v3): along time intervals where the load is suitably bounded, the threshold settles at the right value and the load becomes balanced.

Timeline. The threshold rule with $\Delta=1$ and the fixed threshold $\lfloor\rho\rfloor$ was shown to have the same fluid and diffusion limits as Join the Shortest Queue for constant arrival rates and exponential service (Goldsztajn et al., INFORMS Journal on Computing, 2022). The present paper (arXiv 2020, revised 2024; Mathematics of Operations Research, 2025) removes the knowledge of $\rho$, allows a time-varying arrival rate, and proves almost-sure statements about the learned threshold.

Setting

Fix a horizon $T>0$, a measurable arrival-rate function $\lambda:[0,T]\to[0,C]$, a service rate $\mu>0$ and an integer $\Delta\ge1$. The system with $n$ pools receives tasks at rate $n\lambda(t)$; service times are exponential with rate $\mu$. The occupancy state $q_n(t)=(q_n(t,i))_{i\ge0}$ records the fraction $q_n(t,i)$ of pools with at least $i$ tasks, so it lies in

$$Q=\{q\in[0,1]^{\mathbb N}: q(i+1)\le q(i)\le q(0)=1\}.$$

The threshold $\ell_n(t)$ is a nonnegative multiple of $\Delta$. An arriving task goes to a pool, chosen uniformly at random, with fewer than $\ell_n$ tasks if there is one; otherwise to one with fewer than $h_n$ tasks if there is one; otherwise to any pool. The refined learning scheme with parameters $\alpha_n\in(0,1)$ acts at arrivals: if, right before the arrival, the fraction of pools with at least $\ell_n$ tasks is at most $\alpha_n$, the threshold drops by $\Delta$; if all pools have at least $\ell_n$ tasks and at least $n-1$ have at least $h_n$, it rises by $\Delta$.

All systems are built on one probability space from independent unit-rate Poisson processes $\mathcal N_i$, i.i.d. uniform selection variables $U_j$, and random initial conditions with $q_n(0)\to q(0)$ almost surely, $q_n(0,B+1)=0$ and $\ell_n(0)\le B$. The paths $(q_n,\ell_n)$ are the solutions of the implicit equations (9a)–(9b): arrivals follow $\mathcal N^\lambda_n(t)=\mathcal N_0(n\int_0^t\lambda)$ and are routed by the $U_j$; departures from pools with $i$ tasks follow $\mathcal N_i$ run at the clock $n\int_0^t\mu i[q_n(s,i)-q_n(s,i+1)]ds$.

The fluid total mass is $u(t)=u(0)e^{-\mu t}+\int_0^t\rho(s)\mu e^{-\mu(t-s)}ds$ with $u(0)=\sum_{i\ge1}q(0,i)$. On an interval $[a,b]\subset[0,T]$ let $\rho_{\min},\rho_{\max}$ be the infimum and supremum of $\rho$. The load is $(m,\Delta)$-bounded on $[a,b]$ (Definition 1) if $m\Delta<\rho_{\min}\le\rho_{\max}<(m+1)\Delta$ and $b-a$ exceeds an explicit constant $\sigma(a,b,m,\Delta)$ built from $\log\frac{\rho_{\min}}{\rho_{\min}-m\Delta}$ and $\big[\log\frac{u(a)-\rho_{\max}}{(m+1)\Delta-\rho_{\max}}\big]^+$.

Formalization targets

Goal: Theorem 2

Assume $\alpha_n\to1$ and $\liminf_n n^{\gamma_0}(1-\alpha_n)>0$ for some $\gamma_0\in(0,1/2)$, the load is $(m,\Delta)$-bounded on $[a,b]$, and $\sigma(a,b,m,\Delta)<\sigma<b-a$. Then almost surely

$$\lim_{n\to\infty}\sup_{t\in[a+\sigma,b]}|\ell_n(t)-m\Delta|=0,\qquad \lim_{n\to\infty}\sup_{t\in[a+\sigma,b]}n^{\gamma}|1-q_n(t,i)|=0\ \ (i\le m\Delta,\ \gamma\in[0,\tfrac12)),$$ $$\limsup_{n\to\infty}\sup_{t\in[a+\sigma,b]}\sum_{i>(m+1)\Delta}q_n(t,i)\,e^{\mu[t-(a+\sigma)]}\le u(a+\sigma).$$

Milestones

In the order of the proof: well-posedness of (9a)–(9b) (§5.1.1); Lemmas 21 and 22 and Proposition 4 (relative compactness); Lemmas 5 and 6 and Proposition 7 (the set $\Omega_T$ of nice sample paths); Proposition 8 ($u_n\to u$ uniformly); Proposition 9 (decay of tail masses below the threshold); Proposition 10 (the threshold eventually stays at most $m\Delta$ after $a+\sigma_{\mathrm{bd}}$); Corollary 11 (the bound (6c)); Lemmas 12 and 13 (the threshold locks at $m\Delta$).

Significance

The result. Theorem 2 shows that a scheme using only two bits of state per arrival finds the balancing threshold $m\Delta$ without knowing $\rho$, within the explicit time $\sigma(a,b,m,\Delta)$, which is tight for an initially empty system with constant load. It quantifies balance: the fraction of pools with fewer than $m\Delta$ tasks is $o(n^{-\gamma})$ for every $\gamma<1/2$, and the mass beyond column $(m+1)\Delta$ decays exponentially. Conditions (5) are sharp in kind: $\alpha_n\to1$ prevents settling too high, and the rate $n^{-\gamma_0}$ stops $O(\sqrt n)$ fluctuations from pushing the threshold down.

Formalizing it. The result is proved in the paper; nothing here is open mathematically. Nothing of it is machine-checked. A formal proof would add an almost-sure coupled construction of a many-server Markov process on Poisson primitives, a rate-$n^{-\gamma}$ functional strong law for the Poisson process, and a pathwise relative-compactness argument in the uniform topology. None of these is in Mathlib.

Difficulty

The usual fluid-limit route fails here. The learning scheme reacts to excursions of the occupancy process of vanishing size: a threshold increase needs $n q_n(h_n)\ge n-1$, a decrease $q_n(\ell_n)\le\alpha_n$ with $\alpha_n\to1$. So the threshold is not a continuous function of the fluid state, and limits of $(q_n,\ell_n)$ need not satisfy any closed ODE. The natural first idea, deriving a limiting ODE for $(q,\ell)$ jointly and studying its equilibria, fails for exactly this reason: whether the threshold moves is decided by fluctuations of order $n^{-1/2}$ around the fluid path, which a law of large numbers does not see. The statements must therefore hold almost surely and uniformly in time for the coupled sequence, not in law.

Formalization scope

• Model. UnknownLoads.Refined.LoadData holds $T,\lambda,C,\mu,\Delta$ (with $\lambda$ measurable, an assumption the paper uses tacitly). Primitives holds the Poisson processes (the published BesbesZeevi.Parametric.PoissonProcess, independent as a family), the uniform $U_j$, the initial conditions, and the independence of the three families. Any probability space carrying them is allowed; completion is immaterial for almost-sure statements.
• Initial conditions are random and satisfy, almost surely, $q_n(0)\in Q$, $nq_n(0,i)\in\mathbb N$, $\ell_n(0)\in\Delta\mathbb N$, $q_n(0,B+1)=0$, $\ell_n(0)\le B$, and $q_n(0)\to q(0)$ coordinatewise (the form of (2) for exponential service).
• The processes are given in System with the hypothesis that, almost surely, for every $n\ge1$, $(q_n,\ell_n)$ is a càdlàg, $Q$-valued solution of (9a)–(9b) on $[0,T]$. Left limits are Function.leftLim, and $\tau_{n,k}=\inf\{t\ge0:\mathcal N^\lambda_n(t)\ge k\}$. The well-posedness milestone states that such solutions exist and are unique almost surely, so System is not vacuous.
• $\Omega_T$ is the predicate IsNicePath B_T ω. It holds the equations at $\omega$, simple events (unit jumps, no coincidences) and the initial conditions at $\omega$, Proposition 4's property, (11) and (12a)–(12c). Proposition 7 asserts it almost surely; "for each $\omega\in\Omega_T$" becomes "for every $B_T,\omega$ with IsNicePath B_T ω".
• Conventions. Time is real, with conditions on $[0,T]$. $\lim_n\sup_t(\cdot)=0$ is written in $\varepsilon$–$n$ form. Relative compactness in $(D_{\mathbb R^{\mathbb N}}[0,T],\varrho)$ is coordinatewise uniform convergence along sub-subsequences. Subsequences are StrictMono maps. Tail sums in inequalities ((6c), Corollary 11) are in $[0,\infty]$; $u_n$ and $v_n$ in limit statements are real series, finite sums for large $n$ on $\Omega_T$. $\liminf_n n^{\gamma_0}(1-\alpha_n)>0$ is "eventually $\ge\kappa$ for some $\kappa>0$". The constant in (6c) is fixed to $u(a+\sigma)$.
• Ruled out. A real tsum in (6c) would make the bound vacuous for non-summable tails, and a real supremum would make (6a) vacuous for unbounded thresholds. Neither appears. (6a) says that $\ell_n$ equals $m\Delta$ on $[a+\sigma,b]$ for all large $n$, a property of the learned threshold that no fixed threshold could satisfy for all admissible loads.
• One added hypothesis. Proposition 9 assumes $u(t_0)>0$: for an empty system at $t_0$ the paper's strict inequality reads $0<0$.
• Welcome contributions: the Poisson functional strong law with rate (Lemma 6), Bramson's approximation lemma (Lemma 21), and the construction's well-posedness. All three are reusable for other many-server models.

Selected references

• D. Goldsztajn, S. C. Borst, J. S. H. van Leeuwaarden, Learning and balancing unknown loads in large-scale systems, arXiv:2012.10142v3, 2024 (Mathematics of Operations Research, 2025). https://arxiv.org/abs/2012.10142
• D. Goldsztajn, S. C. Borst, J. S. H. van Leeuwaarden, D. Mukherjee, P. A. Whiting, Self-learning threshold-based load balancing, INFORMS Journal on Computing 34(1), 39–54, 2022.
• M. Bramson, State space collapse with application to heavy traffic limits for multiclass queueing networks, Queueing Systems 30, 89–140, 1998. https://doi.org/10.1023/A:1019160803783
• P. D. Sparaggis, D. Towsley, C. Cassandras, Extremal properties of the shortest/longest non-full queue policies in finite-capacity systems with state-dependent service rates, Journal of Applied Probability 30, 223–236, 1993.

Motivation

Large data centers and cloud platforms route a stream of incoming tasks to many server pools, each pool able to serve several tasks at once. A dispatcher that sends each task to the least loaded pool (join-the-shortest-queue, JSQ) balances the load best, but it needs the exact number of tasks at every pool, which is costly to maintain at scale. A threshold dispatching rule needs much less information: it only needs to know which pools hold fewer than $\ell_n$ tasks, or fewer than $\ell_n+\Delta$ tasks. For constant arrival rates and exponential service it has the same fluid and diffusion limits as JSQ when $\Delta = 1$ and the threshold equals $\lfloor\rho\rfloor$, where $\rho$ is the offered load per pool (Goldsztajn, Borst, van Leeuwaarden, Mukherjee and Whiting, INFORMS Journal on Computing 34(1), 2022, reference [15] of arXiv:2012.10142v3).

The difficulty is that the right threshold depends on $\rho$, which the dispatcher does not know. Goldsztajn, Borst and van Leeuwaarden (arXiv:2012.10142v3) let the dispatcher learn it online. This mission concerns their second main result: with Coxian service times, which are dense among all service-time distributions, and the basic learning scheme, the threshold settles at the optimal value and the load becomes nearly balanced, almost surely in the many-server limit. (The first main result, for exponential service with a time-varying arrival rate and a refined learning scheme, is the subject of a companion mission.)

Setting

There are $n$ server pools. Tasks arrive as a Poisson process of rate $n\lambda$, $\lambda \ge 0$. A task passes through at most $r \ge 1$ phases: it starts in phase $1$, phase $m$ lasts an exponential time of rate $\mu_m > 0$, and after phase $m$ the task moves to phase $m+1$ with probability $p_m$ or leaves with probability $1-p_m$, with $p_r = 0$ and $p_m\in(0,1)$ for $m\ne r$. The mean service time $1/\mu$ follows from these data, and $\rho := \lambda/\mu$.

A pool has profile $\nu\in\mathbb N^r$ if it holds $\nu(m)$ tasks in phase $m$. The occupancy state $s_n(\nu)$ is the fraction of pools with profile $\nu$, a point of $S = \{s\in[0,1]^{\mathbb N^r} : \sum_\nu s(\nu) = 1\}$, and $q_n(i) = \sum_{\nu(1)+\dots+\nu(r)\ge i} s_n(\nu)$ is the fraction of pools with at least $i$ tasks.

Dispatching. With threshold $\ell_n$ and $h_n = \ell_n+\Delta$ for an integer $\Delta\ge1$, an arriving task goes to a uniformly random pool with fewer than $\ell_n$ tasks if there is one; otherwise to a uniformly random pool with fewer than $h_n$ tasks if there is one; otherwise to a uniformly random pool.

Basic learning. $\ell_n(t) = \lfloor u_n(t)\rfloor_\Delta$, where $u_n = \sum_{i\ge1}q_n(i)$ is the number of tasks divided by $n$ and $\lfloor x\rfloor_\Delta = \max\{k\Delta : k\Delta\le x,\ k\in\mathbb Z\}$.

All systems, for every $n$, are built on one probability space from independent unit-rate Poisson processes $\mathcal N_{(\nu,i,j)}$, i.i.d. uniform selection variables $U_j$ and random initial states $s_n(0)$, through the equations (21a)–(21b) of §6.1.1. Initial states converge, $s_n(0)\to s(0)$, and $q_n(0,B+1)=0$ for a fixed $B$.

Formalization targets

Goal: Theorem 3

If $\rho\notin\{i\Delta : i\in\mathbb N\}$, there are constants $\sigma,\eta,c>0$, independent of the horizon $T$, such that almost surely

$$\lim_{n\to\infty}\sup_{t\in[\sigma,T]}|\ell_n(t)-\lfloor\rho\rfloor_\Delta| = 0,\qquad \lim_{n\to\infty}\sup_{t\in[\sigma,T]}|1-q_n(t,i)| = 0\ \ (i\le\lfloor\rho\rfloor_\Delta),$$ $$\limsup_{n\to\infty}\sup_{t\in[\sigma,T]}\sum_{i>\lfloor\rho\rfloor_\Delta+\Delta} q_n(t,i)\,e^{\eta(t-\sigma)}\le c .$$

The constants are left unspecified, as in the paper; what is fixed is the shape: the threshold equals $\lfloor\rho\rfloor_\Delta$ after time $\sigma$, the first $\lfloor\rho\rfloor_\Delta$ columns are asymptotically full, and the excess mass decays exponentially.

Milestones

In the order the proof uses them: well-posedness of the coupled construction (§6.1.1); relative compactness of the occupancy and counting processes (Proposition 14); a uniform bound on occupancy and threshold over $[0,T]$ (Lemma 15); the set $\Omega_T$ of nice sample paths (Proposition 16); the almost-sure law of large numbers $u_n\to u$ for the total mass, with $u$ the infinite-server fluid function built from the residual-service survival functions $G_m$ (Proposition 17); and differential inequalities for the limits of the mass processes $x, y, z$ while the threshold is $\lfloor\rho\rfloor_\Delta$ (Proposition 18).

Significance

Theorem 3 says that a dispatcher that knows nothing about the load except the current number of tasks reaches the threshold JSQ-like balancing needs, and then balances the load: with $\Delta=1$, the fraction of pools with fewer than $\lfloor\rho\rfloor$ tasks vanishes and the fraction with more than $\lceil\rho\rceil$ tasks is $O(e^{-\eta(t-\sigma)})$, where $\eta=\min_m(1-p_m)\mu_m$ is a lower bound on the service hazard rate. Because Coxian laws are dense among service-time distributions, the result is evidence that threshold-based learning works beyond exponential service. Proposition 17 is also a statement of independent interest: the fluid law of large numbers for an infinite-server system with Coxian service, known to hold weakly, holds almost surely under this coupling.

The results are proved in the paper (arXiv:2012.10142v3, 2024). No part of them is formalized. The mission produces a machine-checked model of the coupled many-server construction with phase-type service, which no Lean library has, and a complete formal proof of the paper's almost-sure fluid-limit argument.

Difficulty

The statements are almost sure and pathwise, about one coupled sequence of jump processes with a countable state space $\mathbb N^r$, so weak-convergence arguments do not suffice. The natural first idea, to read off Theorem 3 from Proposition 17 alone, settles only (8a): $u_n\to u$ and $u(t)\to\rho$ force $\ell_n=\lfloor\rho\rfloor_\Delta$ eventually, but they say nothing about how the mass is distributed across the pools. Statements (8b) and (8c) require tracking the column masses $x_n, y_n, z_n$ through subsequential fluid limits that are only known to be Lipschitz, with dispatching decisions that depend discontinuously on the state. The phases complicate this: a pool's departure rate depends on the phases of its tasks, which the column picture ignores, and only the lower bound $\eta$ on the hazard rate controls the decay. The hypothesis $\rho\notin\Delta\mathbb N$ cannot be dropped: when $\rho$ is a multiple of $\Delta$, the threshold can oscillate between $\rho-\Delta$ and $\rho$.

Formalization scope

• Phases and profiles. Phases are Fin r; profiles are Fin r → ℕ; a fixed enumeration $\nu_i$ of $\mathbb N^r$ is a parameter. $q(i)$ is computed as $1-\sum_{\Sigma(\nu)<i}s(\nu)$, equal to (1) on $S$.
• Residual service. $G_m(t) = (e^{tQ}\mathbf 1)_m$ with the Coxian sub-generator $Q$ ($Q_{mm}=-\mu_m$, $Q_{m,m+1}=p_m\mu_m$).
• The construction is a structure: primitives (the published BesbesZeevi.Parametric.PoissonProcess for every driving process, their mutual independence, i.i.d. uniforms, independent initial conditions with $n\,s_n(0,\nu)\in\mathbb N$), plus processes that almost surely solve (21a)–(21b) for every $n\ge1$ and all $t\ge0$, are càdlàg, $S$-valued and have finitely many tasks. Left limits are Function.leftLim; $\nu-e_1$ and $\nu+e_m-e_{m+1}$ are guarded, never truncated. The dispatching indicators $r_{ij}$ are defined for all $i\ge0$, and the endpoints of $J_i(s,j)$ are corrected so that the intervals partition $[0,1)$ as the text states.
• $\Omega_T$ is a predicate collecting exactly the properties of Propositions 14 and 16; relative compactness with respect to $\varrho$ is rendered as subsequential coordinatewise uniform convergence on $[0,T]$.
• Theorem 3 quantifies $\exists\,\sigma,\eta,c>0$ before $\forall T$; with $T$ fixed first, (8c) would hold trivially with $c$ depending on $T$, because the occupancy vanishes beyond a column $B_T$. The tail sum in (8c) is taken in $[0,\infty]$, so it cannot be satisfied through a non-summable family, and $\eta$ must be positive.
• Needed infrastructure: functional strong laws for Poisson processes, Arzelà–Ascoli-type compactness in the uniform topology on càdlàg paths, a pathwise forward-induction construction of jump processes, and matrix-exponential facts for phase-type laws. The last three are reusable well beyond this mission. Contributions to any milestone, or to these supporting lemmas, are welcome.

Selected references

• D. Goldsztajn, S. C. Borst, J. S. H. van Leeuwaarden, Learning and balancing unknown loads in large-scale systems, arXiv:2012.10142v3, 2024. https://arxiv.org/abs/2012.10142v3
• D. Goldsztajn, S. C. Borst, J. S. H. van Leeuwaarden, D. Mukherjee, P. A. Whiting, Self-learning threshold-based load balancing, INFORMS Journal on Computing 34(1), pp. 39–54, 2022 (reference [15] of the paper above).
• M. Bramson, State space collapse with application to heavy traffic limits for multiclass queueing networks, Queueing Systems 30, 1998 (the compactness technique of Appendix A). https://doi.org/10.1023/A:1019108120366