actionJ
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.
claimLet γ 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 in Recognition Science
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.
scope and limits
- Does not establish existence or uniqueness of minimizers.
- Does not specify the explicit form of the J-cost function.
- Does not impose fixed-endpoint conditions on the path.
- Does not compute variations or Euler-Lagrange equations.
formal statement (Lean)
69noncomputable def actionJ {a b : ℝ} (γ : AdmissiblePath a b) : ℝ :=
proof body
Definition body.
70 ∫ t in a..b, Jcost (γ.toFun t)
71