IndisputableMonolith.Cost.Derivative
The Cost.Derivative module establishes differentiability of the J-cost function J(x) = (x + x^{-1})/2 - 1 for all x > 0 together with an explicit derivative formula. Researchers analyzing local linearization or harmonic approximations inside the Recognition Science cost framework cite these lemmas when passing from the global Recognition Composition Law to first-order expansions. The module consists of short, direct applications of Mathlib real-analysis rules to the closed algebraic form of J.
claimThe map $J:(0,∞)→ℝ$ given by $J(x)=(x+x^{-1})/2-1$ is differentiable at every $x>0$, with $J'(x)=(1-x^{-2})/2$.
background
The parent module IndisputableMonolith.Cost defines the J-cost via the Recognition Composition Law J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y) together with the normalization J(1)=0. The explicit closed form J(x)=(x+x^{-1})/2-1 is the unique solution that is even under inversion. The Derivative module imports Mathlib to obtain the standard calculus facts needed for local analysis of this function on the positive reals.
proof idea
Each sibling lemma (differentiableAt_Jcost, deriv_Jcost_eq, etc.) is obtained by applying the differentiability of addition, scalar multiplication, and inversion on (0,∞) directly to the algebraic expression of J; no induction or special Recognition Science lemmas are required.
why it matters in Recognition Science
These differentiability statements supply the analytic foundation for the linearization lemmas linJ, linJ_eq_derivative_times_x and harm_linearization_correct that sit immediately downstream in the same Cost module. They thereby connect the global Recognition Composition Law to the first-order behavior used in the forcing chain at the self-similar fixed point.
scope and limits
- Does not treat differentiability at zero or for non-positive arguments.
- Does not compute second or higher derivatives.
- Does not address complex or matrix-valued extensions of J.
- Does not derive any physical interpretation of the derivative.