actionJ_const_one
plain-language theorem explainer
The lemma shows that the J-action integral vanishes for the constant admissible path valued at 1. Researchers deriving the variational principle from the d'Alembert cost would cite it as the explicit zero baseline. The proof is a direct unfolding of the action definition followed by simplification with the constant-path evaluation rule and the unit vanishing of Jcost.
Claim. Let $a,b$ be real numbers and let $γ$ be the constant admissible path on $[a,b]$ with value 1. Then the action $S[γ] := ∫_a^b J(γ(t)) dt = 0$.
background
The module sets up the variational stage for least action derived from the J-cost functional. An admissible path on $[a,b]$ is a continuous strictly positive real function on the closed interval. The action functional is the integral of Jcost along the path. The constant path at positive value c is the admissible path whose underlying function is constantly c everywhere on the interval.
proof idea
The proof is a one-line wrapper that unfolds the definition of the action functional and applies simplification using the constant-path evaluation lemma together with the fact that Jcost at 1 equals zero.
why it matters
This supplies the zero-action baseline for the variational principle of least action in the Recognition Science setup. It appears in the path-space construction that precedes the strict-convexity arguments of the functional-convexity module and the paper RS_Least_Action.tex. The result confirms that the cost-minimizing constant path at the unit fixed point of J has vanishing action, consistent with the self-similar structure of the J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.