differentiableAt_Jcost
plain-language theorem explainer
The J-cost function J(x) = (x + x^{-1})/2 - 1 is differentiable at every positive real x. Workers replacing harm axioms with linearization bounds in the Ethics module would cite this result to justify Taylor expansions of bond deltas. The proof unfolds the definition and chains the standard differentiability rules for addition, constant division, identity, and inversion at nonzero points.
Claim. For every real number $x > 0$, the function $J(x) = (x + x^{-1})/2 - 1$ is differentiable at $x$.
background
The J-cost function is the map $J(x) = (x + x^{-1})/2 - 1$ that appears in the Recognition Composition Law and in the phi-forcing derivation of the self-similar fixed point. The Cost.Derivative module supplies the calculus needed to replace axioms in the Ethics/Harm module by explicit linearizations and remainder bounds. Upstream structures such as PhiForcingDerived.of record the algebraic definition of J, while LedgerFactorization.of calibrates the same map on the positive reals.
proof idea
The term proof first records that x is nonzero, unfolds the definition of Jcost, then applies DifferentiableAt.sub to separate the variable part from the constant. The variable part is handled by DifferentiableAt.div_const applied to an addition of differentiableAt_id and differentiableAt_inv; the constant is immediate from differentiableAt_const.
why it matters
This lemma supplies the differentiability premise required by the sibling result deriv_Jcost_eq, which in turn feeds linBondDelta_is_derivative and the quadratic remainder bound remJ_quadratic. Those statements close the path from T5 J-uniqueness in the forcing chain to the consent derivation in the Ethics module, replacing an axiom with a calculus identity whose remainder is O(L^2).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.