AdmissiblePath
plain-language theorem explainer
Admissible paths on a closed real interval [a,b] are continuous strictly positive functions. Variational analysts working on the J-action in Recognition Science cite this type as the domain for the least-action principle. The declaration is introduced as a structure with three fields encoding the function, its continuity, and its positivity.
Claim. Let $a,b$ be real numbers. An admissible path on the closed interval $[a,b]$ is a function $f:ℝ→ℝ$ that is continuous on $[a,b]$ and satisfies $f(t)>0$ for all $t∈[a,b]$.
background
The module sets up the variational stage for the principle of least action derived from the d'Alembert cost functional J. It defines admissible paths, the J-action as the integral of J(γ(t)) dt, fixed-endpoint relations, and straight-line interpolation in path space. The crucial structural fact is that admissible paths remain admissible under convex interpolation, which enables the strict-convexity arguments in FunctionalConvexity without extra positivity hypotheses. The upstream interval definition supplies the spacetime interval for a displacement vector but is not invoked in the path-space structure itself.
proof idea
This is a structure definition that packages the underlying function together with its continuity and strict-positivity conditions on the closed interval.
why it matters
AdmissiblePath supplies the domain for actionJ and is referenced by every convexity and minimization result in FunctionalConvexity, including actionJ_convex_on_interp, geodesic_minimizes_unconditional, and principle_of_least_action. It therefore occupies the path-space slot in the derivation of the unconditional least-action principle recorded in papers/RS_Least_Action.tex. The construction directly supports the Recognition Composition Law and the J-uniqueness step of the forcing chain by guaranteeing that the interpolation segment stays inside the admissible set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.