Jcost_quadratic_leading_coeff
plain-language theorem explainer
The second derivative of the J-cost function at unity equals one. Researchers deriving classical mechanics from the Recognition Science cost functional cite this to fix the quadratic coefficient in the small-strain expansion of the action. The proof is a direct one-line reference to the second-derivative result in the Cost.Convexity module.
Claim. $J''(1) = 1$, where $J(x) = ½(x + x^{-1}) - 1$.
background
The J-cost is given by $J(γ) = ½(γ + γ^{-1}) - 1$. In the Action.QuadraticLimit module the small-strain regime is introduced by the substitution $γ = 1 + ε$ with $|ε| ≪ 1$. Under this substitution the J-action reduces to the standard kinetic action $½ ∫ ε² dt$ as stated in the module document.
proof idea
The proof is a one-line wrapper that applies the theorem deriv2_Jcost_one from Cost.Convexity.
why it matters
The declaration supplies the Hessian value used by newtonSecondLawCert in Action.NewtonSecondLawDomainCert. It fills the local quadratic approximation step in the derivation of Newton's second law as a corollary of the J-action, as outlined in the paper companion RS_Least_Action.tex Section Newton's Second Law as a Corollary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.