fixedEndpoints_trans
plain-language theorem explainer
The lemma shows that the fixed-endpoints relation on admissible paths is transitive. Variational analysts working with the J-action in Recognition Science would cite it when chaining paths that preserve boundary values. The proof is a one-line term that applies transitivity of equality componentwise to the two endpoint pairs.
Claim. Let $a,b$ be reals and let $γ_1,γ_2,γ_3$ be admissible paths on $[a,b]$. If $γ_1$ and $γ_2$ agree at the endpoints $a$ and $b$, and $γ_2$ and $γ_3$ agree at those same points, then $γ_1$ and $γ_3$ agree at $a$ and $b$.
background
AdmissiblePath $a$ $b$ is the structure whose carrier is a continuous function on the closed interval $[a,b]$ that is strictly positive at every point of that interval. fixedEndpoints $γ_1$ $γ_2$ is the proposition that the underlying functions of $γ_1$ and $γ_2$ take the same value at $a$ and the same value at $b$ (the two components of the defining pair). 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 admissible under convex interpolation.
proof idea
The proof is a one-line term that builds the required pair by applying transitivity of equality to the first components of the two hypotheses and separately to the second components.
why it matters
The lemma supplies the transitivity leg of the equivalence relation on path space that is required for the least-action variational argument in the Recognition Science framework. It belongs to the module whose paper companion is papers/RS_Least_Action.tex and is a prerequisite for the strict-convexity results that rely on the closure of admissible paths under interpolation. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.