minimal_sync_360_divides
plain-language theorem explainer
Any common multiple of 8 and 45 is necessarily a multiple of 360. Analysts of periodic pattern resolution in the Gap45 framework cite this lemma to bound minimal windows. The proof is a one-line wrapper that rewrites via the beats_eq_360 equality into the general divisibility result for the joint duration.
Claim. Let $t$ be a natural number. If $8$ divides $t$ and $45$ divides $t$, then $360$ divides $t$.
background
The Gap45 module encodes a gating rule: 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 Beat submodule defines the minimal joint duration for 8-beat and 45-fold patterns as their least common multiple.
proof idea
This is a one-line wrapper. It applies simpa with the beats_eq_360 equality to instantiate the general minimal_sync_divides lemma at the target t.
why it matters
The lemma supplies the 360-explicit form of the minimality condition. It is used to derive no_smaller_multiple_8_45, which shows no positive n less than 360 is divisible by both 8 and 45. It also feeds resolution_requires_full_period, which requires any resolving window to be a multiple of 360. This aligns with the eight-tick octave by fixing the minimal alignment period.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.