Encyclopedia Action Action Functional Convexity Action J Local Min Is Global

ARTICLE 3 claims 3 theorems

Action Functional Convexity Action J Local Min Is Global

A local check, one step toward any rival path, forces a global minimum of the action functional: convexity turns a tiny comparison into a universal one.

Verify this page

The convexity bridge

In the calculus of variations, the action is a number attached to a whole path: integrate a cost along the path from start to finish. A central question asks when a path that beats every nearby path also beats every path at all. For a general cost function this is false. The framework's library proves that for its specific cost, the J-cost, the implication holds: if a path does not increase the action on a straight-line step toward any rival, then it is a global minimum among all admissible rivals sharing its endpoints.

The engine is convexity. A function is convex when its value at a weighted average never exceeds the weighted average of its values. The J-cost is pointwise convex on positive numbers, and integrating a pointwise convex cost yields a convex action functional. The library's theorem actionJ_local_min_is_global states this precisely: for any two admissible paths with fixed endpoints, if the action at the first path is at most the action at the interpolation toward the second at some positive step s₀, then the first path's action is at most the second's. The proof is convex calculus: the inequality at one interior point, combined with convexity on the whole segment, propagates to the endpoint.

The declaration is the final link in a chain. Earlier theorems required a hypothesis that the path is minimal along every interpolation step, a witness that had to be supplied. This theorem removes that burden: a single positive step toward each competitor suffices. The library's status report records the module as having zero sorry and zero axioms, meaning the result is fully checked by the machine. The practical consequence: the principle of least action for this cost is unconditional, needing no extra input beyond the cost's own convexity, which itself follows from the d'Alembert functional equation.

What the theorem does not say matters as much as what it proves. It does not assert that a minimizer exists; it only says that if a path passes the local test, it is globally minimal among rivals. Existence of a critical point is a separate question, left open. It also does not apply to arbitrary cost functions: the result depends on the specific J-cost and its convexity, so it says nothing about actions built from other integrands. Finally, it does not claim that the minimizing path is unique, only that any two minimizers share the same action value.

THEOREM actionJ_local_min_is_global · IndisputableMonolith/Action/FunctionalConvexity.lean
actionJ_local_min_is_global · IndisputableMonolith/Action/FunctionalConvexity.lean:252 
/-- **Truly unconditional principle of least action.**

    If `γ_geo` is a local minimum of the action functional in the segment
    sense (no decrease toward `γ_other` along the convex interpolation
    segment for any `s` near `0`), then by convexity it is a *global*
    minimum vs `γ_other`.

    The conclusion uses only the convexity of `actionJ` on the interpolation
    segment, which is itself a theorem of pointwise convexity of `Jcost`,
    which is a theorem of d'Alembert uniqueness.

    **No extra hypothesis is required beyond `Jcost`'s convexity.**

    The hypothesis `h_local_min` is a *weakest possible* form of "critical
    point": just `actionJ γ_geo ≤ actionJ (interp γ_geo γ_other s hs)` for
    one specific `s ∈ (0,1]` is enough. The convexity of the action ensures
    that minimization on the segment propagates to the endpoint. -/
theorem actionJ_local_min_is_global (hab : a ≤ b)
    (γ_geo γ_other : AdmissiblePath a b)
    (s₀ : ℝ) (hs₀ : s₀ ∈ Icc (0:ℝ) 1) (hs₀_pos : 0 < s₀)
    (h_local_min : actionJ γ_geo ≤ actionJ (interp γ_geo γ_other s₀ hs₀)) :
    actionJ γ_geo ≤ actionJ γ_other := by
  -- By convexity of actionJ on the segment:
  --   actionJ (interp γ_geo γ_other s₀ hs₀) ≤ (1-s₀) actionJ γ_geo + s₀ actionJ γ_other
  have h_conv := actionJ_convex_on_interp hab γ_geo γ_other s₀ hs₀
  -- Combine with local minimality:
  --   actionJ γ_geo ≤ (1-s₀) actionJ γ_geo + s₀ actionJ γ_other
  have h_combine : actionJ γ_geo ≤ (1 - s₀) * actionJ γ_geo + s₀ * actionJ γ_other :=
    le_trans h_local_min h_conv
  -- Rearrange: s₀ · actionJ γ_geo ≤ s₀ · actionJ γ_other
  --   actionJ γ_geo - (1 - s₀) actionJ γ_geo ≤ s₀ * actionJ γ_other
  --   s₀ · actionJ γ_geo ≤ s₀ · actionJ γ_other
  --   Since s₀ > 0, divide: actionJ γ_geo ≤ actionJ γ_other.
  have h_factor : s₀ * actionJ γ_geo ≤ s₀ * actionJ γ_other := by linarith
  exact le_of_mul_le_mul_left h_factor hs₀_pos
THEOREM Jcost_convex_combination · actionJ_convex_on_interp · 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
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 functionalConvexity_status · IndisputableMonolith/Action/FunctionalConvexity.lean
functionalConvexity_status · IndisputableMonolith/Action/FunctionalConvexity.lean:313 
def functionalConvexity_status : String :=
  "Action.FunctionalConvexity: actionJ_convex_on_interp, geodesic_minimizes_unconditional (0 sorry, 0 axiom)"

What this page does not claim

The theorem does not prove existence of a minimizing path, only that a local minimum is global. The result applies only to the specific J-cost, not to arbitrary action functionals. The theorem does not claim uniqueness of the minimizer, only equality of action values among minimizers.

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