interp_fixedEndpoints
plain-language theorem explainer
Interpolation between admissible paths preserves shared endpoints. Researchers deriving the least-action principle from the J-cost functional would cite this to close the path-space convexity argument. The proof is a direct algebraic verification that applies the interpolation evaluation lemma at the endpoints and simplifies using the shared-endpoint hypothesis.
Claim. Let $a,b$ be reals and let $γ_1,γ_2$ be continuous strictly positive functions on the closed interval $[a,b]$ such that $γ_1(a)=γ_2(a)$ and $γ_1(b)=γ_2(b)$. For any $s∈[0,1]$, the interpolated path $γ(t)=(1-s)γ_1(t)+sγ_2(t)$ satisfies $γ(a)=γ_1(a)$ and $γ(b)=γ_1(b)$.
background
AdmissiblePath a b is the structure of a continuous function on the closed interval [a,b] that is strictly positive at every point of that interval. The fixedEndpoints relation is the proposition that two such paths agree at the left and right endpoints. The interp operation returns the straight-line path-space interpolation (1-s)γ₁ + sγ₂ for parameter s in [0,1], which remains admissible by construction of the module.
proof idea
The proof is a term-mode verification that refines the goal into the pair of endpoint equalities. It invokes the interp_apply lemma to expand the interpolated path at a and at b, then substitutes the two components of the shared-endpoint hypothesis and reduces each linear combination with the ring tactic.
why it matters
This lemma supplies the structural fact that the fixed-endpoint constraint is preserved under convex interpolation, which is required for the strict-convexity argument of Action.FunctionalConvexity. It therefore supports the variational derivation of the least-action principle from the J-cost functional in the Recognition Science framework and closes a prerequisite recorded in the PathSpace module for the companion paper RS_Least_Action.tex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.