swingRatio_moderate
plain-language theorem explainer
swingRatio_moderate supplies the constant real number 3/2 as the moderate swing ratio. Researchers extending the eight-tick octave into musical rhythm cite it when linking swing to the fifth interval. The definition is a direct constant assignment with no lemmas or computation.
Claim. The moderate swing ratio is the real number $3/2$.
background
The MusicTheory.Rhythm module builds rhythmic structures on the eight-tick octave that follows from D=3 in the forcing chain T0-T8. Sibling definitions such as ticksPerCycle, subdivisionLevels, and the various tempo_ lemmas organize measures into eighth notes, triplets, and subdivisions at fixed frequencies. This constant sets the moderate swing value, consistent with the phi self-similar fixed point and the Recognition Composition Law.
proof idea
The declaration is a direct definition that assigns the value 3/2. No lemmas or tactics are applied; it functions as a primitive constant for downstream use.
why it matters
This definition is referenced by the theorem swing_moderate_is_fifth, which confirms the value by reflexivity. It supplies the moderate swing ratio inside the rhythmic reading of the eight-tick octave (T7), connecting musical intervals to the phi-ladder constants and the underlying functional equation without new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.