The Mean-Field Limit of Online Rademacher Vector Balancing

Let X₁, …, Xₙ be independent uniform vectors in {−1, 1}ⁿ. At time k, a sign is chosen after observing X₁, …, Xₖ. We identify the limit of the minimum expected terminal maximum norm of n^(−1/2) ∑ₖ₌₁ⁿ εₖXₖ with the mean-field control value introduced by Fiedler, Jackson, Lacker, and Niles-Weed for Gaussian inputs. Their universal lower bound reduces the question to the matching upper bound. We construct signs with approximately prescribed drift, compare frozen blocks through their transition operators, and control the empirical energy of the actual Rademacher process. An exact variance identity for separable functions handles the dependence created by a shared sign. A regularized Föllmer control yields a terminal estimate uniform over initial states satisfying a sixth-moment clipping budget. A density argument preserves a deterministic initial condition and a strict instantaneous energy margin, allowing the comparison to reach bounded measurable controls. We also provide Lean 4 proofs of the finite variance identity and selected finite-model statements; the full limit theorem is not formally verified. Version 1: 14-page preprint with LaTeX source and a frozen six-module partial Lean 4 supplement. Extensive AI assistance is disclosed in the manuscript. The full main limit theorem has not been formally verified.