ledgerSkew_antisymmetric
plain-language theorem explainer
Ledger skew is antisymmetric under inversion: for nonzero real r the skew of the reciprocal equals the negative of the skew of r. Music theorists modeling signed interval deviations in the Recognition Science valence calculations would cite the result when establishing consistent treatment of ratios above and below unity. The proof is a one-line algebraic reduction that unfolds the definition, cancels the double inverse, and simplifies by ring.
Claim. For every real number $r$ with $r ≠ 0$, if ledgerSkew$(r) := r - r^{-1}$, then ledgerSkew$(r^{-1}) = -$ledgerSkew$(r)$.
background
Ledger skew is the real-valued map defined by ledgerSkew$(r) := r - r^{-1}$. It quantifies the signed deviation of a ratio from unity and is used inside the Valence module to compare harmonic intervals. The upstream Skew abbrev from RSNative.Core supplies only the dimensional wrapper; the present theorem works directly with the underlying real expression.
proof idea
Unfold the definition of ledgerSkew, rewrite the double inverse via inv_inv, then close with the ring tactic.
why it matters
The theorem supplies the basic antisymmetry fact required by the sibling declarations on major-third skew, minor-third skew and their positivity statements. It closes an algebraic prerequisite inside the music-theoretic layer without invoking the forcing chain, phi-ladder or Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.