actionJ_def
plain-language theorem explainer
The lemma equates the J-action of an admissible path γ on [a,b] to the integral from a to b of Jcost evaluated at γ(t). Variational analysts working on least-action principles derived from the d'Alembert ledger cite this when converting abstract path functionals into explicit integrals for convexity arguments. The proof is a one-line reflexivity that unfolds the definition of actionJ.
Claim. For an admissible path $γ$ on the closed interval $[a,b]$, the action equals $S[γ] = ∫_a^b J(γ(t)) dt$.
background
AdmissiblePath is the structure of continuous, strictly positive functions toFun : ℝ → ℝ on Icc a b. The J-action functional is defined upstream as the integral ∫_a^b Jcost(γ.toFun t) dt, where Jcost is the Recognition Science cost calibrated from the d'Alembert ledger factorization. This module establishes the variational stage for the principle of least action, with the key structural fact that admissible paths remain closed under convex interpolation, enabling strict-convexity results without extra positivity hypotheses. The paper companion is papers/RS_Least_Action.tex.
proof idea
The proof is a one-line wrapper that applies reflexivity to match the definition of actionJ as the integral of Jcost along the path.
why it matters
This supplies the explicit integral representation of the J-action, the central object of the variational principle. It supports downstream convexity and minimization arguments in the Action module. Within Recognition Science it realizes the T5 J-uniqueness and ledger factorization as a concrete path integral, with the Hessian metric g(x) = 1/x³ entering the geodesic minimization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.