T5_EL_equiv_general
plain-language theorem explainer
The theorem shows that any function F obeying the averaging derivation condition induces a composed map t |-> F(exp t) whose derivative vanishes at the origin, which is its unique global minimum of value zero. Analysts verifying the log-domain translation of J-cost uniqueness in Recognition Science cite the result when confirming that the exponential reparametrization preserves the T5 characterizing properties. The proof is a direct term-mode refinement that assembles the three component lemmas for the derivative, non-negativity, and zero-set.
Claim. Let $F : {R} {to} {R}$ satisfy the averaging derivation condition $F(e^{t}) = J_{cost}(e^{t})$ for all real $t$. Then the function $t {mapsto} F(e^{t})$ satisfies $frac{d}{dt} F(e^{t}) big|_{t=0} = 0$, $F(e^{0}) le F(e^{t})$ for all $t$, and $F(e^{t}) = 0$ if and only if $t = 0$.
background
The module develops the log-domain formulation of cost by composing the J-cost with the exponential map. Flog is defined by Flog F (t) := F(exp t). The AveragingDerivation typeclass extends the symmetric unit property with the agreement condition that F(exp t) equals Jcost(exp t) for every real t. This places the result in the setting where derivative calculations and uniqueness statements are transferred from the native positive-real domain to the additive real line.
proof idea
The proof is a one-line term wrapper. It refines the conjunctive goal and discharges the three subgoals by direct application of deriv_Flog_zero_of_derivation, Flog_nonneg_of_derivation, and Flog_eq_zero_iff_of_derivation, each instantiated on the given F.
why it matters
The declaration supplies the general T5 uniqueness statement in the exponential-logarithmic domain, confirming that the log-domain cost inherits vanishing derivative at zero, non-negativity, and unique zero at the origin. It supports the J-uniqueness step of the forcing chain (T5) and the Recognition Composition Law by providing the translated properties needed for derivative-based arguments. No downstream uses are recorded yet, but the result closes a translation interface between the core Cost module and the FlogEL development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.