Encyclopedia Action Action Functional Convexity Jcost Convex Combination

ARTICLE 3 claims 3 theorems

Action Functional Convexity Jcost Convex Combination

A single inequality about a cost function turns a local check into a global proof, and it is the engine behind a least-action principle.

Verify this page

The convexity engine

In the Recognition Science framework, a ledger, a discrete record of events, assigns a cost, a nonnegative number, to each possible transition. The central object is the cost function J(x) = (x + 1/x)/2 - 1, which the framework's library of machine-checked theorems derives from five plain conditions. The declaration Jcost_convex_combination establishes a specific property of this function: for any two positive numbers x and y, and any mixing weight s between 0 and 1, the cost of the weighted average is never more than the weighted average of the costs. In symbols, J((1-s)x + s y) ≤ (1-s)J(x) + s J(y). This is the definition of a convex function, and it holds for all positive inputs.

The inequality matters because it is the engine for a much larger result. The framework defines an action, a total cost accumulated along a path, by integrating the cost function along that path. The declaration actionJ_convex_on_interp shows that this action functional inherits the convexity of the cost: the action of a weighted average of two paths is bounded by the weighted average of their actions. From this, the framework's library proves the headline theorem geodesic_minimizes_unconditional: if a path has no lower action than any competitor along the straight-line interpolation between them, then it is a global minimum of the action among all admissible competitors with the same endpoints. The local check, done on a single segment, propagates to a global statement. This is the unconditional principle of least action, with no extra hypothesis beyond the convexity of J, which is itself a theorem of the d'Alembert functional equation.

The declaration itself is a narrow lemma, not a sweeping statement. It does not claim that any particular path is a minimizer, nor does it assert that a minimizer exists. It only states the convexity inequality for the cost function at two points. The existence of a critical point, a path where the action is stationary, is a separate matter that the framework treats as a modulo condition. The convexity result is the tool that turns a local minimum into a global one, but it does not by itself produce the minimum. The declaration also does not claim anything about the physical interpretation of the action, such as which paths are physically realized; that is a further step that the framework's least-action principle addresses.

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_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 geodesic_minimizes_unconditional · IndisputableMonolith/Action/FunctionalConvexity.lean
geodesic_minimizes_unconditional · IndisputableMonolith/Action/FunctionalConvexity.lean:170 
/-- **Headline theorem.** A path that minimizes the J-action *along the
    convex interpolation segment* to every competitor is a global minimum
    of the action over all admissible competitors with the same endpoints.

    This discharges the `h_min` interpolation-witness that
    `Decision.VariationalCalculus.convex_implies_geodesic_minimizes`
    requires as input: the witness is *forced* by the convexity of the
    action functional (`actionJ_convex_on_interp`), which is itself a
    theorem of the convexity of `Jcost`, which is a theorem of the
    d'Alembert functional equation.

    Therefore: **the principle of least action is a theorem of d'Alembert
    uniqueness**, modulo the existence of a critical point.

    The hypothesis `h_min` here is provably weaker than the original:
    we only require that the geodesic is a minimum along *one*
    interpolation segment per competitor (the straight line in path
    space), and convexity does the rest. -/
theorem geodesic_minimizes_unconditional (_hab : a ≤ b)
    (γ_geo γ_other : AdmissiblePath a b)
    (_h_endpoints : fixedEndpoints γ_geo γ_other)
    (h_critical_along_segment :
      ∀ (s : ℝ) (hs : s ∈ Icc (0:ℝ) 1),
        actionJ γ_geo ≤ actionJ (interp γ_geo γ_other s hs)) :
    actionJ γ_geo ≤ actionJ γ_other := by
  -- Specialize the segment-minimality at s = 1.
  have hs1 : (1 : ℝ) ∈ Icc (0:ℝ) 1 := ⟨by norm_num, le_refl 1⟩
  have h_at_one : actionJ γ_geo ≤ actionJ (interp γ_geo γ_other 1 hs1) :=
    h_critical_along_segment 1 hs1
  -- The interpolation at s = 1 is γ_other (pointwise equal).
  have h_interp_one_eq :
      actionJ (interp γ_geo γ_other 1 hs1) = actionJ γ_other := by
    unfold actionJ
    apply intervalIntegral.integral_congr
    intro t _
    have h_eq : (interp γ_geo γ_other 1 hs1).toFun t = γ_other.toFun t := by
      simp [interp_apply]
    exact congrArg Jcost h_eq
  rw [← h_interp_one_eq]
  exact h_at_one

What this page does not claim

The declaration does not assert that any particular path is a minimizer of the action. The declaration does not claim that a minimizer exists, only that convexity propagates a local minimum to a global one. The declaration does not address the physical interpretation of the action or which paths are physically realized.

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