perfectFifth
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.