valence_difference_one_twelfth
plain-language theorem explainer
Ledger skew of the major third exceeds that of the minor third by exactly one twelfth. Recognition Science music theorists cite this identity when calibrating valence for just-intonation intervals. The proof rewrites the difference via the valence difference identity and reduces the resulting arithmetic constants directly.
Claim. Let $s(r) = r - r^{-1}$. Then $s(5/4) - s(6/5) = 1/12$.
background
In the MusicTheory.Valence module, ledgerSkew is the map sending a ratio $r$ to $r - r^{-1}$. The major third is fixed at the just-intonation ratio 5/4 and the minor third at 6/5. The valence difference identity expresses the difference of these two ledger-skew values as a single expression that the present theorem evaluates.
proof idea
One-line wrapper that rewrites the left-hand side using the valence difference identity and then normalizes the resulting rational arithmetic.
why it matters
The identity supplies a concrete numerical anchor for valence calculations inside the Recognition Science treatment of harmonic modes. It sits downstream of the ledgerSkew definition and the interval constants imported from HarmonicModes, providing a calibrated difference that later scale constructions can invoke.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.