Cost Convexity Jlog Strict Convex On

The shape of the cost curve

A function is strictly convex when the line segment between any two points on its graph lies strictly above the graph itself. The Recognition Science framework's central cost function, written Jcost(x) = ½(x + x⁻¹) - 1, has exactly this bowl shape on the positive numbers. Its graph bends upward everywhere, with no flat stretches and no wobbles. The framework proves this in its machine-checked library of formal theorems, where the declaration Jlog_strictConvexOn records the result. The proof works by changing variables: write x as e^t, so the cost becomes cosh t - 1, and the hyperbolic cosine is strictly convex because its second derivative is itself, always positive.

Strict convexity is not a decorative property. A strictly convex function has at most one minimum, and for this cost function the minimum sits at x = 1, where the cost is zero. That single minimum is what lets the framework's uniqueness theorem T5 select one cost function among all candidates. Without strict convexity, the functional equation that forces the cost could admit multiple solutions, and the whole derivation would branch. The curvature is the guarantee that the ledger's cost has one unambiguous shape.

The classical picture behind this is older than the framework. The function ½(x + x⁻¹) is the arithmetic mean of a number and its reciprocal, and its convexity on the positive reals is a standard fact in real analysis. The framework's contribution is to show that this particular convex function, not some other one, is forced by the five conditions of reciprocal symmetry, zero cost at unity, composition law, calibration, and continuity. The strict convexity is a lemma in that proof, a step that makes the uniqueness argument work.

What the declaration does not claim is just as important as what it proves. It does not claim that Jcost is convex on all real numbers; the function is undefined at zero and the convexity statement is restricted to positive inputs. It does not claim that strict convexity alone identifies the cost function; many strictly convex functions exist, and the uniqueness comes from the full set of conditions, not from the bowl shape by itself. It does not claim anything about the physical interpretation of the cost, only about its mathematical properties.

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

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

What this page does not claim

Jcost is not claimed to be convex on all real numbers, only on the positive reals. Strict convexity alone does not identify the cost function; the full set of five conditions is needed. The declaration makes no claim about the physical meaning of the cost function.

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: