hasDerivAt_Jcost
plain-language theorem explainer
Recognition Science researchers cite the derivative of the J-cost when locating minima or scaling along the phi-ladder. The claim states that J(x) = (x + x^{-1})/2 - 1 has derivative (1 - x^{-2})/2 at every nonzero real x. The proof reduces the statement to the chain rule for addition, inversion, and constant subtraction, then matches coefficients by algebraic identity.
Claim. For every real number $x$ with $x ≠ 0$, the function $J(x) := (x + x^{-1})/2 - 1$ satisfies that its derivative at $x$ equals $(1 - x^{-2})/2$.
background
The J-cost is defined in the Cost module by the expression (x + x^{-1})/2 - 1. This matches the J-uniqueness form from the forcing chain, equivalently written as cosh(log x) - 1, and satisfies the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The module also records nonnegativity, symmetry under inversion, and agreement with exponential forms that appear in discrete tier calculations.
proof idea
The proof unfolds the definition of Jcost, applies HasDerivAt.add to the sum and hasDerivAt_inv to the reciprocal term, divides the result by the constant 2, subtracts the zero derivative of the constant 1, then rewrites the coefficient (1 + (-(x^2)^{-1}))/2 as (1 - x^{-2})/2 via inv_pow and linarith.
why it matters
The result is invoked directly by deriv_Jcost_one to conclude that the derivative vanishes at x = 1, confirming a stationary point at the self-similar fixed point. It supplies the local analytic behavior required for cost arguments in the T5 J-uniqueness step and the T6 phi fixed-point construction, and supports derivative calculations that feed into the eight-tick octave and D = 3 spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.