interp_apply
plain-language theorem explainer
The lemma records that the interpolated path between two admissible paths evaluates pointwise to the convex combination with weights (1-s) and s. Variational analysts deriving least-action principles from the J-cost would cite this when verifying that the action functional commutes with linear interpolations in path space. The proof is immediate by reflexivity on the definition of the interpolation operator.
Claim. Let $a,b$ be reals with $a<b$, let $γ_1,γ_2$ be continuous strictly positive functions on $[a,b]$, and let $s∈[0,1]$. For the interpolated path $γ$ defined by $γ(t)=(1-s)γ_1(t)+sγ_2(t)$, the evaluation identity $γ(t)=(1-s)γ_1(t)+sγ_2(t)$ holds for every $t$.
background
The PathSpace module equips the variational setting for the J-action principle. It defines admissible paths as continuous strictly positive real-valued functions on a closed interval, the action functional as the integral of the J-cost, and the interpolation operator that produces the straight-line combination between two such paths while preserving admissibility. The local setting is the convex structure of path space needed for the strict-convexity argument in the companion FunctionalConvexity module. The upstream definition of admissible paths supplies the continuity and positivity hypotheses, while the interp construction explicitly builds the convex combination of the underlying functions.
proof idea
The proof is a one-line term proof that applies reflexivity to the definition of interp, confirming that the toFun component of the resulting admissible path is exactly the stated linear combination.
why it matters
This supplies the explicit evaluation rule required to establish pointwise convexity of the integrand in the actionJ_convex_on_interp theorem, which in turn discharges the interpolation witness for the unconditional geodesic minimization result. It forms part of the structural setup that lets the Recognition Science J-cost induce a convex variational problem without extra positivity hypotheses. The parent theorems are actionJ_convex_on_interp and geodesic_minimizes_unconditional; the module doc flags this convexity preservation as the key fact enabling the least-action derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.