interp_zero
The lemma shows that straight-line interpolation of two admissible paths at s=0 recovers the first path pointwise. Researchers deriving the least-action principle from the J-cost functional cite it to fix boundary conditions in path space. The proof is a one-line wrapper that applies the interpolation evaluation lemma and simplification.
claimLet $a,b$ be reals and let $γ_1,γ_2$ be continuous strictly positive functions on the closed interval $[a,b]$. For the convex combination path defined by $(1-s)γ_1(t)+sγ_2(t)$ at $s=0$, the resulting function equals $γ_1(t)$ for every $t$ in $[a,b]$.
background
AdmissiblePath a b is the structure whose toFun component is a continuous map from the closed interval Icc a b to R that is strictly positive at every point of that interval. The interpolation operator interp γ1 γ2 s produces the convex combination (1-s)·γ1 + s·γ2; its defining property is recorded in the sibling lemma interp_apply, which states that the toFun of the result is exactly that linear combination. The module sets up the variational stage for the principle of least action derived from the d'Alembert cost functional J, with the key structural fact that admissible paths remain admissible under convex interpolation for s in [0,1].
proof idea
The proof introduces the dummy variable t and invokes simplification on the lemma interp_apply. Because interp_apply states that the toFun of interp γ1 γ2 s hs is exactly (1-s)γ1.toFun + sγ2.toFun, the case s=0 collapses directly to γ1.toFun t.
why it matters in Recognition Science
The lemma supplies the endpoint boundary condition for the interpolation operator used throughout the path-space construction of the J-action. It therefore supports the strict-convexity argument in the companion paper RS_Least_Action.tex by guaranteeing that the interpolated paths remain admissible without extra positivity hypotheses. In the Recognition framework it closes one of the elementary identities needed before the action functional can be shown to attain its minimum on fixed-endpoint classes.
scope and limits
- Does not compute the value of the J-action on any interpolated path.
- Does not prove that the interpolated path is admissible.
- Does not extend to non-linear interpolations or higher-dimensional domains.
formal statement (Lean)
141lemma interp_zero {a b : ℝ} (γ₁ γ₂ : AdmissiblePath a b) :
142 ∀ t, (interp γ₁ γ₂ 0 ⟨le_refl 0, by norm_num⟩).toFun t = γ₁.toFun t := by
proof body
Term-mode proof.
143 intro t; simp [interp_apply]
144
145/-- Interpolation at `s = 1` is the second path. -/