ticksPerCycle
plain-language theorem explainer
The definition sets the number of ticks per cycle to eight. Researchers deriving rhythmic frequencies from musical tempo cite this constant to connect subdivisions to the eight-tick octave. It supplies the base value for theorems that equate the cycle length to two to the power three and compute eighth-note rates. The declaration is a direct constant assignment carrying the simplification attribute.
Claim. Define the number of ticks per cycle to be $8$.
background
The MusicTheory.Rhythm module introduces a Tempo structure consisting of a positive real beats-per-minute value together with a derived beats-per-second function. This structure supports mapping rhythmic subdivisions to frequencies in hertz. A musical tempo (BPM) combined with a rhythmic subdivision determines a repetition frequency in Hz. This frequency can fall in the 5-35 Hz range.
proof idea
The declaration is a direct definition assigning the natural number eight, annotated with the simplification attribute for use in rewriting.
why it matters
This definition provides the cycle length required by eighth_notes_per_measure and eight_ticks_from_dimension. The latter theorem rewrites it to two to the power three, closing the link to the eight-tick octave in the forcing chain. It underpins tempo-to-frequency conversions that place repetition rates in the five to thirty-five hertz interval.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.