lcm_8_45_div_8
plain-language theorem explainer
The lemma establishes that lcm(8,45) divided by 8 equals exactly 45. Researchers counting 8-beat cycles inside the minimal joint alignment period in the Gap45 synchronization analysis cite this identity. The proof reduces the claim to the prior result lcm(8,45)=360 followed by direct arithmetic verification.
Claim. $lcm(8,45)/8=45$
background
The Gap45 module studies integer relations between the periods 8 and 45 that arise in the eight-tick octave and 45-fold symmetry alignments. The module opens by recording that 9 and 5 are coprime, noting that 45 factors as their product. The immediate upstream result is the lemma lcm_8_45_eq_360, which states lcm(8,45)=360 and is proved from the identity lcm(a,b)=ab/gcd(a,b) together with the numerical check that 845=360.
proof idea
The tactic proof first obtains the equality lcm(8,45)=360 from the upstream lemma, then uses decide to confirm that 360/8=45, and finishes with simpa to substitute and close the goal.
why it matters
This identity supplies one conjunct of the sync_counts theorem, which asserts that the minimal joint duration aligning 8-beat and 45-fold symmetries is exactly 360 beats, corresponding to 45 cycles of the 8-beat period and 8 cycles of the 45-fold period. It is also invoked by the cycles_of_8 lemma. In the Recognition framework it concretizes the eight-tick octave (T7) by furnishing explicit cycle counts for the phi-ladder alignments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.