ledgerSkew_pos_above_one
plain-language theorem explainer
The theorem establishes that ledger skew is strictly positive for any real ratio exceeding unity. Music theorists applying Recognition Science to interval valence would cite it when proving directional bias in harmonic structures above the reference. The proof is a short tactic sequence that unfolds the definition and closes via linear arithmetic after deriving the reciprocal bound.
Claim. For every real number $r$ with $r > 1$, the inequality $0 < r - r^{-1}$ holds.
background
The MusicTheory.Valence module defines ledgerSkew as the explicit difference $r - r^{-1}$, serving as a signed measure of asymmetry for ratios in harmonic analysis. This definition appears alongside sibling constructions for major and minor thirds and supports the broader valence calculations in the Recognition framework. The sole upstream dependency is the ledgerSkew definition itself, which supplies the algebraic expression used in the goal.
proof idea
The tactic proof unfolds ledgerSkew to reduce the claim to positivity of $r - r^{-1}$. It obtains $0 < r$ by linarith from the hypothesis $r > 1$, invokes the lemma inv_lt_one_of_one_lt₀ to secure $r^{-1} < 1$, and finishes with a final linarith step that combines the two inequalities.
why it matters
The result supplies a foundational positivity fact required for the subsequent skew comparisons and antisymmetry lemmas within the same module. It anchors the directional analysis of musical intervals in the Recognition Science music-theory extension, where ledger skew quantifies valence bias. No immediate downstream theorems are recorded, yet the lemma closes the basic case needed before interval-specific skew statements can be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.