swing_triplet_is_octave_ratio
plain-language theorem explainer
The declaration asserts that the triplet swing ratio equals 2, matching the octave ratio in the Recognition Science rhythm module. Researchers modeling musical subdivisions through the eight-tick octave and phi-ladder would cite this to fix triplet timing. The proof is a direct reflexivity step on the constant definition of the swing ratio.
Claim. The triplet swing ratio equals the octave ratio 2.
background
In the MusicTheory.Rhythm module the swing ratio for triplets is introduced as the real constant 2. This value aligns with the eight-tick octave (period 2^3) from the unified forcing chain T7. The upstream definition swingRatio_triplet supplies the base value used by the theorem.
proof idea
One-line wrapper that applies reflexivity directly to the definition swingRatio_triplet := 2.
why it matters
The equality anchors triplet rhythm inside the eight-tick octave of the Recognition framework. It supports self-similar timing derived from J-uniqueness and the phi fixed point. No downstream theorems are listed, yet the result contributes to the rhythmic reading of the T7 octave step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.