hasDerivAt_Jcost
plain-language theorem explainer
The Jcost function, given by (x + x^{-1})/2 - 1 for real x, admits the derivative (1 - x^{-2})/2 at every nonzero point. Researchers deriving cost gradients in Recognition Science ledger models or phi-forcing calculations would reference this result. The proof applies standard real-analysis differentiation rules for sums, reciprocals, and constants, then simplifies the coefficient algebraically.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$. For every real number $x ≠ 0$, the derivative of $J$ at $x$ equals $(1 - x^{-2})/2$.
background
Jcost is defined in the Cost module as (x + x^{-1})/2 - 1, matching the J-uniqueness expression from the forcing chain T5. This module imports Mathlib for real analysis and depends on structures from ledger factorization and spectral emergence that employ J-cost in physical calculations. Upstream results include PhiForcingDerived.of which structures J-cost and DAlembert.LedgerFactorization.of which calibrates J.
proof idea
The proof unfolds the definition of Jcost and chains HasDerivAt rules: additivity of derivatives for the sum y + y^{-1}, using hasDerivAt_id and hasDerivAt_inv, followed by division by the constant 2 and subtraction of the constant 1. Algebraic rewriting equates the resulting coefficient to (1 - x^{-1}^2)/2 via inv_pow and linarith.
why it matters
This theorem supports the downstream result deriv_Jcost_one showing vanishing derivative at unity, which aligns with the fixed point of the phi-ladder in Recognition Science. It underpins differentiation steps in cost-based derivations for mass formulas and the eight-tick octave. The result closes a basic analytic requirement for the J-cost appearing in T5 J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.