Cost Convexity Deriv2 Jcost One

The curvature at one

The function J(x) = ½(x + x⁻¹) − 1, defined for positive x, is the cost of recognition in the Recognition Science framework: it measures how much a ledger, a discrete record of events, must pay to recognize a change of scale x. The declaration deriv2_Jcost_one establishes that the second derivative of this function at x = 1 equals 1. In plain terms, the curvature of the cost curve at its minimum is exactly one, a clean unit value that anchors the framework's uniqueness theorem.

The proof is short and mechanical. The first derivative of J is J'(x) = (1 − x⁻²)/2, and the second derivative is J''(x) = x⁻³. At x = 1, this gives J''(1) = 1. The machine-checked library of formal theorems confirms this in a few lines, using the fact that the second derivative of the related function Jlog(t) = cosh(t) − 1 is cosh(t), which is always positive, making Jlog strictly convex on the whole real line. Strict convexity of Jcost on the positive reals follows by composition with the exponential function.

What the declaration does not claim is just as important. It does not assert that J is the only cost function with this property; that is a separate uniqueness theorem. It does not say anything about x = 0 or negative x, where the function is not defined. It does not claim that the value 1 has any physical meaning by itself; it is a mathematical anchor, not a measured constant. The theorem is a precise, narrow statement about the shape of one function at one point, and it earns its place by supporting the larger forcing chain that derives the golden ratio and three spatial dimensions.

For the reader, the payoff is a concrete picture: the cost curve bottoms out at x = 1 with a curvature of exactly one, no more and no less. That unit curvature is what makes the uniqueness proof tractable, because it fixes the local behavior of the cost function at the point where recognition costs nothing. The declaration is a small gear in a large machine, but it is a gear that has been checked by a computer and found to fit.

/-- Second derivative of Jcost at 1 equals 1: J''(1) = 1 -/
theorem deriv2_Jcost_one : deriv (deriv Jcost) 1 = 1 := by
  rw [deriv2_Jcost one_pos]
  simp

lemma hasDerivAt_Jcost_pos {x : ℝ} (hx : 0 < x) :
    HasDerivAt Jcost (JcostDeriv x) x := by
  -- Jcost x = (x + x⁻¹)/2 - 1
  -- Jcost' x = (1 - x⁻²)/2
  unfold Jcost JcostDeriv
  have hne : x ≠ 0 := hx.ne'
  -- d/dx (x + x⁻¹)/2 - 1 = (1 - x⁻²)/2
  have h1 : HasDerivAt (fun y => y) 1 x := hasDerivAt_id x
  have h2 : HasDerivAt (fun y => y⁻¹) (-(x^2)⁻¹) x := by
    have hinv := hasDerivAt_inv hne
    simp only [neg_neg] at hinv
    convert hinv using 1
  have h3 : HasDerivAt (fun y => y + y⁻¹) (1 + (-(x^2)⁻¹)) x := h1.add h2
  have h4 : HasDerivAt (fun y => (y + y⁻¹) / 2) ((1 + (-(x^2)⁻¹)) / 2) x := h3.div_const 2
  have h5 : HasDerivAt (fun y => (y + y⁻¹) / 2 - 1) ((1 + (-(x^2)⁻¹)) / 2) x := h4.sub_const 1
  convert h5 using 1

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

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

What this page does not claim

The declaration does not prove that J is the only cost function with unit curvature at one. The declaration says nothing about the behavior of J at x = 0 or for negative x. The value 1 at x = 1 is a mathematical anchor, not a measured physical constant.

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: