justFifth
plain-language theorem explainer
The just perfect fifth frequency ratio is fixed at 3/2. Music theorists working in the Recognition Science treatment of scales cite this constant when measuring how closely 12-tone equal temperament approximates just intonation. The definition is a direct numerical assignment with no derivation steps.
Claim. The just perfect fifth frequency ratio equals $3/2$.
background
The module derives the 12-tone equal temperament scale from the golden ratio φ by optimizing consonance via simple frequency ratios and closure under the circle of fifths. Key observations include 12 semitones per octave from 2^(1/12) and the perfect fifth (7 semitones) at 2^(7/12) ≈ 1.4983, which is compared against the just value 3/2. The upstream fourth definition supplies the complementary perfect fourth ratio 4/3 as the harmonic counterpart.
proof idea
Direct definition that assigns the constant 3/2. No lemmas or tactics are invoked.
why it matters
This supplies the just-intonation benchmark for the fifth_quality theorem, which bounds the deviation of the 12-TET fifth below 0.003. It implements the AE-001 mechanism linking consonance (simple ratios such as 3:2) and φ-scaling (12 ≈ φ^5 / log(3/2)) to the circle-of-fifths closure (3/2)^12 ≈ 2^7. The definition anchors the framework's prediction that 12 semitones optimize Western harmony.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.