beats
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove that beats equals 360.
- Does not interpret the physical meaning of the 8-beat or 45-fold patterns.
- Does not extend the definition beyond natural numbers.
- Does not address non-minimal common multiples.
formal statement (Lean)
28@[simp] def beats : Nat := Nat.lcm 8 45
proof body
Definition body.
29