ticksPerCycle
ticksPerCycle sets the cycle length to eight ticks inside the rhythm module. Researchers connecting musical subdivisions to the eight-tick octave cite it when converting tempo into frequency. The definition is a direct constant assignment with no computation or lemmas required.
claimThe number of ticks per cycle equals 8.
background
The MusicTheory.Rhythm module models discrete rhythms to interface with the Recognition Science forcing chain. T7 supplies the eight-tick octave whose period is 2 cubed. The Tempo structure records beats per minute with a positivity constraint and defines beatsPerSecond as bpm divided by 60. Downstream theorems use the cycle length to map subdivisions onto frequencies in the 5-35 Hz interval.
proof idea
Direct constant definition that assigns the value 8. Downstream results apply simp to obtain equality with 2^3 or use rfl for immediate equality.
why it matters in Recognition Science
The definition anchors eight_ticks_from_dimension, which rewrites the cycle length as 2^3 and thereby instantiates the eight-tick octave (T7) from the UnifiedForcingChain. It also supports eighth_notes_per_measure and the tempo-to-frequency maps that place rhythms inside the 5-35 Hz band. The construction closes the link between musical subdivision and the D=3 spatial dimensions via the octave period.
scope and limits
- Does not derive the value 8 from J-uniqueness or the Recognition Composition Law.
- Does not assign physical units or interpretation to a tick.
- Does not generalize to variable cycle lengths or other octave periods.
Lean usage
theorem eight_ticks_from_dimension : ticksPerCycle = 2 ^ 3 := by simp [ticksPerCycle]formal statement (Lean)
20@[simp] def ticksPerCycle : ℕ := 8
proof body
Definition body.
21