JcostDeriv
plain-language theorem explainer
JcostDeriv supplies the explicit first-derivative formula for the cost function J. Workers on the cost-rate Euler-Lagrange equations cite it to locate the unique critical point at the ground state x=1. The definition is the direct algebraic reduction of the derivative of ½(x + x⁻¹) - 1.
Claim. Let $J(x) = ½(x + x^{-1}) - 1$ for $x > 0$. Then $J'(x) = (1 - x^{-2})/2$.
background
The Cost.Convexity module proves strict convexity of Jlog(t) = cosh(t) - 1 on ℝ and of Jcost(x) = ½(x + x^{-1}) - 1 on ℝ₊. These facts are foundational for the J-uniqueness statement T5 in the forcing chain. JcostDeriv is the explicit expression for the first derivative that vanishes at the minimum x=1.
proof idea
This is a direct definition that encodes the closed-form derivative. It is invoked by the surrounding lemmas deriv_Jcost and hasDerivAt_Jcost_pos to equate the analytic derivative with the algebraic expression.
why it matters
The definition is the computational bridge into the costRateEL theorems in Action.EulerLagrange. Those theorems show that the constant path γ ≡ 1 is the unique solution of the cost-rate Euler-Lagrange equation among positive paths, realizing the principle of least action at the J minimum. It thereby supports T5 J-uniqueness and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.