valence_difference
plain-language theorem explainer
The theorem states that the ledger skew of the major third minus the ledger skew of the minor third equals 5/60. Researchers working on harmonic valence or interval skew in the Recognition Science music theory layer would cite this result. The proof is a one-line wrapper that rewrites using the precomputed skew values for each interval and then normalizes the arithmetic.
Claim. Let $J(r) := r - r^{-1}$. Then $J(5/4) - J(6/5) = 5/60$.
background
In the Valence module, ledgerSkew is the map sending a real number r to r minus its reciprocal. The major third is defined as 5/4 and the minor third as 6/5, matching the noncomputable definitions imported from HarmonicModes. The upstream theorem major_third_skew establishes that ledgerSkew of the major third equals 9/20; a parallel result minor_third_skew supplies the corresponding value for the minor third.
proof idea
The proof is a one-line wrapper that applies major_third_skew and minor_third_skew to substitute the explicit skew values, then invokes norm_num to evaluate the resulting rational difference.
why it matters
This result is invoked directly by valence_difference_one_twelfth to obtain the simplified equality 1/12. It supplies an intermediate arithmetic step in the valence calculations of the MusicTheory.Valence component, supporting the treatment of interval skew within the broader Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.