Jlog_second_deriv_at_zero
The calibration result establishes that the second derivative of the log-domain cost function Jlog at the origin equals one. Researchers calibrating the Recognition Science cost function would cite this to anchor the unit normalization axiom. The proof reduces the claim via the known second-derivative formula for Jlog and evaluates the hyperbolic cosine at zero.
claim$ (d^2 / dt^2) J_{log}(t) |_{t=0} = 1 $, where $ J_{log}(t) := J_{cost}(e^t) $.
background
Jlog is the log-domain version of the cost function, defined by composing Jcost with the exponential: Jlog(t) = Jcost(exp t), which equals cosh(t) - 1. The module proves the second derivative of Jlog at zero equals 1, establishing the unit normalization axiom (A4) that fixes the scale uniquely and completes the characterization of J. The key upstream lemma states that the second derivative of Jlog equals the hyperbolic cosine function.
proof idea
The proof applies the lemma that the second derivative of Jlog equals cosh, reducing the claim directly to the evaluation cosh(0) = 1.
why it matters in Recognition Science
This result feeds the theorems Jcost_comp_exp_second_deriv_at_zero and Jlog_unit_curvature in the same module. It establishes the unit normalization axiom (A4) as described in the module documentation. In the Recognition Science framework this calibration anchors the J function's curvature at the identity, consistent with J-uniqueness and the self-similar fixed point.
scope and limits
- Does not derive the explicit form of Jlog from first principles.
- Does not compute derivatives at points other than zero.
- Does not address the corresponding statement for Jcost directly.
- Does not extend the result to higher-order derivatives.
Lean usage
theorem Jcost_comp_exp_second_deriv_at_zero : deriv (deriv (fun t : ℝ => Jcost (Real.exp t))) 0 = 1 := by have h : (fun t : ℝ => Jcost (Real.exp t)) = Jlog := rfl; rw [h]; exact Jlog_second_deriv_at_zeroformal statement (Lean)
41theorem Jlog_second_deriv_at_zero : deriv (deriv Jlog) 0 = 1 := by
proof body
Term-mode proof.
42 rw [deriv2_Jlog]
43 exact cosh_zero
44
45/-- Alternative formulation: Jlog has unit curvature at the identity -/