AveragingDerivation
AveragingDerivation specifies that a real-valued function F is a symmetric unit (inversion-symmetric for positive arguments with F(1) equal to zero) and matches the J-cost function exactly on the range of the exponential. Cost theorists in Recognition Science cite it when proving that any such F coincides with Jcost for all positive reals. The declaration is a direct class extension with no proof body or lemmas applied.
claimA function $F : ℝ → ℝ$ satisfies the averaging derivation property when $F(x) = F(x^{-1})$ for all $x > 0$, $F(1) = 0$, and $F(e^t) = J(e^t)$ for every real $t$, where $J$ is the J-cost function.
background
The JcostCore module introduces the J-cost as the base cost measure satisfying the Recognition Composition Law. SymmUnit encodes the two axioms of inversion symmetry on positives and normalization at unity. AgreesOnExp requires exact matching with Jcost when the input is written as an exponential, which aligns with the logarithmic scale used throughout the cost derivations.
proof idea
This is a class definition that extends SymmUnit by adjoining the AgreesOnExp field. No lemmas are invoked and no tactics are used; the structure is purely declarative.
why it matters in Recognition Science
The class feeds the theorems F_eq_J_on_pos_of_derivation and agrees_on_exp_of_symm_unit, which establish that any averaging derivation equals Jcost on positives. It supports the equivalence steps in the FlogEL derivations and the broader identification of cost functions with the J-uniqueness fixed point from the forcing chain.
scope and limits
- Does not give an explicit closed form for the J-cost function.
- Does not constrain the behavior of F on non-positive reals.
- Does not impose differentiability or continuity requirements.
- Does not assert uniqueness of functions satisfying the property.
formal statement (Lean)
169class AveragingDerivation (F : ℝ → ℝ) : Prop extends SymmUnit F where
170 agrees : AgreesOnExp F
171