IndisputableMonolith.Cost.Derivative
The Cost.Derivative module proves differentiability of J(x) = (x + x^{-1})/2 - 1 for x > 0 and supplies explicit derivative and linearization lemmas. Recognition Science researchers cite these when localizing the cost function near fixed points or applying the Recognition Composition Law. The module consists of direct applications of Mathlib real-analysis predicates to the closed-form expression of J.
claim$J(x) = \frac{x + x^{-1}}{2} - 1$ is differentiable for every $x > 0$.
background
The module extends IndisputableMonolith.Cost, which introduces the J-cost as the basic recognition cost obeying the Recognition Composition Law. It operates inside the T5 J-uniqueness step of the forcing chain, where J(x) is also written cosh(log x) - 1. The supplied DOC_COMMENT states the core claim that this explicit algebraic function is differentiable on the positive reals.
proof idea
The module collects targeted lemmas. differentiableAt_Jcost applies Mathlib's differentiableAt predicate to the explicit form of J. deriv_Jcost_eq computes the matching derivative expression. linJ, remJ and their unit variants supply first-order linearization and remainder terms. All proofs are one-line or short wrappers that invoke standard real-analysis rules from the Mathlib import.
why it matters in Recognition Science
The module supplies the derivative and linearization tools required by the Cost domain. Its sibling results (linJ_matches_harm_def, harm_linearization_correct) rely on these statements and support mass-formula and phi-ladder constructions higher in the Recognition Science framework.
scope and limits
- Does not treat x ≤ 0 or complex arguments.
- Does not compute second or higher derivatives.
- Does not invoke the eight-tick octave or spatial dimension D = 3.
- Does not address the alpha band or G, hbar constants.