fixedEndpoints
plain-language theorem explainer
The fixedEndpoints predicate holds precisely when two admissible paths on a closed interval agree at the boundary points. Variational analysts working on the J-action in Recognition Science cite it to state shared-endpoint conditions in uniqueness and minimality theorems. The definition is a direct conjunction of equalities extracted from the underlying functions of the two paths.
Claim. Let $a,b$ be real numbers and let $γ_1,γ_2$ be admissible paths on the closed interval $[a,b]$. The predicate holds if and only if $γ_1(a)=γ_2(a)$ and $γ_1(b)=γ_2(b)$.
background
An admissible path on $[a,b]$ is a continuous function that is strictly positive on the closed interval, formalized as the structure AdmissiblePath with fields toFun, cont, and pos. The module Action.PathSpace introduces the variational setting for the principle of least action derived from the d'Alembert cost functional J, defining admissible paths, the action integral actionJ, the fixed-endpoints relation, and straight-line interpolation in path space. The key structural fact is that admissible paths remain admissible under convex combinations, which supports the strict-convexity arguments in the companion paper RS_Least_Action.tex.
proof idea
One-line definition that extracts the underlying functions via toFun and asserts equality at the two endpoints.
why it matters
This definition supplies the boundary-condition hypothesis required by the headline results in FunctionalConvexity: actionJ_minimum_unique_value, geodesic_minimizes_unconditional, geodesic_minimizes_via_convexity, and principle_of_least_action. It thereby closes the variational stage that converts the Recognition Composition Law and the J-cost into the unconditional principle of least action. The construction sits inside the T0-T8 forcing chain that derives D=3 and the eight-tick octave from the single functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.