fixedEndpoints_trans
plain-language theorem explainer
Transitivity of the fixed-endpoints relation on admissible paths. Researchers deriving the least-action principle from the J-cost functional cite it when chaining boundary conditions across sequences of paths. The proof is a one-line term-mode construction that applies equality transitivity to the pair of endpoint conditions.
Claim. Let $a,b$ be real numbers and let $γ_1,γ_2,γ_3$ be admissible paths on the closed interval $[a,b]$, i.e., continuous and strictly positive functions on $[a,b]$. If $γ_1(a)=γ_2(a)$ and $γ_1(b)=γ_2(b)$, and likewise $γ_2(a)=γ_3(a)$ and $γ_2(b)=γ_3(b)$, then $γ_1(a)=γ_3(a)$ and $γ_1(b)=γ_3(b)$.
background
AdmissiblePath a b is the structure whose fields are a function toFun : R → R together with proofs that it is continuous on Icc a b and strictly positive there. fixedEndpoints γ1 γ2 is the proposition γ1.toFun a = γ2.toFun a ∧ γ1.toFun b = γ2.toFun b. The module sets up the variational stage for the principle of least action derived from the d'Alembert cost functional J, with paper companion papers/RS_Least_Action.tex. The key structural fact recorded here is that admissible paths remain admissible under convex interpolation.
proof idea
The proof is a term-mode construction that builds the required pair by applying transitivity of equality to the two components of the hypotheses: the a-endpoint equality via h1.1.trans h2.1 and the b-endpoint equality via h1.2.trans h2.2.
why it matters
This lemma completes the equivalence-relation structure on fixedEndpoints (with the reflexivity and symmetry siblings in the same module). It supports the strict-convexity argument of Action.FunctionalConvexity by allowing consistent boundary conditions across interpolated paths. The module records that admissible paths remain admissible under convex combinations, which is what enables the J-action functional to be well-defined on path space without extra positivity hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.