AveragingAgree
AveragingAgree packages the requirement that a function F from reals to reals agrees with the J-cost function exactly on all positive exponential inputs. Cost-module derivations and averaging lemmas cite this class to obtain pointwise equality results on the positive reals. The declaration is a direct one-field class wrapper around the AgreesOnExp predicate.
claimA function $F : ℝ → ℝ$ satisfies AveragingAgree when $F(e^t) = J(e^t)$ holds for every real $t$, where $J$ is the J-cost function.
background
The Cost module introduces Jcost as the core cost function on positive reals, equipped with symmetry, non-negativity, and agreement properties. AgreesOnExp is the predicate ∀ t : ℝ, F (exp t) = Jcost (exp t). AveragingAgree is the typeclass that records this predicate as an instance field for use in conditional theorems.
proof idea
One-line class definition that directly requires the AgreesOnExp field; no lemmas or tactics are invoked beyond the referenced definition of AgreesOnExp.
why it matters in Recognition Science
The class supplies the hypothesis for the theorem F_eq_J_on_pos_of_averaging, which concludes F x = Jcost x for x > 0. It supports the cost-equivalence steps that feed into Recognition Science averaging derivations and the J-uniqueness results in the forcing chain.
scope and limits
- Does not assert that any concrete F satisfies the agreement.
- Does not extend the agreement condition to non-exponential arguments.
- Does not compute numerical values or closed forms for Jcost.
- Does not address spatial dimension or phi-ladder rung assignments.
Lean usage
theorem F_eq_J_on_pos_of_averaging {F : ℝ → ℝ} [AveragingAgree F] : ∀ {x : ℝ}, 0 < x → F x = Jcost x := F_eq_J_on_pos (hAgree := AveragingAgree.agrees (F:=F))formal statement (Lean)
46class AveragingAgree (F : ℝ → ℝ) : Prop where
47 agrees : AgreesOnExp F
48