minor_is_positive_but_less
plain-language theorem explainer
The theorem shows that the minor third ratio of 6/5 receives a positive valence label under zero threshold. Music theorists working with Recognition Science models of interval affect would cite it when linking frequency ratios to hedonic sign. The proof is a direct term reduction that substitutes the precomputed ledger skew value and checks the sign numerically.
Claim. Let $r = 6/5$ be the minor third. The valence classification of $r$ at threshold $0$ is positive, which holds precisely when ledgerSkew$(r) > 0$.
background
In the Valence module the minor third is introduced as the ratio $6/5$. The classification function returns positive when ledgerSkew of the ratio exceeds the supplied threshold, negative when it falls below the negated threshold, and neutral otherwise. The supporting lemma minor_third_skew records that ledgerSkew$(6/5)$ evaluates exactly to $11/30$. The surrounding MusicTheory setting treats ledger skew as the direct carrier of valence, with the explicit remark that the skew difference between major and minor thirds is the valence difference heard by the listener.
proof idea
The term proof unfolds the definition of classifyValence, rewrites the ledgerSkew subterm via the minor_third_skew lemma, and finishes with norm_num to confirm that $11/30 > 0$.
why it matters
The result supplies a concrete instance of the module's central identification of ledger skew with hedonic experience. It sits inside the broader Recognition Science program that derives musical affect from the same ledgerSkew function used for interval classification, without yet feeding any downstream theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.