minimal_sync_divides
plain-language theorem explainer
Any natural number t divisible by both 8 and 45 must be divisible by their least common multiple beats. Researchers modeling synchronized 8-beat and 45-fold periodicities in Recognition Science cite this to fix the shortest common cycle length. The argument is a direct one-line reduction via the standard lcm divisibility property after unfolding beats.
Claim. If $8 | t$ and $45 | t$ for a natural number $t$, then $lcm(8,45) | t$.
background
The Gap45 module treats the minimal joint duration for 8-beat and 45-fold patterns, with the module note that 9 and 5 are coprime. beats is defined as Nat.lcm 8 45, the shortest positive integer divisible by both 8 and 45. This sits inside the discrete tier structure supplied by upstream results on J-cost and spectral emergence.
proof idea
The proof is a one-line wrapper that applies Nat.lcm_dvd to the two divisibility hypotheses after the simpa tactic unfolds the definition of beats.
why it matters
The lemma feeds the parent result minimal_sync_360_divides, which rewrites the claim with 360 explicit on the left. It supplies the minimality step for the joint period in Gap45 and aligns with the eight-tick octave (period 2^3) from the unified forcing chain. No open scaffolding questions are resolved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.