minor_third_skew_pos
plain-language theorem explainer
The declaration shows that the ledger skew of the minor third interval is strictly positive. Researchers analyzing harmonic valence within Recognition Science would cite this when ordering interval skews for major and minor thirds. The proof reduces the claim to a numerical check by substituting the explicit skew value already computed for the same interval.
Claim. Let $r = 6/5$. Then $0 < r - r^{-1}$.
background
In the MusicTheory.Valence module the ledger skew of a ratio $r$ is defined by ledgerSkew(r) := r - r^{-1}. The minor third is fixed at the ratio 6/5, matching the definition imported from HarmonicModes. The theorem minor_third_skew already records the exact evaluation ledgerSkew(6/5) = 11/30.
proof idea
The proof is a one-line wrapper that rewrites the goal by the minor_third_skew lemma and then applies norm_num to discharge the resulting numerical inequality 0 < 11/30.
why it matters
This result supplies the positivity half of the minor-third skew needed for downstream comparisons such as major_skew_gt_minor_skew. It sits inside the valence analysis that treats interval skews as signed quantities on the phi-ladder, consistent with the Recognition Composition Law and the eight-tick octave structure. No open scaffolding is closed by this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.