coe_mk
plain-language theorem explainer
The lemma shows that an admissible path constructed from a continuous strictly positive function f on [a,b] recovers f as its underlying map. Researchers developing variational principles from the J-cost functional cite it when unwrapping path data inside integrals or convexity arguments. The proof is a one-line reflexivity on the structure constructor.
Claim. Let $f : [a,b] → ℝ$ be continuous on the closed interval $[a,b]$ and strictly positive there. If $γ$ is the admissible path assembled from the triple consisting of $f$, its continuity proof, and its positivity proof, then the underlying function of $γ$ equals $f$.
background
AdmissiblePath on an interval $[a,b]$ is the structure whose carrier is a function toFun : ℝ → ℝ equipped with a continuity proof on the closed interval Icc a b and a strict-positivity proof on the same interval. The module sets up the variational stage for the principle of least action derived from the d'Alembert cost functional J, recording that admissible paths remain closed under convex interpolation so that strict-convexity arguments proceed without extra positivity hypotheses. The upstream definition of AdmissiblePath supplies the carrier for the J-action functional, defined as the integral of J applied pointwise to the path.
proof idea
The proof is a one-line term that applies reflexivity directly to the structure constructor of AdmissiblePath.
why it matters
The lemma supplies the basic unwrapping property needed to manipulate paths inside the action functional. It supports the least-action development in papers/RS_Least_Action.tex by giving direct access to the path function for integrals and for the convexity arguments that follow from the Recognition Composition Law. It forms the base layer of the PathSpace module that prepares the ground for T5 J-uniqueness and the subsequent forcing chain steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.