actionJ_nonneg
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish that the action attains its infimum on the path space.
- Does not depend on the explicit algebraic form of J beyond non-negativity for positive arguments.
- Does not address paths that fail to be strictly positive on the closed interval.
- Does not provide information about the value of the action for specific paths such as constants.
formal statement (Lean)
76lemma actionJ_nonneg {a b : ℝ} (hab : a ≤ b) (γ : AdmissiblePath a b) :
77 0 ≤ actionJ γ := by
proof body
Term-mode proof.
78 unfold actionJ
79 exact intervalIntegral.integral_nonneg hab
80 (fun t ht => Jcost_nonneg (γ.pos t ht))
81
82/-- The action of the constant path at `1` (the cost-minimum) vanishes. -/