beats
plain-language theorem explainer
beats defines the minimal joint duration in beats for aligning an 8-beat pattern with a 45-fold pattern as their least common multiple. Researchers working on Gap45 synchronization and its applications in decision models or pedagogy cite this quantity as the base period for cycle counting. The definition is introduced directly as a one-line assignment to the standard lcm operation on natural numbers.
Claim. Let $b :=$ lcm$(8,45)$. Then $b$ is the smallest positive integer that is a multiple of both 8 and 45, serving as the minimal joint duration for the 8-beat and 45-fold patterns.
background
The Gap45 module encodes the gating rule that experience is required exactly when the plan period is not a multiple of 8; 8-beat alignment disables Gap45 gating per the Source.txt policy. The upstream result states that beats supplies the minimal joint duration (in beats) for 8-beat and 45-fold patterns. This quantity is obtained via the least common multiple, which equals 360 because 8 and 45 share no common factors greater than 1.
proof idea
This is a one-line definition that directly assigns the value of Nat.lcm applied to the constants 8 and 45.
why it matters
beats supplies the base period used by downstream results including beats_eq_360, cycles_of_8, cycles_of_45, and minimal_sync_divides to establish cycle counts and minimality. It anchors the Gap45 gating mechanism inside the eight-tick octave (T7) of the forcing chain. The same quantity appears in the Monty Hall probability theorem and in the proof that optimal spacing ratio exceeds 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.