Jcost_is_calibrated
plain-language theorem explainer
Jcost satisfies the calibration condition required by uniqueness theorems in Recognition Science. Researchers establishing the T5 result on cost functionals would cite this to confirm the second-derivative normalization of Jcost in logarithmic coordinates. The proof is a one-line wrapper that rewrites the IsCalibrated predicate and applies the pre-established log-second-derivative lemma for Jcost.
Claim. The cost function $J$ satisfies the calibration condition $G''(0)=1$, where $G(t)=J(e^t)$.
background
The CostUniqueness module consolidates convexity, calibration, and functional-equation results to prove that any cost functional satisfying symmetry, unit normalization, strict convexity, and calibration equals Jcost on the positive reals; this is the main unconditional T5 statement. Jcost is the explicit cost function derived from the Recognition Composition Law, written equivalently as $(x+x^{-1})/2-1$ or cosh(log x)-1. The predicate IsCalibrated, defined in FunctionalEquation, requires that the second derivative of the composition of F with the exponential map equals 1 at the origin.
proof idea
The proof is a term-mode wrapper. A change tactic rewrites the IsCalibrated statement for Jcost into the explicit form deriv(deriv(fun t => Jcost (exp t))) 0 = 1. The lemma Jcost_log_second_deriv_normalized from CPM.LawOfExistence is then applied exactly to discharge the goal.
why it matters
This declaration supplies the calibration satisfaction for Jcost, a required hypothesis in the main uniqueness theorem of the CostUniqueness module. It supports the T5 J-uniqueness step in the Recognition Science forcing chain (T5 through T8), where J is identified as the unique cost satisfying the functional equation on positive reals. The result closes one calibration interface needed for the unconditional T5 claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.