lcm_8_45_div_8
plain-language theorem explainer
The lemma establishes that lcm(8,45) divided by 8 equals 45. Researchers on beat synchronization in the Gap45 framework cite it when counting 8-beat cycles inside the minimal joint period. The proof is a one-line wrapper that applies the equality lcm(8,45)=360 and simplifies the division.
Claim. $ (8,45) / 8 = 45 $
background
The Gap45 module encodes the gating rule that experience is required exactly when the plan period is not a multiple of 8, capturing the policy that 8-beat alignment disables Gap45 gating. This lemma supplies the cycle count needed for synchronization arithmetic between 8-beat and 45-fold periods. It depends on the upstream result lcm(8,45)=360, which follows from gcd(8,45)=1 together with the identity lcm(a,b)=a*b/gcd(a,b).
proof idea
The proof invokes the lemma lcm_8_45_eq_360 to substitute lcm(8,45)=360, then applies simpa to reduce the division 360/8 directly to 45.
why it matters
This lemma feeds the theorem sync_counts that fixes the minimal joint duration at 360 beats with exactly 45 cycles of 8 and 8 cycles of 45. It supports the eight-tick octave structure by quantifying alignment between the 8-beat and 45-fold symmetries. The parent result sync_counts quotes it verbatim to close the synchronization requirement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.