IndisputableMonolith.Cost.Derivative
Module Cost.Derivative establishes that J(x) = (x + x^{-1})/2 - 1 is differentiable for every x > 0 and supplies the explicit derivative. Recognition Science researchers cite these lemmas when linearizing the cost function for the phi-ladder and RCL applications. The module consists of direct applications of Mathlib real-analysis tactics to the algebraic form of J, producing results such as differentiableAt_Jcost and deriv_Jcost_eq.
claimThe map J : (0, ∞) → ℝ given by J(x) = (x + x^{-1})/2 - 1 is differentiable at every point, with derivative J'(x) = (1 - x^{-2})/2.
background
The module imports the base J-cost definition from IndisputableMonolith.Cost, where J(x) encodes the recognition cost for scaling factor x and satisfies the functional equation J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). It introduces auxiliary declarations such as differentiableAt_Jcost (asserting differentiability at a positive point) and deriv_Jcost_eq (equating the derivative to the closed-form expression). This sits inside the T5 J-uniqueness step of the forcing chain, where J is also written cosh(log x) - 1.
proof idea
The module applies Mathlib differentiability lemmas for sums, inverses, and powers to the explicit algebraic expression of J. differentiableAt_Jcost follows from composition rules valid on (0, ∞). deriv_Jcost_eq is obtained by direct term-mode computation of the derivative. Subsequent siblings such as linJ and harm_linearization_correct reuse these facts to match the harmonic linearization.
why it matters in Recognition Science
These derivative facts feed the linearization lemmas linJ and harm_linearization_correct inside the same module, which connect directly to the Recognition Composition Law and the self-similar fixed point phi (T6). The results close the calculus gap required for the eight-tick octave and the mass formula on the phi-ladder.
scope and limits
- Does not establish differentiability at x ≤ 0.
- Does not supply higher-order derivatives or Taylor series.
- Does not treat complex or matrix extensions of J.
- Does not prove global convexity or integral identities.