lcm_8_45_div_45
plain-language theorem explainer
The lemma states that lcm(8,45) divided by 45 equals 8, supplying the exact count of 45-fold cycles inside the minimal joint period of 360 beats. Researchers computing synchronization counts or cycle alignments in the Gap45 module cite this result when assembling beat-level clock relations. The proof is a one-line wrapper that invokes the upstream equality lcm(8,45)=360 and reduces the division by simpa.
Claim. $lcm(8,45)/45=8$
background
The Gap45 module encodes the gating rule that experience is required exactly when the plan period is not a multiple of 8. This captures the policy that 8-beat alignment disables Gap45 gating. The lemma operates inside the Beat namespace, which handles alignments between 8-beat and 45-fold periodicities. It depends directly on the upstream result lcm(8,45)=360, whose proof rests on gcd(8,45)=1 together with the identity gcd_mul_lcm.
proof idea
The proof is a one-line wrapper. It obtains the equality lcm(8,45)=360 from the sibling lemma lcm_8_45_eq_360 and applies simpa to reduce the arithmetic 360/45 to 8.
why it matters
The result is invoked by the theorem sync_counts, which packages the full synchronization statement lcm(8,45)=360 together with the two division lemmas, and by the simp lemma cycles_of_45. It contributes to the eight-tick octave structure by quantifying how many 45-fold cycles fit inside the joint period. No open questions are closed by this lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.