IndisputableMonolith.Action.FunctionalConvexity
This module lifts the pointwise convexity of Jcost to convexity of the integrated actionJ functional on admissible paths. Researchers deriving the principle of least action or uniqueness of geodesics cite it to guarantee that convex combinations of paths cannot increase total cost. The argument proceeds by direct integration of the Jcost inequality over the interval after importing the convexity lemma from Cost.Convexity.
claimLet $J(x) = ½(x + x^{-1}) - 1$ for $x > 0$. The functional $S[γ] = ∫_a^b J(γ(t)) dt$ on admissible paths satisfies $S[(1-s)γ_1 + s γ_2] ≤ (1-s) S[γ_1] + s S[γ_2]$ for all $s ∈ [0,1]$ and admissible $γ_1, γ_2$.
background
The module sits inside the variational formulation of Recognition Science. PathSpace supplies the objects: admissible paths are continuous strictly positive functions on a closed interval, and actionJ is the integral of J(γ(t)) dt. Cost.Convexity supplies the engine: Jcost(x) = ½(x + x^{-1}) - 1 is strictly convex on ℝ₊ because it is the composition of the strictly convex map t ↦ cosh t - 1 with the logarithm, as required for T5 uniqueness.
proof idea
The module assembles six lemmas. Jcost_convex_combination records the convex-combination inequality for Jcost. actionJ_convex_on_interp integrates that inequality to obtain convexity of S on linear interpolants. geodesic_minimizes_via_convexity and actionJ_local_min_is_global then extract uniqueness and global-minimizer statements. The remaining results close the chain to the principle of least action.
why it matters in Recognition Science
Convexity of actionJ is the direct input to EulerLagrange, where it forces the EL equation to reduce to γ(t) ≡ 1, and to QuadraticLimit, where the small-strain expansion recovers Newtonian kinetics. It realizes the uniqueness half of T5 inside the action setting and supplies the convexity hypothesis needed for the principle of least action.
scope and limits
- Does not treat paths that touch zero or change sign.
- Does not extend to Sobolev or weak topologies.
- Does not derive explicit Euler-Lagrange equations.
- Does not address time-dependent or non-autonomous costs.