jcost_deriv_neg_of_lt_one
plain-language theorem explainer
The derivative of the J-cost function is strictly negative for all positive reals less than one. Researchers analyzing Recognition Science complexity classes cite this to confirm that the gradient drives states toward the unique minimum at x=1 from below. The proof unfolds the explicit derivative formula, applies a quotient sign lemma, establishes that the squared reciprocal exceeds one via inverse and power inequalities, and closes with linear arithmetic.
Claim. For every real number $x$ with $0 < x < 1$, the derivative of the J-cost satisfies $J'(x) < 0$, where $J'(x) = (1 - x^{-2})/2$.
background
The J-cost is defined by $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$, and its derivative is the explicit function $J'(x) = (1 - x^{-2})/2$. Module IC-005 treats the computational complexity of physics as determined by the structure of J-cost minimization, which is strictly convex with unique minimum at $x=1$ (verifiable in O(1) time) while higher phi-rung states require exponential effort. Upstream results include the ledger factorization that calibrates J and the phi-forcing structure that supplies the cost function itself.
proof idea
The proof unfolds the derivative definition to obtain the quotient form, applies the lemma that a negative numerator over a positive denominator is negative, proves $x^{-2} > 1$ by invoking the power inequality for positive exponents together with the reciprocal inequality for arguments in (0,1), and finishes with linear arithmetic.
why it matters
This result supplies the negative gradient sign below the minimum and is invoked by the gradient-descent convergence theorem and by the IC-005 complexity-class certificate. It completes the IC-005.8 step showing that J-cost minimization is efficiently solvable by local updates, consistent with the eight-tick octave and the convex structure of the cost function. It supports the broader claim that ground-state verification lies in P while leaving phi-rung computations in EXPTIME.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.