Encyclopedia Action Action Functional Convexity Principle Of Least Action

ARTICLE 4 claims 4 theorems

Action Functional Convexity Principle Of Least Action

A path that beats every neighbor in a straight-line test is a global minimum: convexity turns a local check into a universal guarantee.

Verify this page

The Principle of Least Action

The principle of least action is a classical idea in physics: among all the ways a system could move from one configuration to another, the one it actually takes is the one that minimizes a quantity called the action. The action is not a force or an energy; it is a bookkeeping total, an integral over time of a function of the system's state. In the standard account, the principle is an axiom, a rule imposed on nature because it works. The Recognition Science framework, a research program that derives physical structure from a single cost function, treats the principle differently: its machine-checked library of formal theorems proves a version of it, rather than assuming it.

The framework begins with a cost, a function J(x) that measures the price of a recognition event, a discrete record of a comparison. The cost function is forced by five plain conditions, and its uniqueness is a proved theorem. From that cost, the framework builds an action functional, written S[γ] = ∫ J(γ(t)) dt, which integrates the cost along a path. The central technical fact is that this action is convex: the action of a weighted average of two paths is no larger than the weighted average of their actions. Convexity is the mathematical property that makes local checks global: if a function is convex, a point that does not increase the function in any direction is automatically a global minimum.

The headline theorem, named principle_of_least_action, states it precisely. If a path γ_geo has the property that, for every competitor γ_other sharing its endpoints, there is at least one positive step along the straight-line interpolation in path space where γ_geo does not increase the action, then γ_geo minimizes the action globally among all admissible competitors. The proof is short once convexity is in hand: the local non-increase at one step, combined with the convexity inequality, forces the global inequality at the endpoint. The framework's library also proves that any two global minimizers with the same endpoints must have the same action value, a uniqueness statement for the minimum itself.

What the declaration does not claim is as important as what it proves. It does not assert that such a minimizing path exists for every pair of endpoints; the theorem is conditional on the path being given. It does not identify the minimizing path with any particular physical trajectory, such as a geodesic in spacetime. It does not say that the action functional is the only one, or that the framework's J-cost is the unique possible integrand. The theorem is a structural implication: if a path passes the local test, then it is globally minimal. The existence of the path, and its physical interpretation, remain separate questions.

The consequence is a shift in what the principle of least action is. In the framework's account, it is not a separate physical law but a corollary of the convexity of a cost function, which is itself a corollary of the uniqueness of that cost. The principle becomes a theorem about the structure of the framework's mathematics, not an independent postulate about nature. A reader who wants the classical principle as a physical axiom can keep it; the framework's contribution is to show that a version of it follows from a deeper, forced structure.

THEOREM principle_of_least_action · IndisputableMonolith/Action/FunctionalConvexity.lean
principle_of_least_action · IndisputableMonolith/Action/FunctionalConvexity.lean:288 
/-- **The principle of least action, unconditionally.**

    If `γ_geo` does not decrease the action on the way to *any* competitor
    `γ_other` (along the straight-line interpolation in path space, at
    even one positive step), then `γ_geo` minimizes the action globally
    among all admissible competitors with the same endpoints.

    This is the clean unconditional version, with no extra
    interpolation-minimality witness. The witness is *replaced* by
    convexity, which is *proved* from the d'Alembert functional equation. -/
theorem principle_of_least_action (hab : a ≤ b)
    (γ_geo : AdmissiblePath a b)
    (h_no_local_decrease :
      ∀ γ_other : AdmissiblePath a b,
        fixedEndpoints γ_geo γ_other →
        ∃ (s₀ : ℝ) (hs₀ : s₀ ∈ Icc (0:ℝ) 1),
          0 < s₀ ∧ actionJ γ_geo ≤ actionJ (interp γ_geo γ_other s₀ hs₀)) :
    ∀ γ_other : AdmissiblePath a b,
      fixedEndpoints γ_geo γ_other → actionJ γ_geo ≤ actionJ γ_other := by
  intro γ_other h_end
  obtain ⟨s₀, hs₀, hs₀_pos, h_local⟩ := h_no_local_decrease γ_other h_end
  exact actionJ_local_min_is_global hab γ_geo γ_other s₀ hs₀ hs₀_pos h_local
THEOREM actionJ_convex_on_interp · IndisputableMonolith/Action/FunctionalConvexity.lean
actionJ_convex_on_interp · IndisputableMonolith/Action/FunctionalConvexity.lean:67 
/-- **Convexity of the J-action.** For any two admissible paths sharing
    a domain, the action of the convex interpolation is bounded by the
    convex combination of the actions.

    `S[(1-s)γ₁ + s γ₂] ≤ (1-s) S[γ₁] + s S[γ₂]`

    This is the integrated form of pointwise convexity of `Jcost`. -/
theorem actionJ_convex_on_interp (hab : a ≤ b)
    (γ₁ γ₂ : AdmissiblePath a b) (s : ℝ) (hs : s ∈ Icc (0:ℝ) 1) :
    actionJ (interp γ₁ γ₂ s hs) ≤ (1 - s) * actionJ γ₁ + s * actionJ γ₂ := by
  -- Step 1: the integrand is bounded pointwise.
  have h_pointwise : ∀ t ∈ Set.uIcc a b,
      Jcost ((interp γ₁ γ₂ s hs).toFun t) ≤
        (1 - s) * Jcost (γ₁.toFun t) + s * Jcost (γ₂.toFun t) := by
    intro t ht
    -- On `[a,b]` (uIcc reduces to Icc since hab), positivity holds.
    have htIcc : t ∈ Icc a b := by
      have : Set.uIcc a b = Icc a b := by
        rw [Set.uIcc_of_le hab]
      rwa [this] at ht
    have hp1 : 0 < γ₁.toFun t := γ₁.pos t htIcc
    have hp2 : 0 < γ₂.toFun t := γ₂.pos t htIcc
    rw [interp_apply]
    exact Jcost_convex_combination s hs hp1 hp2
  -- Step 2: continuity / integrability of all three integrands on [a,b].
  have h_cont_interp : ContinuousOn (fun t => Jcost ((interp γ₁ γ₂ s hs).toFun t)) (Icc a b) := by
    have hpos : ∀ t ∈ Icc a b, 0 < (interp γ₁ γ₂ s hs).toFun t :=
      (interp γ₁ γ₂ s hs).pos
    -- Jcost is continuous on (0, ∞); composed with the continuous, positive interp.
    have hJcont : ContinuousOn Jcost (Set.Ioi (0:ℝ)) := by
      unfold Jcost
      apply ContinuousOn.sub
      · apply ContinuousOn.div_const
        apply ContinuousOn.add continuousOn_id
        exact continuousOn_inv₀.mono (fun x hx => ne_of_gt hx)
      · exact continuousOn_const
    refine ContinuousOn.comp hJcont (interp γ₁ γ₂ s hs).cont ?_
    intro t htmem
    exact hpos t htmem
  have h_cont_1 : ContinuousOn (fun t => Jcost (γ₁.toFun t)) (Icc a b) := by
    have hJcont : ContinuousOn Jcost (Set.Ioi (0:ℝ)) := by
      unfold Jcost
      apply ContinuousOn.sub
      · apply ContinuousOn.div_const
        apply ContinuousOn.add continuousOn_id
        exact continuousOn_inv₀.mono (fun x hx => ne_of_gt hx)
      · exact continuousOn_const
    refine ContinuousOn.comp hJcont γ₁.cont ?_
    intro t htmem; exact γ₁.pos t htmem
  have h_cont_2 : ContinuousOn (fun t => Jcost (γ₂.toFun t)) (Icc a b) := by
    have hJcont : ContinuousOn Jcost (Set.Ioi (0:ℝ)) := by
      unfold Jcost
      apply ContinuousOn.sub
      · apply ContinuousOn.div_const
        apply ContinuousOn.add continuousOn_id
        exact continuousOn_inv₀.mono (fun x hx => ne_of_gt hx)
      · exact continuousOn_const
    refine ContinuousOn.comp hJcont γ₂.cont ?_
    intro t htmem; exact γ₂.pos t htmem
  -- Step 3: integrate the pointwise inequality.
  have h_int_interp : IntervalIntegrable
      (fun t => Jcost ((interp γ₁ γ₂ s hs).toFun t))
      MeasureTheory.volume a b :=
    h_cont_interp.intervalIntegrable_of_Icc hab
  have h_int_1 : IntervalIntegrable (fun t => Jcost (γ₁.toFun t))
      MeasureTheory.volume a b :=
    h_cont_1.intervalIntegrable_of_Icc hab
  have h_int_2 : IntervalIntegrable (fun t => Jcost (γ₂.toFun t))
      MeasureTheory.volume a b :=
    h_cont_2.intervalIntegrable_of_Icc hab
  -- Form the dominating integrand (1-s) Jcost(γ₁) + s Jcost(γ₂).
  set rhs : ℝ → ℝ := fun t => (1 - s) * Jcost (γ₁.toFun t) + s * Jcost (γ₂.toFun t)
  have h_int_rhs : IntervalIntegrable rhs MeasureTheory.volume a b := by
    refine IntervalIntegrable.add ?_ ?_
    · exact h_int_1.const_mul (1 - s)
    · exact h_int_2.const_mul s
  -- Apply integral monotonicity on [a, b].
  have h_mono : ∫ t in a..b, Jcost ((interp γ₁ γ₂ s hs).toFun t)
      ≤ ∫ t in a..b, rhs t := by
    refine intervalIntegral.integral_mono_on hab h_int_interp h_int_rhs ?_
    intro t ht
    have htIcc : t ∈ Icc a b := ht
    have htUI : t ∈ Set.uIcc a b := by
      rw [Set.uIcc_of_le hab]; exact htIcc
    exact h_pointwise t htUI
  -- Compute the RHS integral.
  have h_rhs_eq : ∫ t in a..b, rhs t =
      (1 - s) * (∫ t in a..b, Jcost (γ₁.toFun t)) +
      s * (∫ t in a..b, Jcost (γ₂.toFun t)) := by
    show ∫ t in a..b, ((1 - s) * Jcost (γ₁.toFun t) + s * Jcost (γ₂.toFun t)) =
         (1 - s) * (∫ t in a..b, Jcost (γ₁.toFun t)) +
         s * (∫ t in a..b, Jcost (γ₂.toFun t))
    rw [intervalIntegral.integral_add (h_int_1.const_mul (1 - s)) (h_int_2.const_mul s)]
    rw [intervalIntegral.integral_const_mul, intervalIntegral.integral_const_mul]
  -- Assemble. The goal-as-stated has `actionJ`; unfold it to integrals.
  unfold actionJ
  calc ∫ t in a..b, Jcost ((interp γ₁ γ₂ s hs).toFun t)
      ≤ ∫ t in a..b, rhs t := h_mono
    _ = (1 - s) * (∫ t in a..b, Jcost (γ₁.toFun t)) +
        s * (∫ t in a..b, Jcost (γ₂.toFun t)) := h_rhs_eq
