lcm_8_45_eq_360
plain-language theorem explainer
The equality lcm(8,45)=360 supplies the minimal period aligning an 8-cycle with a 45-cycle. Pattern-synchronization arguments in the Gap45 development cite it to obtain the joint beat count. The short tactic proof first confirms coprimality by decision, invokes the standard gcd-lcm product identity, reduces the product via one_mul, and concludes by arithmetic evaluation.
Claim. $lcm(8,45)=360$
background
In the Gap45 module the arithmetic of periodicities 8 and 45 is developed to characterize synchronization requirements. The key identity used is the relation gcd(a,b) * lcm(a,b) = a * b supplied by the GCDLCM library. The module setting begins from the coprimality of 9 and 5, which indirectly informs the factorization of 45=9*5.
proof idea
The proof is a short tactic sequence. It first obtains Nat.gcd 8 45 = 1 by decide. It then applies the theorem gcd_mul_lcm to obtain the product identity. A simpa step using the coprimality and one_mul reduces the lcm to the product 8*45. A final decide confirms the product equals 360, and transitivity closes the goal.
why it matters
This lemma is the central arithmetic fact feeding the synchronization theorem sync_counts and the beat count beats_eq_360. It supplies the exact joint period 360 that appears in the 45-gap analysis, consistent with the eight-tick structure (period 2^3) of the Recognition framework. Downstream results such as lcm_8_45_div_8 and lcm_8_45_div_45 derive the cycle counts 45 and 8 directly from it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.