minimal_sync_divides
plain-language theorem explainer
If a natural number t is divisible by both 8 and 45 then it is divisible by their least common multiple. Researchers tracking periodic alignments in the Gap45 framework cite this to confirm the minimal joint period before invoking the 360-beat form. The proof is a one-line wrapper that unfolds beats and applies the standard lcm divisibility property.
Claim. Let $t$ be a natural number. If $8$ divides $t$ and $45$ divides $t$, then the least common multiple of $8$ and $45$ divides $t$.
background
In the Gap45.Beat submodule, beats is defined as the least common multiple of 8 and 45; it supplies the minimal joint duration for 8-beat and 45-fold patterns. The module document states 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. The upstream beats definition in Gap45 is identical and supplies the target for the present lemma.
proof idea
The proof is a one-line wrapper. It invokes Nat.lcm_dvd on the two divisibility hypotheses and then simplifies with the definition of beats.
why it matters
This lemma supplies the core minimality fact that feeds minimal_sync_360_divides, which rewrites the conclusion with the explicit value 360. It thereby supports the Gap45 gating rule by confirming that any common multiple of 8 and 45 satisfies the alignment condition that disables experience gating. The result sits inside the eight-tick octave structure of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.