Encyclopedia Action Action Functional Convexity Geodesic Minimizes Via Convexity

ARTICLE 4 claims 4 theorems

Action Functional Convexity Geodesic Minimizes Via Convexity

A path that beats every nearby rival also beats every distant one, once the cost of motion is convex.

Verify this page

Convexity and the shortest path

In the calculus of variations, a central question is when a path that is a local minimum of a cost functional is also a global minimum. For a functional that is convex, meaning the cost of a weighted average of two paths is no more than the weighted average of their costs, this local-to-global step is automatic. The Recognition Science library establishes this for its own action functional, the integral of the recognition cost J along a path, and the theorem is named geodesic_minimizes_via_convexity.

The theorem states: if a path γ_geo has no higher action than any convex interpolation toward a competitor γ_other (for every interpolation parameter s in [0,1]), then γ_geo has action no higher than γ_other itself. The proof is one line of convex calculus: the convexity inequality bounds the interpolated action above, and the hypothesis bounds it below, forcing the endpoint comparison. The library further shows that checking a single positive interpolation step, not all of them, suffices, and that two global minimizers with the same endpoints must have equal action values.

The deep content is not the final implication but the convexity itself. The library establishes that the pointwise convexity of Jcost on the positive reals integrates to convexity of the action functional. This pointwise convexity is itself derived from the d'Alembert functional equation that characterizes J. The chain of reasoning runs: d'Alembert uniqueness forces the form of J, which forces convexity, which forces the least-action principle. The headline theorem principle_of_least_action states this unconditionally: a path that does not decrease the action on the way to any competitor, at even one positive step, is a global minimizer.

What the theorem does not claim is existence. It assumes a path γ_geo that already satisfies the no-decrease condition; it does not establish that such a path exists for given endpoints. The action functional is defined on admissible paths, and the theorem applies only within that class. The theorem also does not claim uniqueness of the minimizing path itself, only uniqueness of the minimum action value. It does not identify the minimizing path explicitly, nor does it connect this abstract variational principle to the physical geodesics of spacetime or to the empirical trajectories of particles.

THEOREM geodesic_minimizes_via_convexity · IndisputableMonolith/Action/FunctionalConvexity.lean
geodesic_minimizes_via_convexity · IndisputableMonolith/Action/FunctionalConvexity.lean:211 
/-- **Even stronger headline.** If `γ_geo` is a critical point of the
    action functional in the convexity-witness sense (action does not
    *decrease* under any infinitesimal interpolation perturbation toward
    a competitor), then by convexity it is a global minimum.

    Specifically: if for every `γ_other` and every `s ∈ [0,1]`,
    `actionJ γ_geo ≤ actionJ (interp γ_geo γ_other s)`, then
    `actionJ γ_geo ≤ actionJ γ_other`.

    The convexity inequality already proved (`actionJ_convex_on_interp`)
    says `actionJ (interp γ_geo γ_other s) ≤ (1-s) actionJ γ_geo + s actionJ γ_other`.
    Combining: `actionJ γ_geo ≤ (1-s) actionJ γ_geo + s actionJ γ_other`
    for all `s ∈ [0,1]`. Taking `s = 1` gives the result.

    The point is: the "interpolation-minimality" hypothesis used by the
    legacy `convex_implies_geodesic_minimizes` is **automatically
    satisfied** by any candidate critical point, given convexity. -/
theorem geodesic_minimizes_via_convexity (_hab : a ≤ b)
    (γ_geo γ_other : AdmissiblePath a b)
    (h_endpoints : fixedEndpoints γ_geo γ_other)
    (h_no_decrease :
      ∀ (s : ℝ) (hs : s ∈ Icc (0:ℝ) 1),
        actionJ γ_geo ≤ actionJ (interp γ_geo γ_other s hs)) :
    actionJ γ_geo ≤ actionJ γ_other :=
  geodesic_minimizes_unconditional _hab γ_geo γ_other h_endpoints h_no_decrease
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 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_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

No existence of a minimizing path is established for given endpoints. No identification of the minimizing path is given. No connection to physical geodesics or empirical trajectories is established.

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