deriv_Jcost_one
plain-language theorem explainer
deriv_Jcost_one establishes that the derivative of the J-cost function vanishes at argument 1. Researchers analyzing equilibrium points in recognition sheaves or ledger dynamics cite this when proving stationarity of the cost functional. The argument is a short term-mode reduction that invokes the general HasDerivAt formula for Jcost at x=1, simplifies the coefficient via norm_num, and extracts the derivative value.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$. Then the derivative satisfies $J'(1) = 0$.
background
Jcost is the real function defined by Jcost(x) := (x + x^{-1})/2 - 1. This expression coincides with the J-uniqueness map from the forcing chain and equals cosh(log x) - 1. The Cost module develops its analytic properties, including differentiability away from zero and strict convexity on the positive reals. The upstream result hasDerivAt_Jcost supplies the explicit derivative formula HasDerivAt Jcost ((1 - x^{-1}^2)/2) x whenever x ≠ 0, obtained by direct differentiation of the sum and reciprocal terms.
proof idea
The term proof first applies hasDerivAt_Jcost at the concrete point 1, discharging the nonzero hypothesis by norm_num. It then uses simp to reduce the derivative coefficient (1 - 1^{-1}^2)/2 to zero inside the HasDerivAt fact. Finally it extracts the derivative value via h.deriv.
why it matters
This lemma is invoked directly by J_stationary_at_one in Relativity.Dynamics.RecognitionSheaf, which records the core stationarity principle: the recognition ratio equal to one is the stable equilibrium of the ledger dynamics. The result therefore supplies the local analytic ingredient needed for sections of the recognition sheaf to satisfy the J-cost stationarity condition. In the broader framework it closes the T5 J-uniqueness step by confirming a critical point at the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.