actionJ
plain-language theorem explainer
The J-action functional integrates the J-cost along any admissible path γ on [a, b]. Researchers working on the Recognition Science variational principle cite it as the central object whose minimizers are geodesics of the Hessian metric g(x) = 1/x³. The definition is a direct integral of Jcost composed with the path's underlying function.
Claim. Let γ be an admissible path on the interval [a, b]. The J-action of γ is ∫_a^b J(γ(t)) dt, where J denotes the J-cost function.
background
The module sets up the variational stage for the principle of least action derived from the d'Alembert cost functional J. An admissible path on [a, b] is a continuous, strictly positive function on the closed interval Icc a b. This positivity ensures paths remain in the domain where J and its derivatives are defined.
proof idea
This is a direct definition that sets actionJ γ to the integral from a to b of Jcost applied to γ.toFun t.
why it matters
This definition supplies the objective functional for the convexity and minimization theorems in Action.FunctionalConvexity, including actionJ_convex_on_interp, geodesic_minimizes_unconditional, and principle_of_least_action. It realizes the central variational object whose minimizers are geodesics of g(x) = J''(x) = 1/x³, consistent with the forcing chain and the companion paper RS_Least_Action.tex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.