actionJ_local_min_is_global
plain-language theorem explainer
If an admissible path γ_geo satisfies actionJ γ_geo ≤ actionJ of its convex interpolation toward any competitor γ_other at some positive s0 in (0,1], then γ_geo globally minimizes the action among all admissible paths with the same endpoints. Variational theorists deriving the principle from the d'Alembert equation cite this to remove conditional witnesses. The short tactic proof invokes the integrated convexity lemma on interpolation segments and rearranges via positive-scalar multiplication.
Claim. Let $a ≤ b$ and let $γ, δ$ be continuous strictly positive functions on $[a,b]$. Let $S[·] = ∫_a^b J(·(t)) dt$ be the action functional. For $s_0 ∈ (0,1]$ with $s_0 > 0$, if $S[γ] ≤ S[(1-s_0)γ + s_0 δ]$, then $S[γ] ≤ S[δ]$.
background
The J-action functional is defined as the integral from a to b of Jcost(γ(t)) dt on the space of admissible paths, which are continuous strictly positive real-valued functions on the closed interval [a,b]. The interpolation operation produces the pointwise convex combination (1-s)γ + sδ, which remains admissible for s in [0,1]. This module proves convexity properties of the action by integrating pointwise convexity of Jcost, which itself follows from the d'Alembert functional equation via the Recognition Composition Law.
proof idea
The tactic proof applies actionJ_convex_on_interp to obtain the bound actionJ(interp γ_geo γ_other s0 hs0) ≤ (1-s0) actionJ γ_geo + s0 actionJ γ_other. It combines this with the local-minimality hypothesis via le_trans to reach actionJ γ_geo ≤ (1-s0) actionJ γ_geo + s0 actionJ γ_other. The linarith tactic rearranges to s0 actionJ γ_geo ≤ s0 actionJ γ_other. Finally le_of_mul_le_mul_left divides by the positive scalar s0 to conclude the global comparison.
why it matters
This supplies the core local-to-global implication invoked by the downstream principle_of_least_action, which states the unconditional principle of least action for admissible paths sharing endpoints. It removes the extra h_min witness that previously made the variational principle conditional, relying only on convexity of Jcost proved from J-uniqueness (T5 in the forcing chain). In the Recognition Science framework it advances the variational principle on the cost manifold, connecting the J-functional to the self-similar fixed point phi and the eight-tick octave. It closes a conditional gap but touches no open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.