AveragingAgree
plain-language theorem explainer
AveragingAgree packages the requirement that a function F from reals to reals satisfies F(exp t) equals Jcost(exp t) for every real t. Researchers deriving cost equalities or gap functions in Recognition Science invoke the class to obtain pointwise agreement on positive reals. The declaration is a direct class definition whose single field embeds the AgreesOnExp predicate.
Claim. A function $F : ℝ → ℝ$ satisfies AveragingAgree when $F(e^t) = Jcost(e^t)$ holds for every real number $t$.
background
The Cost module introduces Jcost as the core cost function obeying symmetry, non-negativity, and the J-cost functional equation. AgreesOnExp is the predicate ∀ t : ℝ, F(Real.exp t) = Jcost(Real.exp t), which encodes agreement after exponential reparametrization. The class AveragingAgree is defined in both the local module and its JcostCore sibling, serving as the interface for physics modules that supply candidate functions F such as gap or generating functionals.
proof idea
This is a class definition that directly wraps the AgreesOnExp predicate into a typeclass field named agrees. No tactics or lemmas are applied; the declaration simply records the agreement condition for later instance synthesis.
why it matters
AveragingAgree supplies the hypothesis for the theorem F_eq_J_on_pos_of_averaging, which concludes F x = Jcost x whenever x > 0. The same class receives an instance from Jcost_agrees_on_exp in JcostCore, confirming that the core cost function itself satisfies the averaging condition. This step supports the Recognition Science derivation of physical quantities from the J-cost via exponential agreement, consistent with the phi-ladder and gap constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.