jcost_deriv
plain-language theorem explainer
J-cost derivative is defined by the closed-form expression (1 - x^{-2})/2. Researchers analyzing monotonic convergence of RS ground states cite this when proving that gradient steps reduce J-cost for x away from 1. The definition is obtained by direct differentiation of the convex J(x) = (x + x^{-1})/2 - 1 expression.
Claim. The derivative of J-cost is given by $J'(x) = (1 - x^{-2})/2$.
background
The PhysicsComplexityStructure module frames RS physics complexity through J-cost minimization. J(x) = (x + x^{-1})/2 - 1 is strictly convex with unique global minimum at x = 1, making ground-state verification linear-time. The derivative supplies the local slope for gradient analysis around this minimum. Upstream results on simplicial ledgers and option programs embed this cost function into ledger dynamics and mechanism design.
proof idea
One-line definition that encodes the analytic derivative of J-cost obtained by term-by-term differentiation of (x + x^{-1})/2 - 1.
why it matters
This definition supports the sign theorems jcost_deriv_pos_of_gt_one and jcost_deriv_neg_of_lt_one together with jcost_gradient_descent_converges, which establish that the gradient points toward x = 1. It fills the IC-005.6 slot confirming the unique critical point in the complexity summary. Within the RS framework it underpins the claim that local J-cost minimization is O(1) per step, consistent with eight-tick octave dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.