gcd_8_45_eq_one
plain-language theorem explainer
The lemma proves that 8 and 45 share no common divisors. Researchers deriving combined periods in the Gap45 synchronization module cite this fact to obtain the lcm value 360. The proof is a direct computation via the decide tactic on natural-number arithmetic.
Claim. $ gcd(8,45)=1 $
background
The Gap45.Beat module encodes the rule that experience is required exactly when the plan period is not a multiple of 8. This implements the policy that 8-beat alignment disables Gap45 gating. The lemma supplies the coprimeness fact required before lcm calculations can proceed to 360.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the gcd directly from the definition of Nat.gcd.
why it matters
The result feeds the lcm_8_45_eq_360 and beats_eq_360 lemmas inside the same module. It supports the eight-tick octave structure by confirming that the 8-beat and 45-beat periods combine only at their product. The declaration therefore closes a prerequisite step for the Gap45 gating rule.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.