Local decisions, diffusive influence, and lower bounds for graphical balanced allocation
Obinna Okechukwu
math.PR
Sep 30, 2026 · v2
cs.DS
TL;DR
All numbered results on lower bounds for graphical balanced allocation are formally verified in Lean.
Abstract
In graphical two-choice allocation, each arriving ball is assigned to one endpoint of a random edge. We study rules whose decision is a monotone function of the two endpoint loads, allowing edge-dependent thresholds and fresh randomization. Such a rule has an exact unit-discrepancy coupling: adding one ball to the initial state produces one tagged discrepancy at every later time. We represent the tag by conditional-expectation projections on the marked edge space and obtain diffusive displacement bounds. A transport-volume inequality then converts slow propagation of influence into lower bounds for the load gap. On the cycle with $n$ vertices, from every initial distribution and at every physical time $t\ge 1/n$, the expected gap is at least a constant times $\min\{\sqrt n,t^{1/4}\}$, and the gap exceeds this scale with probability at least $1/8$. After exactly $k\ge1$ allocations, the corresponding scale is $\min\{\sqrt n,(k/n)^{1/4}\}$. No stationarity, symmetry, recurrence, or moment assumption is used. A smoothed threshold rule in the same class has expected gap $O(\sqrt n\log n)$ up to any fixed polynomial time horizon, so the saturated cycle bound is sharp within the class up to a logarithmic factor. The general inequality also yields a lower bound of order $\sqrt{L/K}$ on the $L\times K$ rectangular torus $C_L\square C_K$; combined with a strategy-independent logarithmic bound, this gives order $\sqrt{L/K}+\log(LK)$. These results separate endpoint-local rules from global-information strategies that achieve polylogarithmic gaps on cycles. All numbered results are verified in Lean.
Problem
In graphical two-choice allocation, each ball is placed at one endpoint of a random edge. The question is how large the load gap must be for rules that decide using only a monotone function of the two endpoint loads.
Approach
Endpoint-local monotone rules admit an exact unit-discrepancy coupling, in which one extra ball produces a single tagged discrepancy at all later times. The tag is represented by conditional-expectation projections on a marked edge space, and a bound on products of projections gives diffusive displacement estimates. A transport-volume inequality then converts this slow propagation of influence into gap lower bounds. All numbered results are verified in Lean.
Results
On the n-cycle the expected gap is at least c·min{√n, t^{1/4}} from any initial state, and the gap exceeds this scale with probability at least 1/8. A smoothed threshold rule in the same class achieves O(√n log n), so the bound is sharp up to a logarithmic factor. On the L×K torus the lower bound is of order √(L/K)+log(LK), which separates endpoint-local rules from global-information strategies.