deriv_Jlog_zero
plain-language theorem explainer
The derivative of the log-domain cost function Jlog vanishes at the origin. Researchers analyzing the Recognition Science cost axioms cite this when they differentiate the exponential reparametrization of Jcost. The proof is a one-line wrapper that invokes the hasDerivAt_Jlog_zero lemma and extracts its derivative value.
Claim. Let $J_ {log} : ℝ → ℝ$ be defined by $J_{log}(t) := J_{cost}(exp t)$. Then $d/dt J_{log}(t)|_{t=0} = 0$.
background
In the Cost module, Jlog is introduced as the composition Jlog(t) := Jcost(exp t). This places the cost in log-domain coordinates and appears in sibling definitions that relate the cost to its symmetric and exponential forms. The upstream result hasDerivAt_Jlog_zero asserts HasDerivAt Jlog 0 0 and rests on the definition of Jlog together with the differentiability properties of Jcost.
proof idea
The proof is a one-line wrapper. It invokes the hasDerivAt_Jlog_zero lemma, applies the .deriv field to obtain the derivative value at zero, and uses simpa to discharge the goal.
why it matters
This lemma supplies the vanishing derivative needed for local analysis of the cost function near the identity. It sits inside the Cost module that supports the J-cost axioms used throughout the Recognition Science development. No downstream uses are recorded yet, but it closes a basic differentiability fact for the log-domain cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.