Real-period pinwheel scheduling at density 5/6

We prove the 5/6 density conjecture for pinwheel scheduling with real periods. For every finite family of labelled tasks with periods a_i ≥ 1 and ∑_i 1/a_i ≤ 5/6, there is a bilateral schedule in which task i occurs at least ℓ times in every ⌈ℓ a_i⌉ consecutive slots, for each positive integer ℓ. A reduction merges arbitrarily large systems down to eight roles; shorter systems are handled separately. The eight-role theorem combines explicit schedules with finite certificates whose rational inequalities cover the remaining real parameter regions, including irrational rates and boundary cases. This record contains the manuscript PDF and a complete supplementary package with editable LaTeX source, finite proof certificates, verification programs, reproduction instructions, and pinned Lean sources for selected formalized subresults. The manuscript, documentation and proof data are licensed under CC BY 4.0; the verification software, typesetting helper and local Lean sources are licensed under MIT.