AveragingDerivation
plain-language theorem explainer
AveragingDerivation packages symmetry under inversion, normalization at unity, and exact agreement with Jcost on the exponential image into a single typeclass for candidate cost maps. Derivations of agreement between F and Jcost on positives cite the interface when closing the averaging step. The declaration is realized as a direct class extension of SymmUnit by the AgreesOnExp field.
Claim. A map $F : ℝ → ℝ$ satisfies the averaging derivation property when $F(x) = F(x^{-1})$ for all $x > 0$, $F(1) = 0$, and $F(e^t) = Jcost(e^t)$ for every real $t$.
background
The JcostCore module supplies the minimal interface for cost functions used throughout the Recognition Science development. SymmUnit encodes the two axioms that any admissible F must be invariant under inversion on the positive reals and must vanish at the multiplicative identity. AgreesOnExp requires that F reproduces the J-cost exactly when its argument lies on the image of the exponential map. The same interface appears in the parent Cost module and in the FlogEL variant, allowing separate but parallel developments of the averaging argument.
proof idea
The declaration is a class definition that extends SymmUnit by adjoining the single field AgreesOnExp. No proof body exists; the object is an interface rather than a derived statement.
why it matters
The interface is invoked by F_eq_J_on_pos_of_derivation to obtain pointwise equality of F with Jcost on positives, and by deriv_Flog_zero_of_derivation to conclude that the derivative of Flog vanishes at the origin. It supplies the averaging step that forces candidate cost functions to coincide with Jcost, a prerequisite for the phi-ladder mass formula and the eight-tick octave in the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.