AveragingDerivation
plain-language theorem explainer
AveragingDerivation packages the requirements that a real-valued function F is symmetric under inversion with F(1) equal to zero and matches Jcost exactly on the positive reals via the exponential map. Cost derivations in the Recognition Science framework cite this class when relating candidate averaging functions to the core J-cost. The declaration is a direct class extension of SymmUnit by the AgreesOnExp predicate.
Claim. A function $F : ℝ → ℝ$ satisfies AveragingDerivation when it obeys the symmetry $F(x) = F(x^{-1})$ for all $x > 0$, the normalization $F(1) = 0$, and the agreement condition $F(e^t) = Jcost(e^t)$ for every real $t$.
background
The Cost module defines interfaces for functions that compute costs compatible with the J-cost core. SymmUnit requires inversion symmetry $F(x) = F(x^{-1})$ for positive arguments together with the unit condition $F(1) = 0$. AgreesOnExp is the predicate that forces exact agreement with Jcost after mapping through the exponential. The same class appears in JcostCore and FlogEL, serving as a shared interface. Upstream results supply the component definitions used to build agreement and symmetry lemmas.
proof idea
This is a class definition that extends SymmUnit by adjoining the AgreesOnExp field. No lemmas or tactics are invoked; the structure is assembled directly from the two component properties.
why it matters
AveragingDerivation supplies the typeclass hypothesis for theorems such as F_eq_J_on_pos_of_derivation and agrees_on_exp_of_symm_unit, which recover pointwise agreement with Jcost on the positives. It is also used in FlogEL for results including Flog_eq_Jlog and deriv_Flog_zero_of_derivation. The class closes the interface between symmetry axioms and explicit cost matching, supporting the J-uniqueness step in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.