Cost Convexity Strict Convex On Cosh

Why the cost curve bends one way

The hyperbolic cosine, cosh(t) = (e^t + e^(-t))/2, is the average of an exponential curve and its mirror image. It is the shape a hanging chain takes, and it is strictly convex: every chord drawn between two points on the curve lies strictly above the curve itself. Because its second derivative is cosh(t), which is positive everywhere, the curve bends upward at every point on the real line. A machine-checked library of formal theorems records this as strict convexity, the property that a straight line segment between any two distinct points on the graph never dips below the graph.

The Recognition Science cost function, a measure of how expensive a recognition event is, takes the form J(x) = ½(x + 1/x) - 1 for positive x. Writing x = e^t turns it into Jlog(t) = cosh(t) - 1. The library proves that Jlog is strictly convex on the whole real line, and that Jcost is strictly convex on the positive reals. The proof for Jcost runs through its second derivative: J''(x) = x^(-3), which is positive for every x > 0. A positive second derivative on an interval means the function curves upward there, so the cost function has exactly one minimum, at x = 1, where J(1) = 0.

This single-minimum property is foundational for the framework's uniqueness theorem T5, which forces the specific form of the cost function from five plain conditions. Strict convexity ensures that if a minimum exists, it is unique; the curve cannot have two separate lowest valleys. The proof is axiom-clean, meaning it relies only on the standard logical axioms of the ambient type theory, not on any framework-specific assumptions.

What the declaration does not claim is broader: it says nothing about the physical interpretation of recognition events, nothing about how the cost function connects to particle masses or spatial dimensions, and nothing about the empirical agreement of the framework's constants with measured values. It is a purely mathematical statement about the shape of one function, verified mechanically, that serves as one rung in a longer chain of derivations.

/-- cosh is strictly convex on ℝ.

    Proof: cosh'' = cosh > 0 everywhere. A function with positive second
    derivative on a convex set is strictly convex. -/
theorem cosh_strictly_convex : StrictConvexOn ℝ univ Real.cosh := by
  apply strictConvexOn_of_deriv2_pos convex_univ
  · -- cosh is continuous
    exact Real.continuous_cosh.continuousOn
  · -- cosh'' = cosh > 0 on interior (which is univ)
    intro x _
    -- deriv^[2] cosh = cosh
    show 0 < deriv^[2] Real.cosh x
    rw [Function.iterate_succ, Function.iterate_one, Function.comp_apply]
    -- First derivative of cosh is sinh
    have h1 : deriv Real.cosh = Real.sinh := Real.deriv_cosh
    -- Second derivative: deriv sinh = cosh
    have h2 : deriv Real.sinh = Real.cosh := Real.deriv_sinh
    -- So deriv (deriv cosh) x = cosh x > 0
    rw [h1, congrFun h2 x]
    exact Real.cosh_pos x

/-- 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

The declaration says nothing about the physical meaning of recognition events or their cost. It does not connect the cost function to particle masses, spatial dimensions, or any measured physical constant. It does not claim the cost function is convex on any domain other than the positive reals.

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: