ledgerSkew_zero_at_unity
plain-language theorem explainer
The theorem asserts that ledger skew vanishes exactly at the unit ratio. Analysts of harmonic modes in Recognition Science reference this when confirming zero baseline for valence skew calculations. The proof is a direct simplification that unfolds the definition of ledgerSkew.
Claim. Let $f(r) = r - r^{-1}$ for real $r$. Then $f(1) = 0$.
background
The Valence submodule defines ledgerSkew on real numbers as the difference between the argument and its reciprocal. This construction supports analysis of ratio asymmetries in harmonic contexts built on HarmonicModes. The upstream definition supplies the algebraic expression $r - r^{-1}$ used throughout the module.
proof idea
This is a one-line wrapper that applies the simp tactic to unfold the definition of ledgerSkew and evaluate the expression at unity.
why it matters
The result anchors the family of skew theorems in the Valence module, including sign properties for ratios above and below one. It connects to the self-similar fixed point in the forcing chain where unity serves as the identity. No downstream uses are listed, but it enables the antisymmetry and positivity results among siblings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.