jcost_deriv
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove convexity or second-derivative positivity of J-cost.
- Does not supply numerical bounds or decay rates away from x = 1.
- Does not connect the derivative to phi-ladder rungs or physical constants.
- Does not address implementation stability or discretization effects.
formal statement (Lean)
83noncomputable def jcost_deriv (x : ℝ) : ℝ := (1 - (x⁻¹)^2) / 2
proof body
Definition body.
84
85/-- **THEOREM IC-005.6**: J'(1) = 0 — the gradient vanishes at the ground state.
86 This confirms x = 1 is the unique critical point (and global minimum). -/