perfectFifth
plain-language theorem explainer
The definition supplies the equal-tempered perfect fifth frequency ratio as 2 raised to the power 7/12. Researchers comparing 12-tone scales to the golden ratio phi in Recognition Science cite it when measuring deviation from just intonation. It is introduced as a direct real-number expression with no lemmas or reduction steps.
Claim. The frequency ratio of the perfect fifth in twelve-tone equal temperament is given by $2^{7/12}$.
background
The module derives the Western 12-tone scale from phi by optimizing consonance and closure under fifths. It notes that 12 semitones per octave arise because round(phi^5 / 2) yields 12, and the circle of fifths returns after 12 steps since (3/2)^12 approximates 2^7. Upstream results define the just fifth as the constant 3/2 in CircleOfFifths.fifth and HarmonicModes.fifth, and as a FrequencyRatio wrapper in UniversalForcing.Strict.Music.perfectFifth.
proof idea
Direct definition that assigns the arithmetic expression 2^(7/12) to the identifier. No tactics or lemmas are invoked; the body is the standard equal-temperament formula for seven semitones.
why it matters
This definition is referenced by the theorem fifth_quality, which bounds its distance to the just fifth below 0.003. It supplies the equal-tempered value needed to connect the 12-tone scale to the eight-tick octave (T7) and the phi^5 origin of 12 in the forcing chain. The module uses it to quantify how equal temperament approximates just ratios while preserving phi-related structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.