skew_increases_with_interval_size
plain-language theorem explainer
The monotonicity result shows that for ratios r1 and r2 satisfying 1 < r1 < r2 < 2, the ledger skew r1 - 1/r1 is strictly less than r2 - 1/r2. Researchers modeling interval valence in harmonic systems would reference this when establishing orderings among musical intervals. The short tactic proof unfolds the skew definition, derives the reciprocal inequality from the ordering, and closes with linear arithmetic.
Claim. Let $r_1, r_2$ be real numbers satisfying $1 < r_1 < r_2 < 2$. Then $r_1 - r_1^{-1} < r_2 - r_2^{-1}$.
background
In the Valence module, ledgerSkew is defined as the difference between a ratio and its reciprocal. This quantity measures the asymmetry or skew associated with an interval ratio r > 1. The theorem operates in the context of positive real ratios less than 2, which covers common musical intervals such as thirds and fifths. It depends on the ledgerSkew definition and the Valence inductive type for classifying positive, negative, or neutral contributions, though the latter is not invoked in this monotonicity statement.
proof idea
The proof unfolds the ledgerSkew definition to obtain the inequality r1 - 1/r1 < r2 - 1/r2. It first establishes positivity of both r1 and r2 via linarith from the lower bound greater than 1. The reciprocal inequality 1/r2 < 1/r1 follows from the ordering r1 < r2 and positivity. The final step applies linarith to combine these facts into the desired skew comparison.
why it matters
This lemma provides the monotonicity foundation for comparing skew values across different interval sizes in the music theory component of Recognition Science. Although no immediate downstream uses are recorded, it underpins sibling results such as major_third_skew and minor_third_skew by guaranteeing that larger ratios within the octave produce larger positive skew. It aligns with the broader framework's use of phi-ladder structures for mass and interval quantization, where ordered skew contributes to valence assignments in harmonic modes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.