principle_of_least_action
plain-language theorem explainer
The unconditional principle of least action asserts that an admissible path minimizes the J-action globally if it satisfies a local non-decrease condition along convex interpolations to any competitor path. Researchers deriving variational principles from the Recognition Science functional equation would cite this result. The proof extracts the interpolation witness from the hypothesis and applies the local-to-global minimizer theorem.
Claim. If an admissible path on $[a,b]$ with $a le b$ satisfies that for every admissible competitor sharing endpoints there exists $s_0 in (0,1]$ with $S[gamma_geo] le S[(1-s_0)gamma_geo + s_0 gamma_other]$, then $S[gamma_geo] le S[gamma_other]$ for all such competitors, where $S$ is the J-action functional.
background
The J-action functional is defined as $S[gamma] = int_a^b J(gamma(t)) dt$ on admissible paths, which are continuous strictly positive functions on the closed interval. Convex interpolation between two admissible paths is their pointwise linear combination, which remains admissible by construction. This theorem rests on the upstream local-to-global result whose doc-comment states that if a path is a local minimum of the action in the segment sense then by convexity it is a global minimum versus any competitor.
proof idea
This term-mode proof is a one-line wrapper. It introduces the competitor path and the fixed-endpoint condition, obtains the positive interpolation parameter together with the local inequality from the hypothesis, and applies the local-to-global minimizer theorem to conclude the global inequality.
why it matters
This declaration converts the conditional variational principle into an unconditional statement by replacing the minimality witness with convexity of the action functional, which follows from the d'Alembert functional equation. It supports the headline result that geodesics minimize the action unconditionally among paths with fixed endpoints. The module connects to the variational principle on the cost manifold in the companion paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.