actionJ_nonneg
plain-language theorem explainer
The lemma establishes that the J-action integral is non-negative for every admissible path on a closed interval. A researcher deriving the variational principle from the d'Alembert cost in Recognition Science would cite it to bound the functional from below before invoking convexity or existence arguments. The proof is a one-line wrapper that applies the interval-integral non-negativity lemma to the pointwise non-negativity of Jcost on positive reals.
Claim. Let $a,b$ be real numbers with $a≤b$ and let $γ$ be a continuous strictly positive function on the closed interval $[a,b]$. Then $∫_a^b J(γ(t)) dt ≥ 0$, where $J$ denotes the cost function satisfying $J(x)≥0$ for all $x>0$.
background
The PathSpace module sets up the variational stage for the least-action principle derived from the d'Alembert cost functional J. An admissible path on [a,b] is a continuous function that remains strictly positive on the closed interval Icc a b. The action functional is defined as the integral from a to b of Jcost applied to the path value at each t.
proof idea
The proof unfolds the definition of actionJ to the interval integral of Jcost(γ(t)), then applies the Mathlib lemma intervalIntegral.integral_nonneg using the hypothesis a≤b together with the pointwise non-negativity supplied by Jcost_nonneg on the positive values given by γ.pos.
why it matters
This lemma supplies the lower bound required for the variational principle in the Recognition Science framework and supports the development of the least-action principle recorded in papers/RS_Least_Action.tex. It rests on the upstream Jcost_nonneg result (J(x)≥0 for x>0 via AM-GM or square representation) and connects to the J-uniqueness and phi-ladder structures in the forcing chain. No immediate downstream uses are recorded, but the result underpins convexity arguments in related modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.