Flog_eq_Jlog
plain-language theorem explainer
Given that F satisfies the averaging derivation condition, the composition of F with the exponential equals the canonical log-domain cost. Cost analysts in the Recognition Science setting cite the result when moving between parameterized and standard representations of the J-cost. The proof reduces the functional claim to the pointwise case via extensionality and invokes the agreement axiom directly.
Claim. If $F$ is an averaging derivation, then the map $tmapsto F(e^t)$ equals the map $t mapsto Jcost(e^t)$.
background
The module develops log-domain costs by composing the J-cost with the exponential. The canonical log-domain cost is the composition of Jcost with exp. Flog applies the same composition to an arbitrary function F. The averaging derivation class extends SymmUnit and requires that F agrees with Jcost on the exponential image, that is F(exp t) equals Jcost(exp t) for every real t. This lemma follows the pointwise agreement result, which applies the agrees field of the class directly.
proof idea
One-line wrapper that applies function extensionality and then supplies the pointwise equality lemma.
why it matters
The equality transfers derivative information from the canonical log-domain cost to the parameterized version. It is consumed by the derivative lemma that rewrites the derivative of the canonical cost through this functional identity. In the Recognition framework the result supports cost calculations in the log domain and aligns with the J-uniqueness step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.