Cacophonies of Metronomes: Multi-sequence Generalizations of Beatty's Theorem

Two multi-sequence generalizations of Beatty's theorem, both derived from a single geometric observation (the Height Lemma) about monotone paths crossing the faces of a cubical tiling of the positive orthant. The first partitions the positive integers into n sieved Beatty sequences; the second keeps the Beatty sequences and gives up exactness, with sharp one-sided bounds. Also included: an n-gap generalization of the classical two-gap property, an arbitrary-clock master theorem containing the two-function theory of Lambek–Moser and Holshouser–Reiter, and Irwin–Hall limit laws for the displacement. The repository accompanies the paper with a Lean 4 development verifying the load-bearing results (sorry-free, with classical inputs recorded as named hypotheses rather than axioms) and an exact-integer-arithmetic script verifying every numerical claim in the paper.