interp_one
plain-language theorem explainer
The lemma shows that straight-line interpolation of two admissible paths at parameter value 1 recovers the second path pointwise. Analysts working on the variational formulation of least action from the J-cost would invoke it to confirm endpoint recovery when checking fixed-boundary conditions. The proof is a one-line simplification that unfolds the interpolation definition at s=1.
Claim. Let $a,b$ be real numbers and let $γ_1,γ_2$ be continuous strictly positive functions on the closed interval $[a,b]$. Then for every real $t$, the pointwise value of the convex combination $(1-s)γ_1 + sγ_2$ evaluated at $s=1$ equals $γ_2(t)$.
background
AdmissiblePath is the structure of continuous functions on $[a,b]$ that remain strictly positive throughout the closed interval. The module defines the J-action as the integral of the J-cost along such paths and introduces convex interpolation between any two admissible paths. Interpolation at parameter $s$ is the map sending $t$ to $(1-s)·γ_1(t) + s·γ_2(t)$, which stays admissible for $s$ in the unit interval. The companion paper RS_Least_Action.tex uses this construction to set up the variational stage for the principle of least action derived from the d'Alembert cost functional J.
proof idea
The proof is a one-line wrapper. It introduces the dummy variable t and applies the simplification lemma for the interpolation map, which directly substitutes the convex combination formula at s=1 to obtain the second path.
why it matters
The result closes the interpolation family at the second endpoint, which is required to make the fixed-endpoints relation well-defined and to enable the strict-convexity argument in the action functional. It sits inside the PathSpace module that prepares the variational calculus for the J-action; the module document states that admissible paths remain closed under convex interpolation precisely so that convexity proofs need no extra positivity hypotheses. No downstream uses are recorded yet, but the lemma is a direct prerequisite for any boundary-value verification in the least-action setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.