cycles_of_8
plain-language theorem explainer
The lemma shows that the minimal joint duration for 8-beat and 45-fold patterns contains exactly 45 cycles of the 8-beat pattern. Researchers constructing synchronization objects in the Gap45 model cite it when building the canonical Sync record. The proof is a one-line simplification that unfolds the beats definition and applies the companion division lemma.
Claim. Let $b = {lcm}(8,45)$. Then $b/8 = 45$.
background
beats is defined as the least common multiple of 8 and 45, the minimal joint duration for an 8-beat pattern and a 45-fold pattern. The Gap45 module works under the assumption that 9 and 5 are coprime, which guarantees the lcm properties used here. The upstream lemma lcm_8_45_div_8 states that lcm(8,45)/8 equals 45 and derives it from the equality lcm(8,45) = 360.
proof idea
The proof is a one-line wrapper that invokes the simp tactic on the definition of beats together with the lemma lcm_8_45_div_8.
why it matters
This lemma supplies the cycles8 field for the canonical Sync record in Gap45.Beat, which packages beats, cycles_of_8 and cycles_of_45 into a single synchronization object. It supports the eight-tick octave structure by confirming the exact cycle count inside the lcm period. The result closes a small computational step required for later synchronization arguments in the Gap45 layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.