beats_eq_360
plain-language theorem explainer
The lemma establishes that the minimal joint duration for 8-beat and 45-fold patterns equals 360. Researchers deriving synchronization conditions or divisibility constraints in periodic structures within Recognition Science would cite this result. The proof is a one-line simplification that unfolds the definition of beats and substitutes the pre-established lcm equality.
Claim. Let beats denote the least common multiple of 8 and 45. Then beats = 360.
background
The Gap45 module works under the assumption that 9 and 5 are coprime. This underpins calculations involving multiples of 8 and 45. The identifier beats is defined directly as Nat.lcm 8 45 and stands for the smallest positive integer that is a common multiple of both the 8-beat cycle and the 45-fold pattern.
proof idea
The proof is a one-line wrapper. It invokes the simp tactic on the definition of beats together with the upstream lemma lcm_8_45_eq_360, which itself rests on the identity lcm(a,b) = a*b/gcd(a,b) with gcd(8,45)=1.
why it matters
This lemma supplies the concrete value 360 that appears in the parent result minimal_sync_360_divides, which states that any common multiple of 8 and 45 must be a multiple of 360. It thereby closes the computation of the base period for the Gap45 synchronization analysis and connects to the eight-tick octave (T7) in the forcing chain. The equality is used verbatim in both the main Gap45 and the Beat submodule.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.