interp
plain-language theorem explainer
The interp definition supplies the convex combination of any two admissible paths on a shared interval, weighted by s in the closed unit interval, and confirms the result remains admissible. Variational analysts working on the J-action in Recognition Science cite this to enable convexity arguments for the integrated functional. The construction substitutes the linear combination into the path structure and verifies continuity plus strict positivity via scaled sums and case analysis on the weight.
Claim. Let $a,b$ be reals with $a≤b$, let $γ_1,γ_2$ be admissible paths on $[a,b]$, and let $s∈[0,1]$. The interpolated path $γ$ is defined pointwise by $γ(t):=(1-s)γ_1(t)+sγ_2(t)$ for $t∈[a,b]$. Then $γ$ is continuous and strictly positive on $[a,b]$, hence admissible.
background
The PathSpace module defines admissible paths as continuous strictly positive functions on a closed interval $[a,b]$, the J-action as the integral of J-cost along such a path, and the fixed-endpoints relation. The module records that admissible paths are closed under convex combinations; this fact is stated explicitly to support the convexity proofs that follow in FunctionalConvexity. Upstream, the admissible-path structure supplies the continuity and positivity fields that any interpolation must preserve, as quoted in the module documentation: admissible paths are continuous, strictly positive functions.
proof idea
The definition installs the pointwise linear combination as the underlying function. Continuity of the result is obtained by scaling each input path by a constant (via const_smul) and adding the results. Positivity proceeds by case distinction on whether the weight is zero or positive, applying multiplication rules for positive and nonnegative reals together with linear arithmetic to conclude strict inequality.
why it matters
This definition is invoked directly by actionJ_convex_on_interp, actionJ_local_min_is_global, geodesic_minimizes_unconditional, and principle_of_least_action in FunctionalConvexity. It supplies the interpolation segment that converts pointwise convexity of J-cost into convexity of the integrated action, discharging the witness required by the unconditional least-action statements. In the Recognition framework it closes the structural requirement that lets the variational stage inherit convexity from the core J functional equation without extra positivity hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.