minimal_sync_360_divides
plain-language theorem explainer
Any natural number t divisible by both 8 and 45 must be divisible by 360. Recognition Science modelers working on joint periodicities cite this to enforce the minimal synchronization interval between an 8-beat cycle and a 45-fold pattern. The proof is a one-line term wrapper that rewrites the joint period via beats_eq_360 and invokes the general lcm-divisibility result.
Claim. If $8 mid t$ and $45 mid t$ for $t in mathbb{N}$, then $360 mid t$.
background
The module establishes that 9 and 5 are coprime, which fixes the least common multiple of 8 and 45 at 360. The identifier beats denotes the minimal joint duration for an 8-beat cycle and a 45-fold pattern. Upstream lemma beats_eq_360 states that this minimal duration equals 360, while minimal_sync_divides asserts that any common multiple of 8 and 45 is a multiple of beats.
proof idea
This is a one-line term proof. It applies simpa with the simp lemma beats_eq_360 to rewrite the target divisibility condition, then directly invokes minimal_sync_divides on the supplied hypotheses h8 and h45.
why it matters
The lemma supplies the concrete 360-divisibility step required by no_smaller_multiple_8_45, which shows no positive integer smaller than 360 can satisfy both divisibility conditions simultaneously. It is invoked verbatim in resolution_requires_full_period to conclude that any window resolving both periodicities must be a multiple of 360. In the Recognition framework this anchors the eight-tick octave (period 2^3) together with the 45-fold structure arising from the coprime factors 9 and 5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.