eighth_notes_per_measure
plain-language theorem explainer
The theorem fixes the cycle length in the rhythm model at exactly eight ticks, matching the eight-tick octave forced by the T7 step of the unified forcing chain. Physicists modeling entrainment between musical subdivisions and the 5-35 Hz DFT-8 spectral modes would cite this equality when linking BPM to resonant frequencies. The proof is a direct reflexivity step that records the equality as definitional.
Claim. In the rhythm model the cycle length satisfies $ticksPerCycle = 8$.
background
The MusicTheory.Rhythm module maps musical tempo (BPM) and subdivision to repetition frequencies in Hz. These frequencies are required to lie inside the 5-35 Hz band of the eight-mode DFT-8 spectrum that emerges from the Recognition Science forcing chain. The upstream result PhiForcingDerived.of supplies the J-cost structure whose fixed point yields the eight-tick period; IntegrationGap.A encodes the active-edge count per fundamental tick that balances at D = 3.
proof idea
The proof is a one-line reflexivity application. It records that ticksPerCycle is introduced as the constant 8 in the module definition, so the equality holds by construction.
why it matters
The declaration supplies the concrete period required by T7 (eight-tick octave) inside the MusicTheory layer. It thereby licenses the subsequent tempo_120, tempo_150 and tempo_75 definitions that convert BPM into frequencies resonant with the DFT-8 modes. No downstream theorems yet depend on it; the result closes the link between the phi-ladder octave and musical subdivision without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.