AveragingAgree
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.