interp_fixedEndpoints
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish that the interpolated path is admissible.
- Does not apply when the input paths fail to share endpoints.
- Does not extend to non-convex or nonlinear combinations.
- Does not address open intervals or non-closed domains.
formal statement (Lean)
151lemma interp_fixedEndpoints {a b : ℝ} {γ₁ γ₂ : AdmissiblePath a b}
152 (h : fixedEndpoints γ₁ γ₂) (s : ℝ) (hs : s ∈ Icc (0:ℝ) 1) :
153 fixedEndpoints γ₁ (interp γ₁ γ₂ s hs) := by
proof body
Term-mode proof.
154 refine ⟨?_, ?_⟩
155 · simp [interp_apply, h.1]; ring
156 · simp [interp_apply, h.2]; ring
157
158/-! ## Status report -/
159
160/-- Status string for the path-space module. -/