interp_apply
The interp_apply lemma states that the pointwise value of the interpolated path between two admissible paths γ₁ and γ₂ at parameter s equals the convex combination (1-s)γ₁(t) + sγ₂(t). Variational analysts working on the J-action would cite this when verifying that interpolation commutes with evaluation in the path space. The proof is a one-line reflexivity that unfolds the definition of interp.
claimLet γ₁, γ₂ be continuous strictly positive functions on [a, b]. For s ∈ [0, 1] and any real t, the interpolated path satisfies [(1-s)γ₁ + sγ₂](t) = (1-s)γ₁(t) + sγ₂(t).
background
In the PathSpace module the admissible path structure requires a continuous function on the closed interval [a, b] that is strictly positive everywhere on that interval. The interp definition constructs the straight-line interpolation as the pointwise convex combination (1-s)γ₁ + sγ₂ and proves that this combination remains continuous and strictly positive, hence admissible, for every s in [0, 1]. This closure property is the key structural fact recorded in the module that lets the subsequent convexity argument proceed without extra positivity hypotheses.
proof idea
The proof is a one-line term-mode reflexivity that directly matches the toFun field of the interp construction to the explicit linear combination (1-s)·γ₁.toFun + s·γ₂.toFun.
why it matters in Recognition Science
This lemma is invoked by actionJ_convex_on_interp to obtain the pointwise inequality needed for the integrated convexity of the J-action, and by geodesic_minimizes_unconditional to discharge the interpolation-witness hypothesis in the global minimization statement. It therefore sits at the base of the variational stage for the principle of least action derived from the d'Alembert cost functional J, as described in the module companion paper RS_Least_Action.tex.
scope and limits
- Does not prove that the interpolated path remains admissible.
- Does not evaluate or bound the J-action integral.
- Does not address preservation of fixed endpoints.
- Does not extend beyond linear interpolation in path space.
Lean usage
simp [interp_apply]formal statement (Lean)
136@[simp] lemma interp_apply {a b : ℝ} (γ₁ γ₂ : AdmissiblePath a b) (s : ℝ)
137 (hs : s ∈ Icc (0:ℝ) 1) (t : ℝ) :
138 (interp γ₁ γ₂ s hs).toFun t = (1 - s) * γ₁.toFun t + s * γ₂.toFun t := rfl
proof body
Term-mode proof.
139
140/-- Interpolation at `s = 0` is the first path. -/