justFifth
The just perfect fifth frequency ratio is defined as the real number 3/2. Music theorists comparing just intonation to twelve-tone equal temperament cite this constant when measuring interval purity against the equal-tempered fifth. The definition is a direct numerical assignment with no computation or lemmas required.
claimThe just perfect fifth frequency ratio is given by $3/2$.
background
The module derives the Western 12-tone scale from the golden ratio φ by optimizing consonance and closure under frequency ratios. It notes that 12 semitones per octave satisfy 2^(1/12) ≈ 1.0595, while the perfect fifth (7 semitones) satisfies 2^(7/12) ≈ 1.4983, which is close to the simple ratio 3/2. The upstream definition fourth supplies the complementary interval 4/3 for harmonic mode constructions.
proof idea
Direct definition assigning the rational constant 3/2 to the real number justFifth. No lemmas or tactics are invoked; the value stands as a primitive constant for downstream numerical comparisons.
why it matters in Recognition Science
This definition supplies the reference just interval used by the theorem fifth_quality to bound the deviation of the equal-tempered fifth below 0.003. It instantiates the RS mechanism for optimal ratios, where the circle of fifths closes after 12 steps because (3/2)^12 ≈ 2^7 and 12 emerges from φ^5 scaling for consonance. It supports the prediction that 12 semitones optimize Western harmony while leaving open the φ-derived structure of alternative scales such as 5, 7, 19 or 31 tones.
scope and limits
- Does not derive the ratio 3/2 from the golden ratio φ.
- Does not prove the numerical approximation to 2^(7/12).
- Does not address closure properties of the circle of fifths.
- Does not specify semitone counts or other scale sizes.
formal statement (Lean)
49def justFifth : ℝ := 3 / 2
proof body
Definition body.
50
51/-- Perfect fourth frequency ratio: 2^(5/12). -/