THEOREM Jcost_convex_combination · IndisputableMonolith/Action/FunctionalConvexity.lean
Jcost_convex_combination · IndisputableMonolith/Action/FunctionalConvexity.lean:47 
/-- The pointwise convexity of `Jcost` on `(0,∞)`: for `γ₁(t), γ₂(t) > 0` and
    `s ∈ [0,1]`, `J((1-s)γ₁ + s γ₂) ≤ (1-s) J(γ₁) + s J(γ₂)`.

    This is the engine of the convexity of `actionJ`. -/
lemma Jcost_convex_combination (s : ℝ) (hs : s ∈ Icc (0:ℝ) 1)
    {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
    Jcost ((1 - s) * x + s * y) ≤ (1 - s) * Jcost x + s * Jcost y := by
  -- Use ConvexOn version derived from StrictConvexOn.
  have hconv : ConvexOn ℝ (Ioi (0:ℝ)) Jcost := Jcost_strictConvexOn_pos.convexOn
  have h1 : (1 - s) + s = 1 := by ring
  have h0_le : 0 ≤ 1 - s := by linarith [hs.2]
  have hs_nn : 0 ≤ s := hs.1
  have hxmem : x ∈ Ioi (0:ℝ) := hx
  have hymem : y ∈ Ioi (0:ℝ) := hy
  have := hconv.2 hxmem hymem h0_le hs_nn h1
  -- The mathlib statement uses `•` (smul). Translate to `*`.
  simpa [smul_eq_mul] using this
THEOREM actionJ_minimum_unique_value · IndisputableMonolith/Action/FunctionalConvexity.lean
actionJ_minimum_unique_value · IndisputableMonolith/Action/FunctionalConvexity.lean:237 
/-- **Uniqueness via convexity.** If two paths both minimize the action
    among competitors with their shared endpoints, they have the same
    action value. -/
theorem actionJ_minimum_unique_value (_hab : a ≤ b)
    (γ₁ γ₂ : AdmissiblePath a b)
    (h_endpoints : fixedEndpoints γ₁ γ₂)
    (h₁ : ∀ γ : AdmissiblePath a b, fixedEndpoints γ₁ γ → actionJ γ₁ ≤ actionJ γ)
    (h₂ : ∀ γ : AdmissiblePath a b, fixedEndpoints γ₂ γ → actionJ γ₂ ≤ actionJ γ) :
    actionJ γ₁ = actionJ γ₂ := by
  have h12 := h₁ γ₂ h_endpoints
  have h21 := h₂ γ₁ (fixedEndpoints_symm h_endpoints)
  linarith

What this page does not claim

The existence of a minimizing path is not proved; the theorem is conditional on the path being given. The minimizing path is not identified with any specific physical trajectory, such as a geodesic in spacetime. The framework does not claim its J-cost is the only possible integrand for an action functional.

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/FunctionalConvexity.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND