UnitCurvature
plain-language theorem explainer
The UnitCurvature class encodes the normalization that the second derivative of F composed with exp equals one at zero. Researchers calibrating the Recognition Science cost function cite this to fix the unit scale for Jcost. The declaration supplies an instance for Jcost by direct appeal to the precomputed second-derivative theorem.
Claim. For a map $F : ℝ → ℝ$, UnitCurvature($F$) asserts that the second derivative of $F ∘ exp$ at zero equals 1. An instance holds for the Jcost function.
background
The module proves the second derivative of Jlog at zero equals 1, establishing the unit normalization axiom (A4). Jcost is the cost function in RS-native units; the upstream theorem Jcost_comp_exp_second_deriv_at_zero reduces Jcost ∘ exp to Jlog by definition, then invokes Jlog_second_deriv_at_zero. This calibration fixes the scale uniquely and completes the characterization of J.
proof idea
The declaration is a one-line instance of UnitCurvature for Jcost. It assigns the second_deriv_at_identity field to the theorem Jcost_comp_exp_second_deriv_at_zero, which substitutes the composition equality and applies Jlog_second_deriv_at_zero.
why it matters
This packages the calibration axiom (A4) that fixes the scale of the J function. It completes the characterization of J in the Recognition Science framework by enforcing unit curvature at the identity. The module thereby supplies the normalization required for downstream cost and mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.