tempo_75
plain-language theorem explainer
tempo_75 supplies the Tempo instance with 75 beats per minute for rhythmic calculations in Recognition Science. It is referenced in establishing that the sixteenth-note subdivision under this tempo yields a frequency of 2.5 Hz. The definition constructs the structure directly and uses norm_num to confirm the positive bpm requirement.
Claim. Let $Tempo$ be the structure whose field $bpm$ is a positive real number. Then $tempo_{75}$ is the element of $Tempo$ with $bpm=75$.
background
The Tempo structure in the MusicTheory.Rhythm module pairs a positive real bpm with a proof of its positivity. Derived operations include beatsPerSecond as bpm divided by 60, tickHz as beatsPerSecond times ticksPerCycle, and subdivisionFreq as beatsPerSecond times a natural-number subdivision level. The module develops rhythmic patterns connected to the eight-tick cycle.
proof idea
The definition applies the structure constructor to the numeral 75 and discharges the positivity obligation via the norm_num tactic.
why it matters
tempo_75 supplies the concrete input to the theorem tempo_75_sixteenth_note_is_mode1, which verifies that subdivision frequency at level 2 equals 2.5. It anchors the rhythmic subdivision hierarchy in the Recognition Science treatment of music theory and supplies a base case for mode-1 frequency computations tied to the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.