const_apply
plain-language theorem explainer
The constant admissible path evaluates to its fixed value at every point. Researchers working on the J-action variational principle cite this to simplify integrals over constant paths. The proof is a one-line reflexivity on the definition of the constant path constructor.
Claim. Let $a,b,c$ be reals with $c>0$ and let $t$ be real. Let $γ$ be the constant admissible path on $[a,b]$ with value $c$. Then $γ(t)=c$.
background
AdmissiblePath a b is the structure of a continuous function toFun : ℝ → ℝ that is strictly positive on the closed interval Icc a b. The constant path constructor builds such a path by setting toFun to the constant function with value c, using continuousOn_const for continuity and the positivity hypothesis for the strict inequality on the interval.
proof idea
One-line wrapper that applies reflexivity to the definition of the constant path constructor.
why it matters
This lemma is used by actionJ_const_one to show that the J-action of the constant path at 1 vanishes. It supports the central object of the variational principle, the J-action functional S[γ] = ∫_a^b J(γ(t)) dt, which is minimized by geodesics of the Hessian metric g(x) = J''(x) = 1/x³. It supplies the structural simplification needed for the least action principle in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.