perfectFifth
This definition supplies the just perfect fifth frequency ratio as the positive real 3/2. Scale theorists comparing just intonation to equal temperament cite it when bounding interval deviation. The construction packages the literal into the positive-real subtype with an automated positivity check.
claimThe just perfect fifth frequency ratio is the positive real number $3/2$.
background
FrequencyRatio is the subtype of positive real numbers, serving as the carrier for frequency ratios in this strict musical realization. The module supplies domain-rich musical structures over these ratios, employing equality cost for comparisons in the strict pass while leaving richer psychoacoustic dissonance costs for later refinement. It depends on the equal-tempered perfect fifth $2^{7/12}$ defined in the Aesthetics module, which acts as the numerical comparison target.
proof idea
One-line definition that constructs the subtype element via the literal 3/2 and discharges the positivity proof obligation with norm_num.
why it matters in Recognition Science
It supplies the just-fifth value required by the fifth_quality theorem, which establishes that the 12-TET fifth lies within 0.003 of the just value. This anchors musical interval comparisons inside the universal forcing framework and supports the eight-tick octave structure. Later refinements can replace equality cost with psychoacoustic measures.
scope and limits
- Does not define the equal-tempered fifth.
- Does not incorporate psychoacoustic dissonance costs.
- Does not extend to non-positive ratios.
Lean usage
theorem example_use : |perfectFifth - (2^(7/12 : ℝ))| < 0.003 := by simp [perfectFifth]; norm_numformal statement (Lean)
34noncomputable def perfectFifth : FrequencyRatio := ⟨(3 : ℝ) / 2, by norm_num⟩