Jcost_convex_combination
plain-language theorem explainer
The lemma establishes pointwise convexity of the J-cost function on positive reals: convex combinations of arguments yield a cost no larger than the same combination of costs. Researchers deriving the unconditional principle of least action from Recognition Science axioms cite it to pass from pointwise cost properties to the integrated action functional. The proof extracts the ConvexOn predicate from the upstream strict-convexity theorem, verifies the weights sum to one and are nonnegative, and applies the convexity definition with a final sima
Claim. For $s$ in the closed interval $[0,1]$, and for $x>0$, $y>0$, $Jcost((1-s)x + s y) ≤ (1-s) Jcost(x) + s Jcost(y)$.
background
The Action.FunctionalConvexity module develops convexity properties of the J-action $S[γ] = ∫ Jcost(γ(t)) dt$ on admissible paths. Jcost is the cost function obtained from the d'Alembert ledger factorization and the phi-forcing structures; its explicit form satisfies the Recognition Composition Law. The upstream result Jcost_strictConvexOn_pos states that Jcost is strictly convex on the open interval (0,∞), which immediately supplies ordinary convexity on the same domain.
proof idea
The tactic proof first obtains ConvexOn ℝ (Ioi 0) Jcost by applying .convexOn to the strict-convexity theorem. It then uses ring to confirm the weights sum to 1, linarith to confirm nonnegativity from the Icc hypothesis, and places the arguments in Ioi 0. The convexity definition is applied directly and the smul notation is rewritten to ordinary multiplication via simpa.
why it matters
This pointwise inequality is the engine for the sibling theorem actionJ_convex_on_interp, which integrates the cost convexity to obtain convexity of the full action functional. That result in turn discharges the extra hypothesis that previously made the variational principle conditional, yielding the unconditional geodesic-minimization statement. The module documentation identifies the companion paper RS_Least_Action.tex, Section on the Variational Principle on the Cost Manifold, as the place where this step closes the argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.