cycles_of_45
plain-language theorem explainer
The lemma establishes that the minimal joint period beats, defined as lcm(8,45), contains exactly eight 45-fold cycles. Modelers of periodic synchronization in the Gap45 framework cite this when counting cycles inside the least common multiple duration of 360 beats. The proof is a one-line simp wrapper that unfolds the beats definition and applies the pre-established lcm division equality.
Claim. Let $b = {lcm}(8,45)$. Then $b/45 = 8$.
background
In the Gap45.Beat module the quantity beats is defined as Nat.lcm 8 45 and represents the minimal joint duration for 8-beat and 45-fold patterns. The surrounding Gap45 setting encodes the gating rule that experience is required precisely when a plan period is not a multiple of 8, capturing the policy that 8-beat alignment disables Gap45 gating. The lemma depends on the auxiliary result lcm_8_45_div_45, which proves Nat.lcm 8 45 / 45 = 8, and on the beats definition itself.
proof idea
The proof is a one-line wrapper that invokes the simp tactic with the beats definition and the lcm_8_45_div_45 lemma. This reduces the goal directly to the known numerical equality 360/45 = 8.
why it matters
The result supplies the cycles45 component of the canonical Sync record inside the Beat namespace. It thereby supports minimality arguments for simultaneous multiples of 8 and 45, feeding the parent cycles_of_45 statement in the Gap45 module. The construction aligns with the eight-tick octave structure (T7) of the Recognition Science forcing chain by fixing the cycle count inside the 360-beat joint period.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.