fixedEndpoints
plain-language theorem explainer
Two admissible paths on a common interval satisfy the fixedEndpoints relation precisely when their underlying functions agree at both endpoints. Analysts deriving the principle of least action from the J-cost functional cite this predicate to enforce boundary conditions when stating uniqueness or global minimization results. The definition is a direct conjunction of equalities extracted from the toFun fields of the AdmissiblePath structure.
Claim. Let $a,b$ be real numbers with $a≤b$ and let $γ_1,γ_2$ be admissible paths on $[a,b]$. The paths share fixed endpoints when $γ_1(a)=γ_2(a)$ and $γ_1(b)=γ_2(b)$.
background
The PathSpace module sets up the variational stage for the J-action functional. An admissible path on $[a,b]$ is a continuous function that is strictly positive on the closed interval Icc a b. The fixedEndpoints predicate records the shared boundary values required for comparing paths under the least-action principle.
proof idea
This is a direct definition. It projects each path to its underlying function via toFun and asserts equality at the two endpoints. No lemmas or tactics are applied.
why it matters
The predicate supplies the boundary-condition hypothesis in the headline results of FunctionalConvexity, including actionJ_minimum_unique_value, geodesic_minimizes_unconditional, and principle_of_least_action. It fills the role of the fixed-endpoint constraint in the companion paper RS_Least_Action.tex and enables the convexity arguments that derive the principle of least action from the Recognition Science J-cost without extra positivity hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.