geodesic_minimizes_via_convexity
plain-language theorem explainer
A candidate path satisfying the non-decrease condition under convex interpolation to any competitor is a global minimizer of the J-action among admissible paths with fixed endpoints. Recognition Science researchers cite this to convert the variational principle into an unconditional statement derived solely from J-cost convexity. The argument reduces to a direct invocation of the unconditional minimizer theorem.
Claim. Let $a ≤ b$. Let $γ_{geo}$ and $γ_{other}$ be admissible paths on $[a,b]$ sharing endpoints. If the J-action of $γ_{geo}$ satisfies $S[γ_{geo}] ≤ S[(1-s)γ_{geo} + s γ_{other}]$ for every $s ∈ [0,1]$, then $S[γ_{geo}] ≤ S[γ_{other}]$, where $S[γ] = ∫_a^b J(γ(t)) dt$.
background
The module establishes convexity properties of the J-action functional $S[γ] = ∫_a^b J(γ(t)) dt$, where $J$ is the Recognition cost function. Admissible paths are continuous strictly positive real-valued functions on the closed interval $[a,b]$. The interpolation operation produces the convex combination $(1-s)γ_1 + s γ_2$, which remains admissible for $s ∈ [0,1]$.
proof idea
The proof is a one-line wrapper that applies the upstream theorem geodesic_minimizes_unconditional to the interval bound, the two paths, the fixed-endpoints hypothesis, and the non-decrease condition along the interpolation segment.
why it matters
This declaration removes the extra interpolation-minimality hypothesis from the legacy variational principle, producing an unconditional statement of the principle of least action. It relies on the convexity of the action functional, which follows from pointwise convexity of Jcost. In the Recognition framework the result advances the derivation of the variational principle from the d'Alembert equation via J-uniqueness (T5) and feeds the principle_of_least_action theorem in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.