beats
plain-language theorem explainer
beats defines the minimal joint duration as the least common multiple of 8 and 45 for 8-beat and 45-fold patterns. Researchers modeling synchronization in decision theory or pedagogy cite it to derive cycle counts and fractions such as 3/64. The definition is a direct abbreviation via the Nat.lcm operation on fixed constants.
Claim. Let $b = {lcm}(8,45)$. This $b$ is the minimal joint duration in beats for an 8-beat cycle and a 45-fold pattern.
background
The Gap45 module begins from the coprimality of 9 and 5 to construct gcd and lcm relations for the number 45. The upstream Beat.beats supplies the identical lcm expression in a sub-namespace, establishing the base period before any cycle-counting lemmas. This arithmetic setting prepares the eight-tick structure for later mapping to time deltas and decision probabilities.
proof idea
The declaration is a direct abbreviation that invokes Nat.lcm on the constants 8 and 45. No lemmas or tactics appear in the body.
why it matters
This definition supplies the base period that feeds beats_eq_360, cycles_of_8, cycles_of_45, and delta_time_eq_3_div_64 inside Gap45, plus p_switch_eq in MontyHall and spacing_ratio_pos in pedagogy. It anchors the 45-gap arithmetic that connects the eight-tick octave to concrete cycle counts and the 2/3 switch probability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.