Action Path Space Action J Nonneg

The nonnegative action

The action of a path is a single number that summarizes the whole curve, a staple of classical mechanics since the 1740s. Leonhard Euler and Joseph-Louis Lagrange developed the principle that a moving body follows the path that makes this number, the action, as small as possible. For a path described by a positive function γ(t), the action is the integral of a cost function along the curve, written S[γ] = ∫ J(γ(t)) dt. The cost function measures how expensive it is to be at each value along the way.

In the Recognition Science framework, the cost function takes the specific form J(x) = (x + 1/x)/2 − 1, which is zero when x equals 1 and grows as x moves away from 1 in either direction. The framework's machine-checked library of formal theorems defines an admissible path as a continuous, strictly positive function on a closed interval, and the action of such a path as the integral of J along it. The declaration actionJ_nonneg establishes that this action is always greater than or equal to zero for any admissible path on any interval where the start is not after the end.

The proof is short and direct. Since J(x) is nonnegative for every positive x, and an admissible path is strictly positive everywhere, the integrand J(γ(t)) is nonnegative at every point. The integral of a nonnegative function over an interval is itself nonnegative. The constant path at value 1, where J vanishes identically, has action exactly zero, so the bound is sharp: zero is achieved, not merely approached.

In Recognition Science, this nonnegativity is the foundation for the variational principle that follows. The framework models physical trajectories as paths that minimize this action among admissible paths with fixed endpoints. The fact that the action cannot go negative means the minimization problem is well-posed: there is a floor below which no path can push the action, so seeking a minimum is a meaningful question rather than a chase toward negative infinity.

The declaration does not claim that a minimizing path exists, nor that any particular path is the unique minimizer. It establishes only the lower bound. It also does not claim that all actions are positive; the constant path at 1 has action zero, so the correct statement is nonnegativity, not positivity. The result is a lemma about the integral of a nonnegative function, not a statement about the physical content of the action principle itself.

/-- The action of any admissible path is non-negative. -/
lemma actionJ_nonneg {a b : ℝ} (hab : a ≤ b) (γ : AdmissiblePath a b) :
    0 ≤ actionJ γ := by
  unfold actionJ
  exact intervalIntegral.integral_nonneg hab
    (fun t ht => Jcost_nonneg (γ.pos t ht))

/-- The action of the constant path at `1` (the cost-minimum) vanishes. -/
lemma actionJ_const_one {a b : ℝ} :
    actionJ (AdmissiblePath.const a b 1 one_pos) = 0 := by
  unfold actionJ
  simp [AdmissiblePath.const_apply, Jcost_unit0]

/-- An admissible path on `[a, b]` is a continuous, strictly positive function. -/
structure AdmissiblePath (a b : ℝ) where
  /-- The underlying function. -/
  toFun : ℝ → ℝ
  /-- Continuity on the closed interval. -/
  cont : ContinuousOn toFun (Icc a b)
  /-- Strict positivity on the closed interval. -/
  pos : ∀ t ∈ Icc a b, 0 < toFun t

What this page does not claim

The declaration does not prove that a minimizing path exists. The declaration does not claim the action is always positive, since the constant path at 1 has action zero. The declaration says nothing about the physical interpretation of the action principle.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Action/PathSpace.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: