Tempo
plain-language theorem explainer
Tempo equips a positive real beats-per-minute value with derived tick and subdivision frequencies scaled by the fixed eight-tick cycle. Researchers mapping musical performance to DFT-8 modes cite the structure when converting BPM into rates that land on the phi-ladder lattice. The definitions arise by direct multiplication and division against ticksPerCycle, with positivity and equality proved by unfolding plus mul_pos and ring.
Claim. A Tempo is a pair consisting of a positive real number $b$ (beats per minute) and a proof that $b > 0$. Beats per second are defined as $b/60$. Tick frequency equals beats per second multiplied by 8. Subdivision frequency at level $n$ equals beats per second times $n$.
background
ticksPerCycle is the constant 8 inside the same Rhythm module. This length realizes the eight-tick octave (period $2^3$) required by the forcing chain at T7. The from theorem in PrimitiveDistinction reduces seven independent axioms to four structural conditions plus three definitional facts. The that structure in PhiLadderLattice supplies a hypothesis interface for phi-ladder Poisson summation on rapidly decreasing functions.
proof idea
beatsPerSecond and tickHz are one-line wrappers that scale bpm by 1/60 and then by ticksPerCycle. tickHz_pos unfolds the definitions, invokes norm_num to obtain 0 < 60 and 0 < 8, then applies mul_pos and div_pos. tickHz_eq unfolds and reduces the expression by ring.
why it matters
The structure supplies the basic tempo object that converts performance BPM into frequencies on the eight-tick lattice. It therefore realizes T7 inside the music-theory layer and prepares the concrete examples (tempo_120, tempo_150) that land on DFT-8 modes. Within the broader framework it supplies the rhythmic interface to D = 3 and the phi-ladder mass formula once the Poisson-summation hypothesis is discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.