classifyValence
plain-language theorem explainer
classifyValence assigns a valence label to a real ratio r by comparing its skew, defined as r minus the reciprocal of r, against a supplied threshold. Music theorists working within the Recognition framework cite it to label intervals as positive, negative, or neutral. The definition executes a direct three-way conditional on the sign of that skew relative to the threshold.
Claim. For a real number $r$ and threshold $t$, the valence is positive when $r - r^{-1} > t$, negative when $r - r^{-1} < -t$, and neutral otherwise.
background
The valence type is an inductive data type whose constructors are positive, negative, and neutral. The skew of a ratio $r$ is the real-valued difference $r - r^{-1}$. This definition lives in the MusicTheory.Valence module, which imports HarmonicModes, and applies the skew computation to produce the label.
proof idea
The definition is a direct conditional expression that evaluates the skew of $r$ and branches on whether it exceeds the threshold, lies below the negated threshold, or falls in between.
why it matters
It supplies the classification step invoked by the theorems that establish positive valence for the major third and the minor third at zero threshold. The definition therefore anchors the music-theory layer that maps real ratios to discrete categories inside the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.