Cost Convexity

Cost convexity

Cost convexity is the shape property of the recognition cost function J that Recognition Science derives from its five founding conditions. A function is strictly convex when the line segment between any two distinct points on its graph lies strictly above the graph itself. For J this means the cost of a mismatch grows faster than linearly as the mismatch moves away from perfect agreement, so the graph is a single bowl with exactly one lowest point. This property is machine-checked, not assumed, and it is foundational for the uniqueness theorem T5, which forces the exact form of J.

The module establishes strict convexity for the two equivalent forms of J. The first form, Jlog(t) = cosh(t) - 1, is strictly convex on the whole real line. The proof uses the fact that the second derivative of cosh is cosh itself, which is always positive. The second form, Jcost(x) = ½(x + x⁻¹) - 1, is strictly convex on the positive reals, the domain where x represents a ratio of recognition magnitudes. Its second derivative is x⁻³, which is positive for every x > 0. The two forms are linked by the substitution x = e^t, so Jcost(e^t) = Jlog(t).

Strict convexity is what makes the cost function well behaved for minimization. A strictly convex function on a convex domain has at most one point where it reaches its minimum. For Jcost on the positive reals, that unique minimum sits at x = 1, where the cost is zero, meaning perfect agreement. The second derivative at that point equals 1, which sets the local curvature scale. Because the minimum is unique and the graph has no flat regions, the forcing chain that builds the rest of Recognition Science has a stable foundation: the cost function cannot wander into multiple equally good states.

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

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

What this page does not claim

This answer does not prove the uniqueness theorem T5 itself. This answer does not claim that convexity alone determines the numerical value of J; the five founding conditions are needed for that. This answer does not claim that Jcost is convex on the whole real line; its domain is 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: