eight_ticks_from_dimension
plain-language theorem explainer
The declaration shows that the rhythm cycle length equals eight ticks, or two raised to the third power. Researchers mapping the Recognition Science forcing chain into musical structures would cite this equality. The proof is a one-line simplification that unfolds the explicit definition of the cycle length.
Claim. The number of ticks per cycle equals $2^3$.
background
The MusicTheory.Rhythm module defines the ticks per cycle as the natural number eight. This sits inside the Recognition Science framework where the eight-tick octave appears as T7 in the forcing chain from T0 to T8, yielding a period of $2^3$ that matches the self-similar fixed point at T6. The upstream definition supplies the concrete value used by the simplification rule.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of ticks per cycle. This directly substitutes the constant eight and confirms equality to two raised to the third power.
why it matters
This result anchors the music theory constructions to the eight-tick octave (T7) required by the forcing chain. It ensures rhythm models inherit the period $2^3$ that precedes the derivation of three spatial dimensions at T8. Related tempo and subdivision definitions in the same module rest on this equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.