third_quality
plain-language theorem explainer
The equal-tempered major third exceeds the just major third. Intonation theorists cite the result to measure the 14-cent sharpness of the 12-tone scale's major third. The proof reduces the claim to a cube comparison by rewriting the exponent as 1/3 and invoking the real rpow monotonicity lemma after a direct numerical check that (5/4)^3 is less than 2.
Claim. In twelve-tone equal temperament the major third satisfies $2^{1/3} > 5/4$, where the left side is the frequency ratio $2^{4/12}$ and the right side is the just-intonation major third.
background
majorThird is the real number $2^{4/12}$ that gives the equal-tempered major third in the 12-tone scale. justMajorThird is the rational $5/4$ that supplies the just-intonation counterpart. The module sets these definitions inside a derivation of the Western scale from the golden ratio, noting that twelve semitones arise as the integer nearest to a multiple of φ^5 and that the circle of fifths closes after twelve steps because $(3/2)^{12} ≈ 2^7$. Upstream results supply the two concrete ratios and the scale function used in related cosmological and spectroscopic contexts.
proof idea
The tactic proof first rewrites the exponent 4/12 as 1/3 by norm_num, then verifies by direct computation that $(5/4)^3 < 2$. It rewrites the base via the identity $(5/4) = ((5/4)^3)^{1/3}$ using Real.pow_rpow_inv_natCast, substitutes the inverse exponent, and finishes with a single application of Real.rpow_lt_rpow under the positivity hypotheses.
why it matters
The inequality supplies a concrete numerical anchor for the module's claim that the 12-tone scale balances consonance with φ-scaling. It quantifies the deviation of the equal-tempered major third from just intonation, consistent with the prediction that $2^{4/12} ≈ 1.26$ lies slightly above 5/4. The result sits inside the Recognition Science account in which twelve emerges from optimizing closure under the golden-ratio ladder and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.