fixedEndpoints_symm
plain-language theorem explainer
The lemma establishes symmetry of the fixed-endpoints relation on admissible paths. Variational analysts working on least-action principles cite it when symmetrizing boundary conditions for uniqueness arguments. The proof is a direct term-mode construction that swaps the two endpoint equalities.
Claim. Let $a,b$ be real numbers and let $γ_1,γ_2$ be admissible paths on $[a,b]$. If $γ_1(a)=γ_2(a)$ and $γ_1(b)=γ_2(b)$, then $γ_2(a)=γ_1(a)$ and $γ_2(b)=γ_1(b)$.
background
AdmissiblePath a b is the structure whose elements are continuous functions on the closed interval [a,b] that remain strictly positive there. The fixedEndpoints relation is the proposition that two such paths agree at the endpoints a and b. The PathSpace 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-mode wrapper. It takes the hypothesis h, which is the conjunction of the two endpoint equalities, and returns the pair whose components are the symmetric equalities.
why it matters
This lemma feeds the uniqueness theorem actionJ_minimum_unique_value in FunctionalConvexity, which concludes that two action minimizers sharing endpoints must deliver the same action value. It supplies the basic symmetry step required by the least-action variational setup in papers/RS_Least_Action.tex and enables the strict-convexity argument without extra positivity hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.