beats_eq_360
plain-language theorem explainer
The lemma establishes that the minimal joint duration for 8-beat and 45-fold patterns equals 360 beats. Researchers modeling Gap45 gating rules in Recognition Science cite it to fix the least common multiple alignment for synchronization checks. The proof is a one-line wrapper that applies simp to the beats definition and the pre-established lcm equality.
Claim. Let $b$ be the minimal joint duration in beats for the 8-beat and 45-fold patterns. Then $b = 360$.
background
In the Gap45 module the quantity beats is defined as the least common multiple of 8 and 45; this is the shortest positive integer that is a multiple of both pattern periods. The module doc states that experience is required exactly when the plan period is not a multiple of 8, capturing the policy that 8-beat alignment disables Gap45 gating. The upstream lemma lcm_8_45_eq_360 proves Nat.lcm 8 45 = 360 by showing the gcd is 1, invoking the identity lcm = product / gcd, and verifying 8 * 45 = 360 by direct computation.
proof idea
This is a one-line wrapper that applies simp [beats, lcm_8_45_eq_360]. The tactic unfolds the definition of beats to Nat.lcm 8 45 and substitutes the equality already proved for that lcm value.
why it matters
The result feeds the lemma minimal_sync_360_divides, which states that any t divisible by both 8 and 45 is divisible by 360. It supplies the concrete numerical value for the joint period inside the Gap45 framework and connects to the eight-tick octave (period 2^3) in the forcing chain. No open questions are touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.