ledgerSkew
plain-language theorem explainer
The ledgerSkew function maps a real number r to the difference r minus its reciprocal. Music theorists in the Recognition Science setting cite it to quantify signed deviation of interval ratios from unity when classifying valence. The declaration is a direct one-line definition with no proof obligations or auxiliary lemmas.
Claim. For a real number $r$, the ledger skew is defined by $r - r^{-1}$.
background
In the MusicTheory.Valence module the ledger skew supplies a signed measure of how far an interval ratio departs from 1. The module imports HarmonicModes to obtain concrete ratios such as majorThird and minorThird, both real numbers greater than 1. Downstream results establish that the function is zero at unity, positive when the argument exceeds 1, negative when the argument lies between 0 and 1, and antisymmetric under inversion.
proof idea
The declaration is a direct definition implemented as the single expression r - r⁻¹.
why it matters
ledgerSkew is the primitive used by classifyValence to decide positive, negative or neutral valence once a threshold is supplied. It also feeds the comparison major_skew_gt_minor_skew and the sign theorems ledgerSkew_pos_above_one and ledgerSkew_neg_below_one. Within the Recognition framework the construction supplies a concrete asymmetry detector for musical structures that is compatible with the eight-tick octave and the self-similar fixed point phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.