majorThird_pos
plain-language theorem explainer
The declaration proves that the major third ratio exceeds zero. Harmonic mode constructions in the Recognition Science music theory module cite this to ensure interval objects are well-defined over the positives. The proof is a direct numerical check that reduces the inequality to an arithmetic fact.
Claim. $0 < 5/4$, where the major third is the just-intonation ratio.
background
In the HarmonicModes module the major third is introduced as the just-intonation interval 5/4. Parallel definitions appear in the Valence and Aesthetics.MusicalScale modules, the latter using the equal-tempered form 2^{4/12}. The module imports Mathlib for the reals and Cost for the surrounding interval structures; the positivity fact is therefore a prerequisite for packaging any ratio into a MusicalInterval.
proof idea
The proof is a one-line wrapper that applies the norm_num tactic to the concrete inequality 0 < 5/4.
why it matters
The result is required by the downstream majorThirdInterval definition, which pairs the ratio with its positivity witness. This supplies the basic positive-interval facts used throughout the HarmonicModes development and aligns with the Recognition framework's need for well-ordered ratios before composing larger structures such as modes or scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.