AveragingAgree
AveragingAgree is a typeclass asserting that a real-valued function F agrees with the J-cost function on every point of the form exp(t). Cost theorists cite it when they need to guarantee that an arbitrary F matches Jcost under exponential averaging before deriving equality on the positive reals. The declaration is a direct class wrapper around the AgreesOnExp predicate.
claimA function $F : ℝ → ℝ$ satisfies AveragingAgree if $F(e^t) = J(e^t)$ for all real $t$, where $J$ denotes the J-cost function.
background
AgreesOnExp is the predicate ∀ t : ℝ, F (exp t) = Jcost (exp t). This predicate is defined both in the parent Cost module and again inside JcostCore, where it serves as the sole field of the AveragingAgree class. The JcostCore module develops the algebraic and positivity properties of Jcost that later feed into mass formulas and the phi-ladder. Upstream results include the gap function F(Z) = log(1 + Z/φ)/log(φ) from AnchorPolicy and the generating functional F(z) = log(1 + z/φ) from Pipelines, both of which are special cases of the same logarithmic form used to define Jcost.
proof idea
This is a class definition whose single field is the AgreesOnExp predicate. No lemmas or tactics are invoked; the declaration simply packages the agreement condition as a typeclass.
why it matters in Recognition Science
AveragingAgree supplies the hypothesis for the theorem F_eq_J_on_pos_of_averaging, which concludes F x = Jcost x for all x > 0. It also receives the canonical instance from Jcost_agrees_on_exp, which proves AgreesOnExp Jcost by reflexivity. In the Recognition framework the class closes the interface between arbitrary averaging functions and the canonical J-cost, supporting later applications of the Recognition Composition Law on the positive reals.
scope and limits
- Does not constrain F on non-positive reals.
- Does not impose continuity, differentiability, or any other regularity on F.
- Does not specify a concrete construction for F beyond the exponential agreement condition.
Lean usage
instance : AveragingAgree Jcost := ⟨Jcost_agrees_on_exp⟩formal statement (Lean)
166class AveragingAgree (F : ℝ → ℝ) : Prop where
167 agrees : AgreesOnExp F
168