fifthInterval
plain-language theorem explainer
The fifthInterval definition packages the ratio 3/2 as a MusicalInterval for harmonic calculations. Music theorists extending Recognition Science to intervals cite it when invoking Jcost on the perfect fifth. The definition is a one-line structure constructor that pairs the pre-defined fifth ratio with its positivity theorem.
Claim. The fifth interval is the MusicalInterval whose ratio is $3/2$ and whose positivity is witnessed by $0 < 3/2$.
background
MusicalInterval is a structure with fields ratio : ℝ and ratio_pos : 0 < ratio; it also carries the derived Jcost function that applies Jcost to the ratio. The fifth ratio is defined as 3/2 in the CircleOfFifths module, where the doc-comment notes that the 12/8 equivalence between semitones and RS modes is the perfect fifth. The same ratio and its norm_num positivity proof appear as siblings in the HarmonicModes module.
proof idea
It is a one-line wrapper that applies the MusicalInterval constructor to the fifth ratio and the fifth_pos theorem.
why it matters
This definition supplies a typed perfect-fifth interval that supports J-cost calculations in music-theoretic extensions of the framework. It directly encodes the 3/2 ratio that the CircleOfFifths doc-comment identifies as the bridge between 12 semitones and the eight-tick octave. No downstream uses are recorded yet, but the construction sits alongside octave, fourth, and third intervals in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.