Flog_eq_zero_iff_of_derivation
plain-language theorem explainer
The lemma establishes that for any averaging derivation F the log-domain cost vanishes at t precisely when t is zero. Researchers verifying uniqueness properties of the J-cost in exponential coordinates would cite this equivalence. The argument is a one-line wrapper that reduces the claim to the known zero set of Jlog after rewriting via the pointwise identification Flog F t = Jlog t.
Claim. Let $F : {R} {to} {R}$ be an averaging derivation. Then for every real $t$, the log-domain cost $F({exp} t)$ equals zero if and only if $t = 0$.
background
The module works in the log-domain formulation of the J-cost obtained by composing with the exponential map. AveragingDerivation is the typeclass that extends the symmetric unit property and requires F(exp t) to agree with Jcost(exp t) for all real t. Flog is defined by sending t to F(exp t). The lemma rests on the upstream result that Jlog t vanishes exactly at t = 0 together with the identification lemma showing Flog coincides with Jlog pointwise under the derivation assumption.
proof idea
The proof obtains the zero-set characterization of Jlog at t and rewrites the left-hand side via the pointwise equality Flog F t = Jlog t supplied by the identification lemma.
why it matters
The equivalence is invoked inside T5_EL_equiv_general to assemble the derivative condition at zero, non-negativity, and zero-set uniqueness for the log-domain cost. It thereby contributes to the verification of T5 J-uniqueness in the forcing chain, consistent with the Recognition Science derivation of the functional equation for J.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.