cycles_of_8
plain-language theorem explainer
The lemma establishes that the minimal joint duration of 8-beat and 45-fold patterns contains exactly 45 repetitions of the 8-beat pattern. Researchers verifying synchronization rules in the Gap45 module of Recognition Science cite this when checking alignment conditions. The proof is a one-line simp wrapper that unfolds the beats definition as lcm(8,45) and applies the supporting division lemma.
Claim. Let $b = {lcm}(8,45)$ denote the minimal joint duration in beats. Then $b/8 = 45$.
background
In the Gap45.Beat module, beats is defined as Nat.lcm 8 45 and represents the minimal joint duration for aligning 8-beat and 45-fold patterns. The module_doc states the Gap45 gating rule: experience is required exactly when the plan period is not a multiple of 8, capturing the policy that 8-beat alignment disables Gap45 gating.
proof idea
The proof is a one-line wrapper that applies simp with the beats definition and the upstream lemma lcm_8_45_div_8.
why it matters
This lemma supplies the cycles8 field for the canonical Sync structure in the same module. It confirms the 8-beat cycle count inside the joint period, supporting the eight-tick octave structure from the Recognition Science forcing chain. The result is mirrored in the parent Gap45 module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.