A Computer-Assisted Proof of the Optimal Density Bound for Pinwheel Covering

In the covering version of the pinwheel scheduling problem, a daily task must be assigned to agents under the constraint that agent $i$ can perform the task at most once in any $a_i$-day interval. In this paper, we determine the optimal constant $\alpha^* = 1.264\ldots {}$ such that every instance with $\sum_{i} \frac{1}{a_i} \ge \alpha^*$ is schedulable. This resolves an open problem posed by Soejima and Kawamura (2020). Our proof combines Kawamura's (2024) techniques for the packing version with new mathematical insights, along with an exhaustive computer-aided search that draws on some ideas from G\k{a}sieniec, Smith, and Wild (2022).