ledgerSkew_neg_below_one
plain-language theorem explainer
For positive real r below 1 the quantity r minus its reciprocal is negative. Music theorists applying Recognition Science to harmonic valence cite this sign fact when ordering distortions on the phi-ladder. The proof is a term-mode script that unfolds the definition and closes the inequality by linear arithmetic after invoking the reciprocal bound.
Claim. If $0 < r < 1$ for real $r$, then $r - r^{-1} < 0$.
background
ledgerSkew is the signed deviation r - r^{-1} introduced in the Valence module of MusicTheory. The module imports HarmonicModes and assembles a family of sign and ordering lemmas around this function. The present theorem supplies the negative case for arguments strictly below unity, pairing with the zero-at-unity and positive-above-one siblings.
proof idea
The script unfolds ledgerSkew to expose the difference r - r^{-1}. It then applies one_lt_inv₀ to the positivity and strict-upper-bound hypotheses to obtain 1 < r^{-1}. Linear arithmetic finishes the proof.
why it matters
The lemma completes the local sign chart for ledgerSkew inside the MusicTheory.Valence development. It supports downstream antisymmetry and comparison statements that feed valence calculations on the phi-ladder. No used-by edges are recorded yet, leaving the result as a self-contained building block for interval distortion ordering.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.