AveragingDerivation
AveragingDerivation equips a map F from reals to reals with the property that F composed with exp agrees exactly with Jcost on the image of exp, while inheriting symmetry under inversion and vanishing at 1 from the SymmUnit parent class. Cost analysts working in the log domain cite this interface to transfer multiplicative properties of Jcost into additive statements about Flog. The declaration is a direct class extension with no separate proof steps.
claimA function $F : {R} {R}$ satisfies the averaging derivation property when it extends the symmetric-unit conditions (i.e., $F(x) = F(x^{-1})$ for $x > 0$ and $F(1) = 0$) and obeys $F(e^{t}) = J_{cost}(e^{t})$ for every real $t$.
background
The module treats log-domain cost by defining Flog F t := F (exp t). SymmUnit supplies the two axioms that F is invariant under inversion on the positive reals and vanishes at unity. AveragingDerivation extends SymmUnit by the single additional axiom that F agrees with Jcost after the exponential change of variables.
proof idea
This is a class definition that directly extends SymmUnit with the agrees axiom. No lemmas or tactics are invoked; the structure is introduced by fiat.
why it matters in Recognition Science
Downstream lemmas such as F_eq_J_on_pos_of_derivation and Flog_eq_Jlog rely on this interface to equate F with Jcost and Flog with Jlog. It supplies the bridge that lets the Recognition cost framework move statements between the multiplicative positive line and the additive log line, supporting later results on derivatives and non-negativity of Flog.
scope and limits
- Does not assert existence of any concrete F satisfying the axioms.
- Does not constrain the values of F on non-positive reals.
- Does not derive the explicit functional form of F beyond the stated agreement.
formal statement (Lean)
43class AveragingDerivation (F : ℝ → ℝ) : Prop extends SymmUnit F where
44 agrees : ∀ t : ℝ, F (Real.exp t) = Jcost (Real.exp t)
45
46/-- Flog definition -/