Cost Convexity Jcost Strict Convex On Pos

The convexity of Jcost

In mathematics, a function is strictly convex on an interval if every chord between two distinct points lies strictly above the graph. Equivalently, the second derivative is positive throughout the interval. Strict convexity guarantees a unique minimum: a strictly convex function can dip to its lowest value at exactly one point, never along a flat stretch.

The Recognition Science framework defines a ledger, a discrete record of recognition events, and assigns each event a cost, a number measuring how much recognition effort the event requires. The framework's central cost function is Jcost(x) = ½(x + x⁻¹) − 1, defined for positive x. This function measures the cost of recognizing a ratio x; it is zero when x = 1, meaning no cost when the recognized ratio matches itself exactly.

The declaration Jcost_strictConvexOn_pos, proved in the framework's machine-checked library of formal theorems, establishes that Jcost is strictly convex on the positive real numbers (0, ∞). The proof computes the second derivative: J''(x) = x⁻³, which is positive for every x > 0. A function with positive second derivative on an interval is strictly convex there. The same library proves the equivalent logarithmic form Jlog(t) = cosh t − 1 is strictly convex on the whole real line, and Jcost is Jlog composed with the natural logarithm, so the two convexity results mirror each other.

This convexity is not an isolated curiosity. It underpins the framework's uniqueness theorem for the cost function: among all functions satisfying the framework's five founding conditions, Jcost is the only one. Strict convexity ensures that the minimum at x = 1 is unique, which the uniqueness proof leans on. The result also means that costs for ratios near 1 grow slowly, while costs for very large or very small ratios grow rapidly, matching the intuition that extreme mismatches are disproportionately expensive to recognize.

The declaration does not claim that Jcost is convex on negative numbers, where the formula involves division by zero and the function is undefined. It does not claim that Jcost is the only strictly convex function satisfying the framework's conditions; other strictly convex functions exist, but they do not satisfy all five founding conditions. It also does not claim that the framework's cost function applies to physical systems directly; that bridge remains open.

/-- Strict convexity of `Jcost` on `(0, ∞)`. -/
theorem Jcost_strictConvexOn_pos : StrictConvexOn ℝ (Ioi (0 : ℝ)) Jcost := by
  -- A function is strictly convex if its derivative is strictly increasing
  apply strictConvexOn_of_deriv2_pos (convex_Ioi 0)
  · -- Continuity on (0, ∞)
    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
  · -- Positive second derivative on interior
    intro x hx
    rw [interior_Ioi] at hx
    -- deriv^[2] Jcost x = x⁻³ > 0
    show 0 < deriv^[2] Jcost x
    rw [Function.iterate_succ, Function.iterate_one, Function.comp_apply]
    -- In a neighborhood of x, deriv Jcost = JcostDeriv
    have h_event : ∀ᶠ y in nhds x, deriv Jcost y = JcostDeriv y := by
      have h_mem : Ioi (0 : ℝ) ∈ nhds x := Ioi_mem_nhds hx
      filter_upwards [h_mem] with y hy using deriv_Jcost hy
    have h_deriv2 : deriv (deriv Jcost) x = deriv JcostDeriv x := Filter.EventuallyEq.deriv_eq h_event
    rw [h_deriv2, deriv_JcostDeriv hx]
    unfold JcostDeriv'
    -- x ^ (-3) > 0 for x > 0
    have hx_pos : 0 < x := hx
    exact zpow_pos hx_pos (-3)

/-- Second derivative of Jcost at x > 0: J''(x) = x⁻³ -/
lemma deriv2_Jcost {x : ℝ} (hx : 0 < x) :
    deriv (deriv Jcost) x = x ^ (-3 : ℤ) := by
  have h_event : ∀ᶠ y in nhds x, deriv Jcost y = JcostDeriv y := by
    have h_mem : Set.Ioi (0 : ℝ) ∈ nhds x := Ioi_mem_nhds hx
    filter_upwards [h_mem] with y hy using deriv_Jcost hy
  have h_deriv2 : deriv (deriv Jcost) x = deriv JcostDeriv x :=
    Filter.EventuallyEq.deriv_eq h_event
  rw [h_deriv2, deriv_JcostDeriv hx]
  rfl

/-- Strict convexity of `Jlog` on `ℝ`. -/
theorem Jlog_strictConvexOn : StrictConvexOn ℝ univ Jlog := by
  -- Jlog = cosh - 1, and cosh is strictly convex
  -- Subtracting a constant preserves strict convexity
  have h : Jlog = fun t => Real.cosh t - 1 := by ext t; exact Jlog_eq_cosh_sub_one t
  rw [h]
  exact strictConvexOn_cosh.add_const (-1)

What this page does not claim

Jcost is not defined or claimed convex on negative numbers, where the formula fails. Jcost is not the only strictly convex function; other strictly convex functions exist that do not satisfy all five founding conditions. The framework's cost function does not directly apply to physical systems; the physical bridge remains open.

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/Cost/Convexity.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: