Jcost_quadratic_leading_coeff
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 in Recognition Science
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.
scope and limits
- Does not establish the remainder bound in the Taylor series.
- Does not extend to finite strains beyond the infinitesimal regime.
- Does not derive the full action functional without the surrounding module results.
Lean usage
def newtonSecondLawCert : NewtonSecondLawCert where el_iff_newton := QuadraticLimit.newton_second_law quadratic_taylor_bound := Jcost_taylor_quadratic hessian_one := Jcost_quadratic_leading_coeffformal statement (Lean)
53theorem Jcost_quadratic_leading_coeff :
54 deriv (deriv Jcost) 1 = 1 :=
proof body
Term-mode proof.
55 IndisputableMonolith.Cost.deriv2_Jcost_one
56
57/-! ## The kinetic action -/
58
59/-- The standard kinetic action `T[ε] = (1/2) ∫_a^b ε(t)² dt`, viewed as
60 the small-strain limit of the J-action via the substitution
61 `γ = 1 + ε`. -/