deriv_Flog_zero_of_derivation
plain-language theorem explainer
The derivative at the origin of the cost function obtained by composing an averaging derivation with the exponential vanishes. Researchers establishing the minimum property for J-uniqueness in log coordinates would cite this lemma. The proof extracts the derivative value directly from the has-derivative result at zero.
Claim. Let $F : {R} {to} {R}$ satisfy the averaging derivation condition. Then $d/dt [F(e^t)]$ evaluated at $t=0$ equals zero.
background
The module treats log-domain costs obtained by composing J-cost with the exponential. An averaging derivation on a function F requires that F applied to the exponential of any real number equals the J-cost of that exponential, while also satisfying the symmetric unit property. This construction allows derivative analysis in additive coordinates.
proof idea
It is a one-line wrapper that invokes the has-derivative lemma for the composed function at argument zero and then applies the derivative accessor to the resulting has-derivative fact.
why it matters
The lemma provides the derivative-at-zero component for the general equivalence theorem that encodes the T5 uniqueness properties in the exponential-log setting. It contributes to the forcing chain by confirming the stationary point required for the self-similar fixed point. No open questions are directly addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.