interp_fixedEndpoints
plain-language theorem explainer
The lemma establishes that linear interpolation between admissible paths on a closed interval preserves shared endpoints. Workers on the J-action variational problem in Recognition Science cite it to close the space of fixed-endpoint paths under convex combinations. The proof is a direct term-mode verification that applies the interpolation evaluation lemma to each endpoint equality and simplifies with ring.
Claim. Let $a,b$ be reals and let $γ_1,γ_2$ be continuous strictly positive functions on $[a,b]$. If $γ_1(a)=γ_2(a)$ and $γ_1(b)=γ_2(b)$, then for every $s∈[0,1]$ the convex combination $γ_s(t)=(1-s)γ_1(t)+sγ_2(t)$ satisfies $γ_s(a)=γ_1(a)$ and $γ_s(b)=γ_1(b)$.
background
An admissible path on $[a,b]$ is a continuous function that is strictly positive on the closed interval. The predicate fixedEndpoints holds when two such paths agree at the endpoints $a$ and $b$. The operation interp produces the pointwise convex combination $(1-s)γ_1+sγ_2$ for $s∈[0,1]$ and returns another admissible path. The module sets up the variational stage for the principle of least action derived from the d'Alembert cost functional J; the key structural fact is that admissible paths remain closed under convex interpolation, which removes any extra positivity hypothesis from later convexity arguments.
proof idea
The term proof refines the goal to a pair of endpoint equalities. Each equality is discharged by simp using the interp_apply lemma together with the corresponding conjunct of the fixedEndpoints hypothesis, followed by ring normalization.
why it matters
The result guarantees that the fixed-endpoint relation is preserved by the straight-line homotopy in path space. This closure property is invoked in the module documentation to justify the strict-convexity argument of Action.FunctionalConvexity without auxiliary hypotheses. It therefore supplies an essential step toward the least-action principle recorded in papers/RS_Least_Action.tex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.