In pinwheel scheduling with real periods, an instance consists of $n$ tasks with real periods $1\leq a_1\leq a_2\leq\cdots\leq a_n$. The goal is to find a schedule that assigns a task to each day in $\mathbb{N}$ such that, for every task $i \in \{1,\dots,n\}$ and every positive integer $\ell$, task $i$ occurs at least $\ell$ times in every block of $\lceil\ell a_i\rceil$ consecutive days. Given an instance $(a_1,a_2,\ldots,a_n)$, its dimension is $n$, its density is $\sum_{i=1}^n 1/a_i$, and its potential is $\sum_{i=1}^{n-1} 1/a_i$.

For integer periods, a long-standing conjecture stated that every instance of density at most $5/6$ admits a periodic schedule. Kawamura proved this conjecture using a computer-assisted proof [STOC 2024, PNAS 2026]. We extend this result to real periods while retaining the density bound of $5/6$. Our computer-assisted proof builds on Kawamura's ideas while using fewer explicit schedules. For integer periods, Kawamura reduced the problem to checking finitely many cases. To handle real periods, we use a satisfiability modulo theories (SMT) solver for linear real arithmetic.

We show that the following two results in bounded dimension suffice: (i) every instance of dimension at most $8$ and density at most $5/6$ admits a schedule; (ii) every instance of dimension $9$ and potential at most $5/6$ admits a schedule. We certify both results with a set of 14397 explicit periodic schedules that includes a valid schedule for every instance in (i) or (ii). We reduce every instance of larger dimension and potential at most $5/6$ to an instance of dimension 9 and potential at most $5/6$. Our result confirms the real-period conjecture of Fujiwara, Miyagi, and Ouchi [DMTCS 2026] and provides a compact and computer-verifiable proof.