interp
plain-language theorem explainer
The interp definition supplies the convex combination of any two admissible paths γ₁, γ₂ on [a,b] at parameter s ∈ [0,1], returning another admissible path. Researchers deriving the principle of least action from the J-cost functional cite this closure property to justify convexity arguments in path space. Construction proceeds by pointwise linear interpolation followed by direct verification that the result remains continuous and strictly positive.
Claim. For admissible paths $γ_1, γ_2$ on the interval $[a,b]$ and $s ∈ [0,1]$, define the interpolated path by $t ↦ (1-s) γ_1(t) + s γ_2(t)$. This map is continuous on $[a,b]$ and strictly positive there, hence admissible.
background
AdmissiblePath a b is the structure consisting of a function toFun : ℝ → ℝ together with witnesses cont : ContinuousOn toFun (Icc a b) and pos : ∀ t ∈ Icc a b, 0 < toFun t. This module sets up the variational stage for the principle of least action derived from the d'Alembert cost functional J. It defines admissible paths, the actionJ integral, fixed endpoints, and the interpolation operation. The key structural fact recorded here is that admissible paths are closed under convex interpolation: if γ₁ and γ₂ are positive on [a,b], so is any (1-s) γ₁ + s γ₂ with s ∈ [0,1]. This is what enables the strict-convexity argument of Action.FunctionalConvexity to work without any extra positivity hypothesis.
proof idea
The definition constructs the new AdmissiblePath by setting toFun to the linear combination (1-s) γ₁.toFun + s γ₂.toFun. Continuity is obtained by scaling each input's continuous witness and adding the results. Strict positivity proceeds by cases on s: when s > 0 the second term is strictly positive while the first is nonnegative; when s = 0 the combination reduces to γ₁.
why it matters
This definition supplies the interpolation map required by the convexity theorems in Action.FunctionalConvexity, including actionJ_convex_on_interp which bounds the action of the combination, actionJ_local_min_is_global, and the unconditional principle_of_least_action. It fills the structural prerequisite for the variational calculus in the Recognition Science derivation of least action, as noted in the module's companion paper RS_Least_Action.tex. The closure property directly supports the eight-tick octave and J-uniqueness steps in the forcing chain by keeping the path space convex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.