major_is_positive
plain-language theorem explainer
The theorem establishes that the major third interval, defined as the ratio 5/4, receives positive valence classification when the threshold is zero. Music theorists working in the Recognition Science framework would cite this result to anchor the positive character of the major third under the ledgerSkew measure. The proof proceeds by unfolding the classification definition, substituting the precomputed skew value of 9/20 from the companion lemma, and verifying the inequality by normalization.
Claim. Let $r = 5/4$ denote the major third ratio. Then classifyValence$(r, 0) = $ positive, where classifyValence$(r, t)$ returns positive precisely when ledgerSkew$(r) > t$.
background
In the MusicTheory.Valence module the classifyValence function maps an interval ratio $r$ and threshold $t$ to a Valence label by comparing ledgerSkew$(r)$ against $t$: positive when the skew exceeds $t$, negative when it falls below $-t$, and neutral otherwise. The majorThird constant is defined as the just ratio $5/4$. The ledgerSkew function supplies the signed deviation measure used for this classification. The upstream major_third_skew lemma records the explicit evaluation ledgerSkew$(5/4) = 9/20$.
proof idea
The term-mode proof first unfolds classifyValence to expose the conditional ledgerSkew majorThird > 0. It then rewrites the ledgerSkew term via the major_third_skew lemma, which supplies the concrete value 9/20. The final norm_num step dispatches the arithmetic comparison 9/20 > 0.
why it matters
The result confirms the positive valence assignment for the major third, supporting the framework's systematic classification of harmonic intervals by ledgerSkew sign. It draws directly on the major_third_skew computation and the classifyValence definition. Within the Recognition Science music-theory layer such valence statements contribute to aesthetic analysis of scales and modes, although no downstream theorems currently depend on this particular declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.