major_third_skew
plain-language theorem explainer
The major third skew theorem states that the ledger skew of the major third equals 9/20. Music theorists classifying intervals by valence in the Recognition Science framework cite this result to establish positivity for major thirds. The proof is a one-line wrapper that simplifies the ledger skew definition and applies ring normalization.
Claim. Let $r = 5/4$ denote the major third ratio. Then the ledger skew $r - r^{-1}$ equals $9/20$.
background
The Valence module defines ledgerSkew as the map sending a real ratio r to r minus its reciprocal. It also defines majorThird as the just major third 5/4, matching the definition supplied by the HarmonicModes module. These sit inside the MusicTheory.Valence module, which develops valence classification for musical intervals by measuring reciprocal deviation from unity via ledger skew.
proof idea
The proof is a one-line wrapper that applies simp to unfold ledgerSkew on the majorThird definition and then uses ring to normalize the arithmetic 5/4 - 4/5.
why it matters
This result feeds directly into major_is_positive, major_third_skew_pos, major_skew_gt_minor_skew, and valence_difference. It supplies the explicit numerical anchor needed for valence classification of the major third within the Recognition Science treatment of harmonic modes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.