Action Path Space

The variational stage

In classical mechanics, the principle of least action states that a system moves along the path that minimizes a certain quantity, the action. Action path space is the set of all candidate paths a system could take between two fixed endpoints. In Recognition Science, this space is built from continuous, strictly positive functions on a time interval. These are the admissible paths: they never touch zero, which keeps the cost function well-defined at every instant.

The framework defines a functional called the J-action, written S[γ] = ∫ J(γ(t)) dt. Here J is the cost function from Recognition Science, and the integral adds up that cost along the whole path. The constant path at value 1, where the cost is zero, has vanishing action. Every other admissible path has non-negative action. This sets up a variational problem: among all paths with fixed endpoints, which one minimizes the J-action? The answer is a geodesic of the metric g(x) = 1/x³, which is the second derivative of J.

The key structural result is that admissible paths are closed under convex interpolation. If γ₁ and γ₂ are two admissible paths, then for any s between 0 and 1, the straight-line combination (1-s)γ₁ + sγ₂ is also admissible. This matters because it lets the strict-convexity argument for the functional work without extra hypotheses. The interpolation also preserves shared endpoints, so the whole space of paths with fixed endpoints is convex.

In Recognition Science, this path space is the stage on which the principle of least action is derived from the cost function J. The framework's library proves that the J-action is non-negative and that the constant path at the cost minimum has zero action. These are the first steps toward showing that the geodesics of this metric are the physically realized paths. The module itself is a foundation: it defines the objects and proves the convexity that later arguments rely on.

@[simp] lemma actionJ_def {a b : ℝ} (γ : AdmissiblePath a b) :
    actionJ γ = ∫ t in a..b, Jcost (γ.toFun t) := rfl

/-- 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]

/-- The straight-line interpolation between two admissible paths.

    `interp γ₁ γ₂ s = (1 - s) · γ₁ + s · γ₂`.

    The key structural fact is that for `s ∈ [0,1]`, this convex combination
    is again strictly positive and continuous, hence again admissible. -/
def interp {a b : ℝ} (γ₁ γ₂ : AdmissiblePath a b) (s : ℝ)
    (hs : s ∈ Icc (0:ℝ) 1) : AdmissiblePath a b where
  toFun := fun t => (1 - s) * γ₁.toFun t + s * γ₂.toFun t
  cont := by
    have h1 : ContinuousOn (fun t => (1 - s) * γ₁.toFun t) (Icc a b) :=
      γ₁.cont.const_smul (1 - s) |>.congr (fun _ _ => by simp [smul_eq_mul])
    have h2 : ContinuousOn (fun t => s * γ₂.toFun t) (Icc a b) :=
      γ₂.cont.const_smul s |>.congr (fun _ _ => by simp [smul_eq_mul])
    exact h1.add h2
  pos := by
    intro t ht
    have h1s : 0 ≤ 1 - s := by linarith [hs.2]
    have hs' : 0 ≤ s := hs.1
    have hp1 : 0 < γ₁.toFun t := γ₁.pos t ht
    have hp2 : 0 < γ₂.toFun t := γ₂.pos t ht
    -- Either s = 0 (LHS pure γ₁), or s > 0 (RHS strictly positive). Either way > 0.
    rcases lt_or_eq_of_le hs' with hs_pos | hs_zero
    · have := mul_pos hs_pos hp2
      have hnn : 0 ≤ (1 - s) * γ₁.toFun t := mul_nonneg h1s hp1.le
      linarith
    · -- s = 0: the combination is 1 · γ₁ + 0 · γ₂ = γ₁
      simp [← hs_zero, hp1]

/-- Interpolation preserves shared endpoints. -/
lemma interp_fixedEndpoints {a b : ℝ} {γ₁ γ₂ : AdmissiblePath a b}
    (h : fixedEndpoints γ₁ γ₂) (s : ℝ) (hs : s ∈ Icc (0:ℝ) 1) :
    fixedEndpoints γ₁ (interp γ₁ γ₂ s hs) := by
  refine ⟨?_, ?_⟩
  · simp [interp_apply, h.1]; ring
  · simp [interp_apply, h.2]; ring

What this page does not claim

This module does not prove that a minimizing path exists or is unique. This module does not derive the Euler-Lagrange equations for the J-action. This module does not connect the J-action to any specific physical system or force law.

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: