Jlog_unit_curvature
plain-language theorem explainer
Jlog has unit curvature at the identity, so its second derivative at zero equals 1. This fixes the normalization scale for the cost function in Recognition Science and completes the local characterization of J. Researchers deriving physical constants from the functional equation cite it to anchor the comparison operator. The proof is a one-line term that invokes the prior second-derivative theorem Jlog_second_deriv_at_zero.
Claim. The second derivative of the log-domain cost function satisfies $ (Jlog)''(0) = 1 $.
background
The Calibration module proves that the second derivative of Jlog at zero equals 1, establishing the unit normalization axiom (A4). Jlog is defined by composing the cost function with the exponential: Jlog(t) := Jcost(exp t). This places comparisons in logarithmic coordinates and builds directly on the Jlog definition in the Cost module together with the upstream theorem Jlog_second_deriv_at_zero, whose doc-comment states it is the calibration theorem whose second derivative at zero equals 1.
proof idea
The proof is a one-line term wrapper that applies Jlog_second_deriv_at_zero.
why it matters
This theorem supplies the alternative formulation of the calibration result, confirming unit curvature at the identity and thereby fixing the scale of J uniquely. It completes the local characterization of the cost function as described in the module documentation. In the Recognition Science framework it anchors the normalization step that precedes derivation of constants such as alpha inverse inside (137.030, 137.039) and supports the forcing chain from T0 through T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.