geodesic_minimizes_unconditional
plain-language theorem explainer
A path minimizing the J-action along every convex interpolation segment to a competitor is a global minimizer among all admissible paths sharing endpoints. Recognition Science derivations cite it to obtain the unconditional principle of least action once convexity of the action functional is in hand. The tactic proof specializes the segment hypothesis at s=1 and uses the interpolation definition to identify the endpoint case with the competitor path.
Claim. Let $a,b$ be reals with $a≤b$ and let $γ_{geo},γ_{other}$ be admissible paths on $[a,b]$ that agree at the endpoints. If $S[γ_{geo}]≤S[(1-s)γ_{geo}+sγ_{other}]$ holds for every $s∈[0,1]$, where $S$ denotes the J-action integral, then $S[γ_{geo}]≤S[γ_{other}]$.
background
AdmissiblePath is a continuous strictly positive function on the closed interval. The J-action is the integral of Jcost along the path, the central functional whose critical points are geodesics for the Hessian metric derived from J. fixedEndpoints asserts agreement at the interval endpoints. interp constructs the pointwise convex combination, which stays admissible for $s∈[0,1]$ by the upstream lemma interp_apply. actionJ_convex_on_interp supplies the integrated convexity inequality $S[(1-s)γ_1+sγ_2]≤(1-s)S[γ_1]+sS[γ_2]$, obtained by integrating the pointwise convexity of Jcost that follows from the d'Alembert functional equation.
proof idea
Specialize the universal hypothesis at s=1 using the fact that 1 lies in the unit interval. Apply interp_apply to equate the interpolated path at s=1 with the competitor path pointwise, then rewrite the action integral to obtain equality of the two actions. The desired inequality follows immediately by transitivity.
why it matters
The result supplies the unconditional principle of least action in the Recognition framework, feeding directly into functionalConvexity_status and geodesic_minimizes_via_convexity. It discharges the interpolation-minimality witness previously required by the legacy convex_implies_geodesic_minimizes, leaving only the existence of a critical point as an open hypothesis. The argument rests on convexity of Jcost, itself a theorem of d'Alembert uniqueness, and closes the variational step after J-uniqueness in the T0-T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.