actionJ_convex_on_interp
plain-language theorem explainer
The convexity theorem for the J-action shows that the functional S[γ] = ∫ J(γ(t)) dt is convex with respect to linear interpolation of admissible paths. Variational analysts in the Recognition Science program cite it to convert local minimality along segments into global minimality. The proof first obtains the pointwise inequality for the integrand from Jcost_convex_combination, then integrates after checking continuity and integrability on the interval.
Claim. Let $a ≤ b$ and let $γ_1, γ_2$ be admissible paths on the interval $[a, b]$. For any $s ∈ [0, 1]$, the action of the interpolated path satisfies $S[(1-s)γ_1 + s γ_2] ≤ (1-s) S[γ_1] + s S[γ_2]$, where $S[γ] := ∫_a^b J(γ(t)) dt$ and $J$ denotes the cost function whose convexity is established pointwise.
background
The J-action functional is defined as the integral of Jcost along an admissible path, where an admissible path is a continuous strictly positive real-valued function on a closed interval. The interpolation operation constructs the convex combination of two such paths, which remains admissible. The upstream lemma Jcost_convex_combination establishes that Jcost itself satisfies the convex combination inequality for positive arguments: Jcost((1-s)x + s y) ≤ (1-s) Jcost x + s Jcost y when s ∈ [0,1] and x,y >0. This module develops the integrated version to support the unconditional variational principle, as described in the module documentation: the deep content is the convexity statement leading to the headline theorem geodesic_minimizes_unconditional.
proof idea
The proof begins by deriving the pointwise bound on the integrand using Jcost_convex_combination after verifying positivity of the paths and applying the interpolation evaluation lemma. It then constructs continuous-on-Icc statements for the three integrands by composing the continuity of Jcost on (0,∞) with the path continuity. Integrability follows from the continuous-on-Icc property. The integral inequality is obtained via intervalIntegral.integral_mono_on, after which the right-hand side integral is expanded by linearity to complete the comparison.
why it matters
This result supplies the convexity needed for the downstream theorems actionJ_local_min_is_global and geodesic_minimizes_unconditional, which together establish the unconditional principle of least action. It discharges the interpolation witness required by earlier conditional versions of the variational principle. In the Recognition framework it closes the gap between pointwise cost convexity and the global minimization property central to the least-action formulation in the companion paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.