IndisputableMonolith.Action.FunctionalConvexity
The module lifts pointwise convexity of Jcost to convexity of the integrated actionJ functional on admissible paths. Variational analysts in the Recognition framework cite it to secure uniqueness of action minimizers before deriving Euler-Lagrange equations. The argument combines the strict convexity theorem from Cost.Convexity with integration over PathSpace, yielding the functional inequality that underpins geodesic minimization.
claimFor admissible paths $\gamma_1,\gamma_2$ on $[a,b]$ and $s\in[0,1]$, $\int_a^b J\big((1-s)\gamma_1(t)+s\gamma_2(t)\big)\,dt\le(1-s)\int_a^b J(\gamma_1(t))\,dt+s\int_a^b J(\gamma_2(t))\,dt$, where $J(x)=\frac12(x+x^{-1})-1$.
background
The module belongs to the Action domain and imports PathSpace, which defines AdmissiblePath as continuous strictly positive functions on a closed interval together with the action functional actionJ $\gamma=\int J(\gamma(t)),dt$. It also imports Cost.Convexity, whose doc-comment states that Jlog$(t)=\cosh t-1$ is strictly convex on $\mathbb R$ and Jcost$(x)=\frac12(x+x^{-1})-1$ is strictly convex on $\mathbb R_+$; these facts are foundational for T5 J-uniqueness.
The supplied DOC_COMMENT identifies the pointwise convexity of Jcost as the engine that produces convexity of actionJ. The module therefore assembles the bridge between the algebraic convexity of J and the variational properties required for the principle of least action.
proof idea
This module collects the convexity lemmas rather than a single proof. Its structure proceeds by first establishing the pointwise convex combination for Jcost, then integrating term-by-term over the interval to obtain the corresponding inequality for actionJ, and finally applying the result to show that geodesics minimize the action unconditionally and locally.
why it matters in Recognition Science
The module supplies the convexity engine required by the downstream EulerLagrange module, whose doc-comment reduces the EL equation to $\gamma(t)\equiv1$, and by QuadraticLimit, which recovers Newton's second law in the small-strain regime. It directly supports the principle of least action and closes the link from T5 J-uniqueness to the eight-tick octave and spatial dimension D=3.
scope and limits
- Does not establish existence of minimizers without compactness on the path space.
- Does not treat paths that change sign or vanish.
- Does not incorporate velocity dependence into the action functional.
- Does not derive the explicit form of the Euler-Lagrange equation.