fifth_quality
plain-language theorem explainer
Frequency ratios in 12-tone equal temperament place the fifth within 0.003 of the just ratio 3/2. Acousticians and music theorists cite the bound when justifying 12-TET as a practical compromise. The proof derives the inequality by bounding the exponential 2^(7/12) between 1.497 and 1.5 using root extractions and real-number comparisons.
Claim. $ |2^{7/12} - 3/2| < 0.003 $
background
In the Aesthetics.MusicalScale module the 12-tone equal temperament scale is constructed by optimizing frequency ratios that tie to the golden ratio φ. The perfect fifth is the equal-tempered ratio 2^(7/12) while the just fifth is the simple ratio 3/2. The module notes that 12 emerges from φ^5 scaling and that the circle of fifths closes after 12 steps because (3/2)^12 is close to 2^7. Upstream definitions supply justFifth := 3/2 and perfectFifth := 2^(7/12 : ℝ).
proof idea
The tactic proof first simplifies the two definitions. It proves the upper bound 2^(7/12) < 3/2 by showing (3/2)^12 > 128 via norm_num, rewriting both sides as 12th roots, and applying Real.rpow_lt_rpow. A matching lower bound 2^(7/12) > 1.497 is obtained from 1.497^12 < 128 and the same root extraction. The goal is then split by abs_lt and closed by linarith.
why it matters
The result quantifies the approximation quality that lets 12 steps serve as a practical octave in the circle of fifths. It supports the module claim that 12 semitones arise from φ-related optimization of consonance and closure. Within Recognition Science this aligns with the eight-tick octave (T7) and the self-similar fixed point φ (T6), though the theorem itself remains local to the aesthetic derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.