Jcost_comp_exp_eq_Jlog
plain-language theorem explainer
The lemma establishes that the composition of Jcost with the exponential map equals the Jlog function pointwise on the reals. Researchers calibrating the cost functional in Recognition Science cite this identity when transferring normalization conditions between linear and logarithmic coordinates. The proof is a single reflexivity step that follows immediately from the definition of Jlog.
Claim. $ (Jcost ∘ exp) = Jlog $
background
The Cost.Calibration module fixes the scale of the cost functional by proving that the second derivative of Jlog at zero equals 1, which is axiom A4. Jcost is the base cost function on positive reals; Jlog is defined in sibling modules as the composition Jcost(exp t), pulling the functional back to additive coordinates on the line. The upstream Calibration class encodes this as the requirement that the second derivative of F(exp t) at zero equals 1, ensuring a unique solution rather than a family of scaled functionals.
proof idea
The proof is a term-mode reflexivity that matches the definition of Jlog as Jcost composed with exp.
why it matters
This identity supplies the definitional bridge that lets the second-derivative condition on Jlog transfer directly to Jcost, completing the unit-curvature normalization in the forcing chain. It supports the unique characterization of J under the Recognition Composition Law. The lemma closes a notational gap inside the calibration module with no open questions remaining.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.