Cost Calibration Deriv2 Jlog

The calibration theorem

In the Recognition Science framework, the cost of a recognition event is measured by a function called cost, a discrete record of how much effort reality's ledger must spend to register a change. The framework's central object, Jcost, is built from a simple requirement: the cost of moving from a state x to a state y must be the same as the cost of moving back. The function Jlog is the same cost written in logarithmic coordinates, where multiplication becomes addition. The declaration deriv2_Jlog establishes that the second derivative of Jlog at zero is exactly 1.

This is a calibration statement. In ordinary language, it fixes the unit of measurement for cost. A second derivative is a measure of curvature, so the theorem says that at the identity point, where no change has occurred, the cost function has unit curvature. This is not a free choice; it is a proved consequence of the framework's defining axioms. The machine-checked library of formal theorems shows that Jlog equals cosh t minus 1, that its first derivative is sinh t, and that its second derivative is cosh t. At t equals zero, cosh zero is 1, so the calibration follows directly.

The theorem also connects the logarithmic and ordinary forms of the cost. The identity (Jcost composed with exp) equals Jlog holds pointwise, so the same calibration applies to Jcost when written in log-coordinates. The framework packages this as a class called UnitCurvature, which states that any function satisfying the same condition has second derivative 1 at the identity. This completes the characterization of J: the five plain conditions force the functional form, and this calibration fixes its scale uniquely.

What the declaration does not claim is equally precise. It does not claim that the second derivative is 1 everywhere; it claims it only at the point zero. It does not claim that any function with unit curvature at the identity is the cost function; the full characterization requires all five axioms, not just the calibration. And it does not claim anything about what the cost function means physically, only that within the framework, its scale is fixed.

/-- Second derivative of Jlog is cosh -/
lemma deriv2_Jlog (t : ℝ) : deriv (deriv Jlog) t = cosh t := by
  have h1 : deriv Jlog = sinh := by
    funext s; exact deriv_Jlog s
  rw [h1]
  exact (hasDerivAt_sinh t).deriv

/-- Jlog equals cosh t - 1 -/
lemma Jlog_eq_cosh (t : ℝ) : Jlog t = Real.cosh t - 1 := Jlog_as_cosh t

/-- First derivative of Jlog is sinh -/
lemma deriv_Jlog (t : ℝ) : deriv Jlog t = sinh t := by
  exact (hasDerivAt_Jlog_new t).deriv

/-- Second derivative of Jlog is cosh -/
lemma deriv2_Jlog (t : ℝ) : deriv (deriv Jlog) t = cosh t := by
  have h1 : deriv Jlog = sinh := by
    funext s; exact deriv_Jlog s
  rw [h1]
  exact (hasDerivAt_sinh t).deriv

/-- The calibration theorem: second derivative at zero equals 1 -/
theorem Jlog_second_deriv_at_zero : deriv (deriv Jlog) 0 = 1 := by
  rw [deriv2_Jlog]
  exact cosh_zero

/-- Identity: (Jcost ∘ exp) equals Jlog pointwise. -/
lemma Jcost_comp_exp_eq_Jlog : (fun t : ℝ => Jcost (Real.exp t)) = Jlog := rfl

What this page does not claim

The second derivative of Jlog is 1 everywhere, not just at zero. Any function with unit curvature at the identity is the cost function; all five axioms are required. The calibration theorem assigns a physical meaning to the cost unit.

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/Calibration.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: