hasDerivAt_Flog_of_derivation
plain-language theorem explainer
The lemma establishes that any F satisfying the AveragingDerivation typeclass yields a function Flog F whose derivative at every real t equals sinh(t). Cost analysts working inside the Recognition Science cost layer cite the result to move differentiability statements from the canonical Jlog to arbitrary averaging derivations. The proof is a one-line wrapper that invokes hasDerivAt_Jlog and rewrites through the equality Flog F = Jlog supplied by Flog_eq_Jlog.
Claim. If $F$ satisfies the averaging derivation condition, then the derivative of $Flog_F$ at $t$ equals $sinh(t)$ for every real $t$, where $Flog_F(t) := F(e^t)$.
background
The Cost.FlogEL module treats log-domain cost functions obtained by composing Jcost with the exponential. Jlog is defined by Jlog(t) := Jcost(exp t) and carries the derivative statement HasDerivAt Jlog (sinh t) t from the upstream lemma hasDerivAt_Jlog. AveragingDerivation is the typeclass that forces F(exp t) = Jcost(exp t) for all t, thereby making Flog F coincide pointwise with Jlog. This construction sits inside the Recognition Science treatment of cost functions obeying the Recognition Composition Law.
proof idea
The proof is a one-line wrapper. It obtains the derivative statement for Jlog at the given t, records the equality Flog F = Jlog from Flog_eq_Jlog, and applies simpa to rewrite the derivative through that equality.
why it matters
The lemma supplies the differentiability of Flog required by the downstream result deriv_Flog_zero_of_derivation, which evaluates the derivative at zero. It closes the transfer of the hyperbolic derivative formula from the canonical Jlog representation to arbitrary averaging derivations, supporting the T5 J-uniqueness identification of J with the hyperbolic-cosine expression.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.