minor_third_skew
plain-language theorem explainer
The theorem states that the ledger skew of the minor third interval ratio 6/5 equals 11/30. Researchers classifying harmonic intervals by valence would cite this to anchor comparisons between minor and major thirds. The proof is a one-line wrapper that unfolds the ledgerSkew definition via simp and normalizes the rational arithmetic with ring.
Claim. Let $r = 6/5$. Then $r - r^{-1} = 11/30$.
background
In the MusicTheory.Valence module the minor third is introduced as the constant 6/5. The ledgerSkew function is defined on any positive real ratio $r$ by ledgerSkew($r$) := $r - r^{-1}$. The present theorem supplies the concrete numerical value needed for downstream valence comparisons and positivity checks.
proof idea
The proof is a one-line wrapper that applies simp to unfold ledgerSkew and then invokes ring to reduce the resulting expression 6/5 - 5/6 to the fraction 11/30.
why it matters
The result is invoked by major_skew_gt_minor_skew to order the two thirds, by minor_third_skew_pos to establish strict positivity, by minor_is_positive_but_less for valence classification, and by valence_difference to compute the exact gap between major and minor skews. It therefore supplies the numerical anchor for the valence classification section of the MusicTheory development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.